HodgeAlgebraicCyclesCert
plain-language theorem explainer
A certificate structure records the biconditional between coarse-graining-stable cohomology classes and those generated by J-cost minimal sub-ledgers on defect-bounded sub-ledgers. Researchers working on the Recognition Science translation of the Hodge conjecture cite this record as the complete equivalence. It is introduced as a structure definition that assembles the two proved implications without further derivation steps.
Claim. A structure whose fields assert that a cohomology class $c$ is coarse-graining stable if and only if there exists $n$ in the natural numbers and a sub-ledger $L$ of size $n$ such that $L$ is minimal with respect to total J-cost.
background
A sub-ledger is a finite collection of voxels equipped with a nonnegative real-valued cost function; its total defect is the sum of these costs. A cohomology class is an abstract object given by an integer degree and a sector index. J-cost minimal sub-ledgers are those for which no proper sub-collection obtained by an injective map has strictly lower total defect; these are the recognition-closed subgraphs. Coarse-graining-stable classes are those that survive every resolution-reducing map, as required by the data processing inequality on Kullback-Leibler divergence.
proof idea
This declaration is a structure definition. It directly encodes the required properties as three fields of the record: the implication from J-cost minimal sub-ledgers to stable classes, the existence of such a minimal sub-ledger for every stable class, and the resulting biconditional. No tactics are used; the structure serves as a container for the two directions established by the algebraic generation lemma and the Hodge extraction lemma in the same module.
why it matters
This certificate completes the formalization of the RS Hodge conjecture by bundling both directions of the equivalence. It is instantiated in the downstream definition that constructs the concrete certificate. The result addresses the question in biggest-questions.md §XIII Q2 and supplies the Recognition Science translation of the classical Hodge conjecture, identifying stable cohomology classes with those generated by J-cost minima on defect-bounded sub-ledgers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.