the mirror is the involution with a constant orbit sum

theorem the_mirror_is_the_involution_with_a_constant_orbit_sum :
  (nonzero.map (fun d => d + tv d)) = [10, 10, 10, 10, 10, 10, 10, 10, 10] ∧ (nonzero.map (fun d => d + swap12 d)) ≠ [10, 10, 10, 10, 10, 10, 10, 10, 10]

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:272
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

• being an involution is not enough for harmony
• 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

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.