hodgeTypeCount
plain-language theorem explainer
The discrete Hodge conjecture in Recognition Science asserts exactly five canonical types for degree-2 classes on the recognition lattice at D=3. Researchers working on the discrete version of the Hodge conjecture cite this cardinality result when certifying the structural match to algebraic cycles. The proof is a one-line decision procedure that enumerates the five constructors of the inductive type HodgeType.
Claim. The finite type of Hodge types at degree 2 on the discrete recognition lattice satisfies $|HodgeType| = 5$, where the five classes are primitive, non-primitive, effective, ample and nef.
background
In the Recognition Science translation of the Hodge conjecture, homology classes stable under coarse-graining correspond to algebraic cycles on the discrete lattice Q3. The module defines five Hodge types at degree 2 via the inductive type with constructors primitive, nonPrimitive, effective, ample and nef; these represent the distinct J-cost zero configurations that remain invariant under the recognition composition law. The upstream arithmetic canonical objects and beat structures supply the counting mechanisms used to enumerate these types on the phi-ladder at D=3.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Because HodgeType derives Fintype and contains exactly five constructors, the cardinality computation evaluates directly to five without further lemmas.
why it matters
This cardinality result supplies the five_hodge_types field in the structural certificate hodgeConjStructuralCert. It fills the discrete ledger step of the Hodge conjecture opening in biggest-questions.md §XXIII, confirming that the number of stable classes equals five at D=3 and anchoring the claim that configDim D equals five. The continuous bridge to algebraic geometry remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.