HarmonicFormsCert
plain-language theorem explainer
HarmonicFormsCert records that J-cost critical sub-ledgers coincide with minimal cycles when charge vanishes, that Hodge decompositions exist with zero correction for defect at most one, and that every stable class under converging flows is realized by a minimal cycle. A mathematician translating the classical Hodge theorem into Recognition Science would cite the certificate to close the hard direction. The structure is assembled directly from four supporting lemmas already proved in the module.
Claim. Let $L$ be a defect-bounded sub-ledger and let $cls$ be a coarse-graining stable class on $L$. The certificate asserts: (i) if the charge of $cls$ is zero then there exists a minimal J-cost cycle whose class has zero charge; (ii) if the defect of $L$ is at most one then a Hodge decomposition of $cls$ exists whose correction term vanishes; (iii) if every coarse-graining flow on $L$ is stable then there exists a minimal cycle realizing the charge of $cls$.
background
In Recognition Science the Hodge theorem is translated by equating harmonic forms with J-cost critical points of sub-ledgers. A J-cost critical point is a configuration at which the gradient of the recognition cost vanishes on the boundary; the associated minimal cycle is the unique lowest-cost representative of its cohomology class (Z-charge). The Hodge decomposition splits any stable class into a harmonic part plus a correction term that is required to vanish for low-defect ledgers.
proof idea
The certificate is a record structure. Its first field is the trivial proposition True. The remaining three fields are discharged by direct application of the lemmas harmonic_form_theorem_zero_charge, hodge_decomposition_exists, and hard_direction_via_defect_budget, each of which is already established in the same module.
why it matters
The certificate supplies the hard direction of the RS Hodge conjecture under the zero-limit flow assumption stated in the module doc-comment: if every coarse-graining flow converges to zero then every stable class is generated by a minimal cycle. It is consumed by the theorem harmonicFormsCert that assembles the full statement. Within the framework it realizes the classical claim that every cohomology class possesses a unique harmonic representative, here identified with a J-cost minimal cycle on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.