rs_hodge_holds_for_unit_defect
plain-language theorem explainer
The theorem establishes that every coarse-graining stable class on a defect-bounded sub-ledger with defect at most one decomposes into a finite list of J-cost minimal cycles whose z-charges sum exactly to the class z-charge. Researchers working on the Recognition Science formulation of the Hodge conjecture cite this as the verified special case for unit-defect ledgers. The proof is a one-line wrapper that delegates directly to the already-established case-B lemma for such ledgers.
Claim. For every defect-bounded sub-ledger $L$ satisfying defect$(L) ≤ 1$ and every coarse-graining stable class cls on $L$, there exists a finite list of J-cost minimal cycles on $L$ such that the z-charge of cls equals the sum of the z-charges of those cycles.
background
DefectBoundedSubLedger supplies the ambient ledger whose defect functional (equal to the J-cost) is bounded above. CoarseGrainingStableClass extends a cohomology class by the stability condition dpi_stable : z_charge ≤ L.defect, ensuring the class survives coarse-graining flow. JCostMinimalCycle is a recognition-closed subgraph with zero net defect, serving as the RS counterpart to an algebraic cycle in the classical Hodge setting. The module assembles the hard direction of the RS Hodge Conjecture under two explicit conditions: case A for zero-limit ledgers and case B for defect ≤ 1 ledgers.
proof idea
The proof is a one-line wrapper that applies the case-B lemma hodge_hard_direction_case_B to the ledger L, the defect bound hypothesis, and the stable class cls.
why it matters
This supplies case B inside the HodgeHardCert certificate and the hodge_hard_direction_summary. It verifies the decomposition claim of the RS Hodge Conjecture when the defect budget is at most one, where the minimization constraint plays the role that harmonic forms play classically. The remaining gap for z_charge > 1 without the unit-defect restriction is left open and requires extension to rational combinations of cycles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.