hodgeHardCert
plain-language theorem explainer
The declaration certifies the hard direction of the RS Hodge conjecture for zero-flow-limit ledgers and for unit-defect ledgers. Researchers working on the Recognition Science reformulation of the classical Hodge conjecture would cite it when assembling special-case proofs. The proof is a direct term-mode instantiation that supplies the two supporting theorems as structure fields and discharges the remaining field by trivial.
Claim. Let $L$ be a DefectBoundedSubLedger. If every CoarseGrainingFlow on $L$ has flowLimit equal to zero, then for every CoarseGrainingStableClass $cls$ on $L$ there exists a list of JCostMinimalCycles whose z-charges sum to $cls.z_charge$. If instead $L.defect ≤ 1$, the same decomposition exists for every such $cls$.
background
Recognition Science recasts the Hodge conjecture in ledger language: every CoarseGrainingStableClass must be generated by JCostMinimalCycles. A DefectBoundedSubLedger carries a bounded total defect; CoarseGrainingFlow tracks its coarse-graining evolution; flowLimit records the asymptotic value of that evolution; z_charge measures the net charge of a stable class or cycle. JCostMinimalCycle is the cycle of minimal J-cost within its class. The module documentation states that the hard direction (every stable class is generated by minimal cycles) is proved under two restrictions: the zero-limit case and the unit-defect case.
proof idea
The proof is a term-mode construction of the HodgeHardCert structure. It directly assigns rs_hodge_holds_for_trivial_ledgers to the case_A field and rs_hodge_holds_for_unit_defect to the case_B field. The both_directions field is discharged by the trivial tactic.
why it matters
This declaration assembles the two proved cases into the single HodgeHardCert structure required by the hard-direction statement of the RS Hodge conjecture. It therefore supplies the concrete content for the module's proof chain and closes the special-case assembly before the general positive-z_charge extension is addressed in HodgeConjecture.lean. The RS framework treats defect budget as the analog of energy minimization, paralleling the role of harmonic forms in the classical setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.