The split loses nothing

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.

AND THE TWO HALVES RECONSTRUCT THE WHOLE. Nothing is lost in the split, and this one needs no involution at all — it is true of the two parts as defined, for every σ.

Proposition

{α : Type} (f : α → Int) (σ : α → α) (x : α) : evenPart f σ x + odd f σ x = 2 * f x

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--the_split_loses_nothing

Proved in the same file

• Orbit sums to zero
• Odd vanishes at a fixed point
• EvenPart is symmetric
• 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