HodgeDecomposition
plain-language theorem explainer
HodgeDecomposition records the splitting of any coarse-graining stable class into a zero-defect minimal cycle plus a bounded boundary correction. Researchers formalizing the RS version of the Hodge conjecture cite this structure when decomposing Z-charge on defect-bounded sub-ledgers. The definition assembles the four fields directly from the input class and cycle data without invoking lemmas.
Claim. For a defect-bounded sub-ledger $L$ and a coarse-graining stable cohomology class $cls$ on $L$, a Hodge decomposition consists of a minimal J-cost cycle $h$, a real correction $c$, such that the Z-charge of $cls$ equals the Z-charge of $h$ plus $c$, with $|c|$ at most the Z-charge of $cls$.
background
In Recognition Science the classical Hodge theorem is translated by identifying harmonic forms with J-cost critical sub-ledgers. A JCostMinimalCycle is a recognition-closed subgraph with zero net defect, the RS analog of an algebraic cycle. CoarseGrainingStableClass extends a cohomology class by the condition that its Z-charge is fixed under the data processing inequality and bounded by the ledger defect, as stated in its doc-comment: a class survives coarse-graining iff its z_charge is anchored to the actual J-cost structure.
proof idea
This is a structure definition that directly packages the four required fields: the harmonic minimal cycle drawn from JCostMinimalCycle, the correction scalar, the charge equality, and the smallness bound. No tactics or lemmas are applied; the definition serves as the interface for downstream existence theorems such as hodge_decomposition_exists.
why it matters
HodgeDecomposition supplies the data type used by hodge_decomposition_exists to assert that every stable class admits a decomposition with zero correction. It feeds HarmonicFormsCert, which certifies the hard direction of the Hodge conjecture under zero-limit flows. The construction closes the gap between classical Hodge theory and the Recognition Science forcing chain by making the minimal-cycle representative explicit for stable classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.