RSHodgeConjecture
plain-language theorem explainer
The RS Hodge Conjecture defines the open statement that every coarse-graining-stable class on a defect-bounded sub-ledger is generated by J-cost-minimal cycles via their z-charge sum. Algebraic geometers and Recognition Science researchers formalizing the Hodge conjecture would cite this as the untranslated hard direction. The definition is a direct encoding of the classical statement into ledger vocabulary with no internal proof steps.
Claim. For every defect-bounded sub-ledger $L$ and every coarse-graining-stable class $cls$ on $L$, there exists a finite list of J-cost-minimal cycles such that the z-charge of $cls$ equals the sum of the z-charges of the cycle classes of those cycles.
background
In the Recognition Science translation, a defect-bounded sub-ledger is a finite voxel set with bounded J-cost, a coarse-graining-stable class is a cohomological feature that survives the data-processing inequality under coarse-graining, and a J-cost-minimal cycle is a recognition-closed subgraph with zero defect on its closure. The module dictionary maps classical varieties to sub-ledgers, Hodge classes to stable classes, and algebraic cycles to minimal cycles. One direction is already proved as a theorem: every J-cost-minimal cycle yields a coarse-graining-stable class.
proof idea
The declaration is a definition that directly states the open conjecture as a universal quantification over sub-ledgers and stable classes. No tactics or lemmas are applied inside the definition itself. Surrounding results in the module establish the converse direction for special cases such as trivial ledgers and unit-defect ledgers.
why it matters
This definition supplies the open half of the RS Hodge conjecture and is referenced by the status certificate HodgeCert as well as the theorem that stable classes must carry zero z-charge. It corresponds to the hard direction in the Recognition Science formalization of the classical Hodge conjecture. Downstream theorems prove the statement for asymptotically trivial and unit-defect sub-ledgers, leaving the general case open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.