harmonicFormsCert
plain-language theorem explainer
The harmonicFormsCert theorem certifies that every coarse-graining stable class on a defect-bounded sub-ledger admits a J-cost-critical representative realized as a minimal cycle, with Hodge decomposition holding at zero correction and the hard direction of the RS Hodge conjecture following from the defect budget. Researchers translating classical Hodge theory into Recognition Science cite this to confirm existence of harmonic representatives under bounded defect. The proof is a term-mode structure construction that sets one field to triviality
Claim. Let $L$ be a defect-bounded sub-ledger. The HarmonicFormsCert structure holds: the J-cost critical structure is defined; for any coarse-graining stable class $cls$ with $z$-charge zero there exists a J-cost minimal cycle generating $cls$; a Hodge decomposition exists with zero correction whenever the defect of $L$ is at most 1; and the hard direction follows from the defect budget.
background
In Recognition Science the classical Hodge theorem is recast by equating harmonic forms with J-cost critical points on sub-ledgers, where the gradient of J-cost vanishes on the boundary. A DefectBoundedSubLedger carries a bounded defect measure, while a CoarseGrainingStableClass represents a cohomology class that survives all coarse-graining flows. The module imports LedgerForcing and HodgeConjecture to supply the necessary ledger and decomposition primitives. Upstream, hard_direction_via_defect_budget states that if every flow is stable then a minimal cycle exists; harmonic_form_theorem_zero_charge supplies the zero-charge case; and hodge_decomposition_exists guarantees a decomposition with vanishing correction when defect ≤ 1.
proof idea
The proof is a term-mode construction of the HarmonicFormsCert structure. The critical_defined field is set to trivial. The zero_charge_case field is obtained by direct application of harmonic_form_theorem_zero_charge. The decomposition_exists field is supplied by hodge_decomposition_exists. The hard_direction_budget field is supplied by hard_direction_via_defect_budget.
why it matters
This declaration assembles the hard direction of the RS Hodge conjecture by bundling the zero-charge minimal-cycle existence, zero-correction decomposition, and defect-budget argument into one certificate. It rests on the module's identification of harmonic forms with J-cost critical points and supports downstream ledger-forcing results that every stable class is generated by a minimal cycle under the zero-limit flow condition. The result touches the Recognition Science translation of Hodge theory but does not yet address the full conjecture for unbounded defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.