Theorems

59 statements accepted by the Lean 4 kernel, of 83 in the corpus. 51 rest on no axioms at all. The other 24 are written down and not proved, and say so — see the ledger.

Every page below carries its statement as written, what the proof rests on, its source line, and the theorems that speak of the same defined objects.

DigitSpace.lean

• agl has order 54
• all three are multiples of thirty six
• astronomical unit has digital root three
• base frequency has digital root nine
• being an involution is not enough for harmony
• c squared exceeds the exact range of a double
• c squared is exact
• doubling and mirror are affine
• doubling and mirror are affine axiom free
• doubling stays in orbit
• doubling stays in orbit axiom free
• dr and drTS differ at zero
• dr idempotent
• dr invariant under nine
• dr is drTS above zero
• 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
• exceeding the range is the hazard not the error
• four three two has twenty divisors its neighbours eighteen
• four three two is a multiple of thirty six but not the only one
• four triples are closed under the mirror
• generators apart give twelve
• light leaves a null interval
• light year has digital root nine
• light year is c times a julian year
• mirror is affine only off the void
• mirror table is through void
• mirror table is through void axiom free
• no triple is closed under both maps
• non fixed points come in pairs
• orbit and axis and void exhaust the digits
• orbit and axis are disjoint
• orbit and axis are disjoint axiom free
• orbit axis void exhaust the digits axiom free
• orbit closes after six
• orbit never repeats a step
• speed of light has digital root one
• swap12 is an involution
• the astronomical unit stays inside it
• the axis is mirrored onto exactly seven four one
• the axis is the only triple closed under doubling
• the digit root nine sum does not single out the axis
• the digital root of c is not robust
• the four pairs are one nine two eight three seven four six
• the light year exceeds it as well
• the mirror fixes the middle triangle setwise
• the mirror is the involution with a constant orbit sum
• the mirror swaps the first triangle with the axis
• the ten digits are two fixed points and four pairs
• the three triangles partition the nonzero digits
• the triangles are the residues mod three
• the void is the one orbit that does not
• there are eighty four triples
• through void fixes only zero and five
• through void is an involution
• whole axis and root nine is exactly thirty six

---

Cite the concept DOI 10.5281/zenodo.22178675; it resolves to the newest release, where a per-version DOI goes stale.