HodgeType
plain-language theorem explainer
This inductive definition enumerates the five canonical Hodge types at degree 2 on the discrete recognition lattice. Algebraic geometers translating the Hodge conjecture into Recognition Science terms would cite it when working with the discrete ledger version. The definition is realized directly as an inductive type with automatic derivation of decidability and finiteness.
Claim. The five Hodge types at degree 2 are the primitive, non-primitive, effective, ample, and nef classes.
background
Recognition Science translates the Hodge conjecture as homology classes stable under coarse-graining equaling algebraic cycles, with algebraic cycles identified as J-cost zeros on the discrete lattice. A coarse-grained recognition class is a sub-manifold of the recognition lattice, and the discrete Hodge asserts J-cost stable classes equal algebraic cycles on Q₃. This module introduces five canonical Hodge types in degree 2 to match configDim D = 5, where D = 3 follows from the forcing chain T8.
proof idea
The declaration is an inductive definition that directly enumerates the five types primitive, non-primitive, effective, ample, and nef, with derived instances for DecidableEq, Repr, BEq, and Fintype.
why it matters
This definition supplies the enumeration required by the downstream structural certificate HodgeConjStructuralCert, which records Fintype.card HodgeType = 5 together with discreteHodgeDimension = 3 and 2^discreteHodgeDimension = 8. It fills the discrete ledger opening for the Hodge conjecture stated in the module documentation, linking stable homology classes to algebraic cycles on Q₃. The construction touches the still-open bridge from the discrete ledger to continuous algebraic geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.