Orbit sums to zero

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.

THE ODD PART CANCELS OVER EVERY ORBIT. For any involution, any f, any point: the pair {x, σx} sums to exactly zero. This is the general form of "every bit of resistance drains", and the coin's version of it is this theorem at σ d = 10 − d.

Proposition

{α : Type} (f : α → Int) (σ : α → α) (h : IsInvolution σ) (x : α) : odd f σ x + odd f σ (σ x) = 0

Proof

By by in involution.lean. The kernel reduces the proposition and reports no axiom dependency.

Sources and identifiers

• Lean source · src/pair/formal/proofs/involution.lean
• Typeset paper · src/research/lean-theorems.tex
• Repository deposit · doi:10.5281/zenodo.21787144
• Author · ORCID 0009-0000-7312-9778
• Deposit record · involution--orbit_sums_to_zero

Proved in the same file

• Odd vanishes at a fixed point
• EvenPart is symmetric
• The split loses nothing
• The instance is an involution
• The instance cancels over every orbit
• The instance has one harmonic point
• The instance splits without loss

All machine-checked theorems