hard_direction_via_defect_budget
plain-language theorem explainer
Any coarse-graining stable class on a defect-bounded sub-ledger that remains stable under every coarse-graining flow must be generated by a J-cost minimal cycle carrying identical Z-charge. Researchers closing the Recognition Science analog of the Hodge conjecture cite this result for the hard direction in zero-limit settings. The argument is a direct composition: defect budget theorem forces zero charge, after which the zero-charge harmonic form theorem supplies the cycle.
Claim. Let $L$ be a defect-bounded sub-ledger and let cls be a coarse-graining stable class on $L$. If every coarse-graining flow on $L$ is stable with respect to cls, then there exists a J-cost minimal cycle cyc on $L$ such that the Z-charge of the cycle class of cyc equals the Z-charge of cls.
background
In the Recognition Science translation of Hodge theory, a harmonic form is a J-cost critical point on a sub-ledger (gradient of J-cost vanishes on the boundary). CoarseGrainingFlow is the structure recording monotone decrease of apparent defect under successive coarsening, with coarsened_defect(0) equal to the ledger defect. The defect functional coincides with J for positive arguments, and DefectBoundedSubLedger supplies an a-priori bound on total defect. The module setting is the RS counterpart of classical Hodge theory on compact Kähler manifolds, where every cohomology class possesses a unique L²-minimizing harmonic representative; here this becomes a unique J-cost minimal cycle for each stable class.
proof idea
The term proof first calls defect_budget_theorem on L, cls and the universal stability hypothesis to obtain that the Z-charge of cls is zero. It then applies harmonic_form_theorem_zero_charge directly to L, cls and this zero-charge datum to extract the required JCostMinimalCycle.
why it matters
This theorem assembles the hard direction of the Hodge conjecture analog under the assumption that all flows are stable, feeding directly into hard_direction_for_zero_limit_ledger and the HarmonicFormsCert certificate. It completes the passage from flow stability to existence of a minimal-cycle generator, consistent with J-uniqueness and the phi-ladder structure of the broader framework. No scaffolding remains open at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.