hodge_decomposition_exists
plain-language theorem explainer
For any defect-bounded sub-ledger with defect at most 1 that belongs to a coarse-graining stable class, a Hodge decomposition exists with the correction term exactly zero. Researchers translating classical Hodge theory into Recognition Science would cite this when establishing minimal J-cost representatives for cohomology classes. The proof is a direct construction that invokes the minimal-ledger harmonic form theorem and assembles the decomposition record with zero correction.
Claim. Let $L$ be a defect-bounded sub-ledger with defect$(L) ≤ 1$ and let cls be a coarse-graining stable class of $L$. Then there exists a Hodge decomposition of cls in which the correction term vanishes.
background
In Recognition Science the classical Hodge theorem is recast by equating harmonic forms with J-cost critical points on sub-ledgers. The HodgeDecomposition structure encodes every stable class as a zero-defect cycle (the harmonic part) plus a real correction that satisfies the charge equation and obeys a smallness bound. The module setting asserts that stability forces the correction to be zero, so the decomposition reduces to a pure minimal cycle.
proof idea
The proof calls harmonic_form_theorem_minimal_ledger to obtain a JCostMinimalCycle, then builds the decomposition record with harmonic_part set to that cycle and correction set to zero. The decomp_eq field is discharged by rewriting the cycle property and applying ring, while correction_small follows from abs_nonneg.
why it matters
This supplies the decomposition_exists clause inside the HarmonicFormsCert certificate. It advances the hard direction of the RS Hodge conjecture by pairing the defect budget theorem with the zero-charge harmonic form theorem, thereby closing the step from stable classes to J-cost minimal cycles. The result aligns with the J-uniqueness property in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.