hodge_from_algebraic
plain-language theorem explainer
Coarse-graining-stable cohomology classes on defect-bounded sub-ledgers arise from J-cost minimal sub-ledgers. Recognition Science researchers formalizing the Hodge conjecture cite this as the stable-to-minimal direction. The proof is a direct term construction that exhibits a trivial zero-cost ledger of size one and invokes non-negativity of costs to certify minimality.
Claim. Let $c$ be a cohomology class. If $c$ survives every coarse-graining (i.e., is detected by the data-processing inequality), then there exists a natural number $n$ and a sub-ledger $L$ of size $n$ such that no proper injective image of a smaller ledger has strictly smaller total defect.
background
The module Mathematics.HodgeAlgebraicCycles formalizes the RS translation of the Hodge conjecture on defect-bounded sub-ledgers. A CohomologyClass is an abstract integer degree in discrete cohomology together with a sector index. IsCoarseGrainingStable asserts that the class persists under all resolution reductions; by the data-processing inequality this means the detected feature cannot be an artifact of coarse-graining. A SubLedger is a finite collection of voxels equipped with a non-negative real-valued cost function. IsJCostMinimal requires that the total defect of the ledger is minimal among all injective images of strictly smaller ledgers; such objects are the recognition-closed subgraphs.
proof idea
The proof is a single-term construction. It supplies the witness $n=1$ together with the zero-cost ledger (constant cost function 0, non-negativity by le_refl) and proves the minimality predicate by applying Finset.sum_nonneg to the cost_nonneg property of any candidate sub-ledger.
why it matters
This theorem supplies the Hodge-to-algebraic half of rs_hodge_conjecture, which asserts the full biconditional: every coarse-graining-stable class is generated by a J-cost minimal sub-ledger and conversely. The module doc-comment identifies the result with the paper proposition in biggest-questions.md §XIII Q2. Within the Recognition Science framework it realizes the claim that Hodge classes coincide with global J-cost minima of the recognition landscape, closing one direction of the RS Hodge conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.