agObjectCount
plain-language theorem explainer
The Recognition Science lattice Q₃ contains exactly five canonical algebraic geometry objects. Researchers verifying the Hodge connection between RS and Calabi-Yau threefolds at D=3 cite this count to confirm the five Hodge types. The proof is a one-line decision procedure that enumerates the constructors of the inductive type.
Claim. The finite cardinality of the set of canonical algebraic geometry objects is five: $|$affine variety, projective variety, Calabi-Yau, K3 surface, elliptic curve$| = 5$.
background
The module interprets the recognition lattice Q₃ as an algebraic variety over F₂. AlgebraicGeometryObject is the inductive type whose five constructors are affineVariety, projectiveVariety, calabiYau, K3Surface, and ellipticCurve; the Fintype instance is derived automatically. The module states that this count equals configDim D=5 and links the five objects to the Hodge numbers of the Calabi-Yau threefold at D=3.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. Decide computes the cardinality directly from the derived Fintype instance on the inductive type with five constructors.
why it matters
This theorem supplies the five_objects field of algebraicGeometryCert, which certifies the algebraic-geometry content of the RS lattice. It realizes the module claim that five canonical objects match configDim D=5 and supports the Hodge connection to Calabi-Yau threefolds at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.