Odd vanishes at a fixed point

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and resting on no axiom beyond propext and Quot.sound. 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 unfold odd in involution.lean. Checked by the Lean kernel: it rests on propext and on no other axiom.

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