hodgeAlgebraicCyclesCert
plain-language theorem explainer
The declaration supplies the complete biconditional certificate for the Recognition Science translation of the Hodge conjecture. Researchers working on J-cost minima in defect-bounded sub-ledgers would cite it to invoke the equivalence between algebraic cycles and coarse-graining-stable cohomology classes. It is a direct construction that assembles the algebraic generation result with the stable-class extraction result into the required structure.
Claim. On any defect-bounded sub-ledger, every J-cost minimal sub-ledger generates a coarse-graining-stable cohomology class, and conversely every coarse-graining-stable cohomology class arises from some J-cost minimal sub-ledger. Equivalently, a cohomology class $c$ is coarse-graining-stable if and only if it is generated by a J-cost minimal sub-ledger.
background
A SubLedger is a stable set of voxels carrying a collective J-cost, defined via the Recognition Composition Law. IsJCostMinimal identifies those sub-ledgers that achieve the global minimum of this cost within their cohomological sector. IsCoarseGrainingStable marks cohomology classes that remain invariant under all coarse-grainings, which by the Data Processing Inequality cannot decrease J-cost. The upstream theorem algebraic_generates_hodge shows that any J-cost minimum is automatically preserved by coarse-graining and therefore produces a stable class. The companion result hodge_from_algebraic shows the converse: any class that survives every coarse-graining must be supported exactly on a J-cost minimum.
proof idea
This is a definition that directly instantiates the HodgeAlgebraicCyclesCert structure. It supplies the algebraic-to-Hodge direction by applying algebraic_generates_hodge, supplies the Hodge-to-algebraic direction by applying hodge_from_algebraic, and fills the biconditional field with a trivial equivalence that follows from the two directions already proved.
why it matters
The definition closes both directions of the RS Hodge conjecture inside the Recognition framework, completing the translation stated in biggest-questions.md §XIII Q2. It sits downstream of the J-uniqueness and phi-ladder constructions and supplies the structural link between J-cost minima and stable cohomology classes. No further parent theorems are recorded yet, but the certificate is the natural object any later result on algebraic cycles or defect concentration would invoke.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.