Sigma preserves degree

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.

σ preserves total degree — it acts WITHIN H^n, which is why it decomposes it.

Proposition

∀ t ∈ middleTypes, (σ t).1 + (σ t).2 = t.1 + t.2

Proof

By decide in hodge.lean. The kernel reduces the proposition and reports no axiom dependency.

Sources and identifiers

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

Proved in the same file

• Sigma is an involution
• Fixed type is p equals q
• Diagonal is fixed at every k
• Involution fixes the diagonal

All machine-checked theorems