discrete_hodge_q3_vertex_count
plain-language theorem explainer
The theorem states that the Q3 lattice in the discrete Hodge setting has exactly 8 vertices. Researchers formalizing the Recognition Science translation of the Hodge conjecture cite this to fix the vertex count once the dimension is set to 3. The proof is a one-line decision procedure that reduces the power equality directly from the upstream dimension definition.
Claim. Let $d$ be the discrete Hodge dimension. Then $2^d = 8$.
background
The module supplies the discrete ledger version of the Hodge conjecture inside Recognition Science. Coarse-grained recognition classes are sub-manifolds of the recognition lattice; algebraic cycles are identified with J-cost zeros; the discrete Hodge statement equates J-cost stable classes with algebraic cycles on Q3. Five canonical Hodge types in degree 2 are tied to configDim D = 5. The upstream definition discreteHodgeDimension : ℕ := 3 records the spatial dimension D = 3 from the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic statement 2^3 = 8, using the definition of discreteHodgeDimension as 3.
why it matters
This supplies the q3_vertices field inside the structural certificate hodgeConjStructuralCert that records the discrete ledger part of the RS Hodge translation. It closes the vertex-count step once the dimension is fixed at 3 by the eight-tick octave and T8. The bridge from this discrete ledger to the full algebraic-geometry Hodge conjecture remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.