the mirror swaps the first triangle with the axis
lean
theorem the_mirror_swaps_the_first_triangle_with_the_axis :
triangleOne.map tv = [9, 6, 3] ∧ axis.map tv = [7, 4, 1]Accepted by the Lean 4 kernel. The proof rests on no axioms at all.
Proven means three things together: the kernel accepted the file, the proof contains no sorry, and #print axioms reports a dependency set within {propext, Quot.sound}. The dependency set above is the evidence, recorded per theorem rather than summarised.
| source | lean/DigitSpace.lean:514 |
| archive | doi:10.5281/zenodo.22178675 — the concept DOI, resolving to the newest release |
| corpus | every statement · the ledger |
| reproduce | git clone https://github.com/ceccec/zeropoint-node && npm run lean:check |
Speaks of the same objects as
- every axis digit mirrors an orbit digit
- every axis digit mirrors an orbit digit axiom free
- every mirror orbit sums to ten
- every mirror orbit sums to ten axiom free
- exactly two digits are their own mirror
- mirror is affine only off the void
- mirror table is through void
- mirror table is through void axiom free
What this does not establish
A theorem is a statement the kernel accepted. It says nothing about whether the surrounding package is useful, whether the idea is novel, or whether anything physical follows. Novelty is a universal negative no finite search decides; a dated deposit establishes priority, which is the defensible claim.