Fixed type is p equals q
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 unique fixed type in degree 2k is (k,k). Here k = 2.
Proposition
(middleTypes.filter (fun t => σ t == t)) = [(2,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--fixed_type_is_p_equals_q