hodge_hard_direction_summary
plain-language theorem explainer
The theorem shows that every coarse-graining stable class on a defect-bounded sub-ledger decomposes into a list of J-cost minimal cycles when the coarse-graining flow limit is zero or when the ledger defect is at most one. A researcher assembling the Recognition Science version of the Hodge conjecture would cite this result to close the hard direction under those two restrictions. The proof is a direct term pairing of the trivial-ledger case with the unit-defect case.
Claim. For every defect-bounded sub-ledger $L$, if every coarse-graining flow on $L$ satisfies flow limit zero, then for every coarse-graining stable class $cls$ on $L$ there exists a list of J-cost minimal cycles whose z-charges sum to $cls.z_charge$. The same decomposition holds whenever the defect of $L$ is at most 1.
background
A DefectBoundedSubLedger is a finite list of recognition events whose total J-cost (defect) is finite; it plays the role of a smooth projective variety. A CoarseGrainingFlow equips such a ledger with a monotone decreasing sequence of coarsened defects whose value at scale zero recovers the ledger defect. A CoarseGrainingStableClass extends a cohomology class by the additional requirement that its z-charge is bounded by the ledger defect, enforcing stability under the data-processing inequality.
proof idea
The proof is a one-line term wrapper that directly pairs the theorem rs_hodge_holds_for_trivial_ledgers (covering the zero-limit case) with rs_hodge_holds_for_unit_defect (covering the defect ≤ 1 case). No additional tactics or reductions are performed.
why it matters
The declaration assembles the hard direction of the RS Hodge conjecture under the two special cases stated in the module documentation: zero flow limit and unit defect. It supplies the summary needed for the parent certificate HodgeHardCert and leaves the general case (z_charge > 1 without defect bound) for the extension to rational combinations in HodgeConjecture.lean. Within the Recognition Science framework it mirrors the classical Hodge decomposition via defect-budget minimization, while the remaining gap for unrestricted z_charge is explicitly flagged as requiring recursive cycle decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.