Odd vanishes at a fixed point

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 HARMONIC POINT CARRIES NOTHING. Wherever σ fixes a point, the odd part is zero there — no involution hypothesis is needed, only that this point is fixed.

Proposition

{α : Type} (f : α → Int) (σ : α → α) (x : α) (hx : σ x = 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--odd_vanishes_at_a_fixed_point

Proved in the same file

• Orbit sums to zero
• 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