defect_budget_theorem
plain-language theorem explainer
If a coarse-graining stable class on a defect-bounded subledger survives every flow, including those whose defect limit is zero, then its z_charge vanishes. Researchers formalizing the RS version of the Hodge conjecture cite this to close the zero-cost case before invoking minimal-cycle generation. The proof builds one explicit flow with coarsened defect L.defect/(n+1), proves its limit is zero via ciInf and le_antisymm, then applies the stability-at-zero lemma.
Claim. Let $L$ be a defect-bounded subledger and let cls be a coarse-graining stable class on $L$. If cls.z_charge is at most the limit of the coarsened defect for every coarse-graining flow on $L$, then cls.z_charge = 0.
background
A DefectBoundedSubLedger is a finite list of recognition events whose total J-cost (defect) is nonnegative and bounded above by phi^44. A CoarseGrainingStableClass on such an L extends a cohomology class by the condition that its z_charge satisfies the data-processing inequality z_charge ≤ L.defect. A CoarseGrainingFlow on L is a monotone nonincreasing sequence of apparent defects starting at L.defect; IsFlowStable(L, cgf, cls) asserts that cls.z_charge ≤ flowLimit(cgf).
proof idea
The tactic proof constructs an explicit CoarseGrainingFlow whose coarsened_defect(n) equals L.defect/(n+1). It verifies monotonicity and nonnegativity by div_le_div_of_nonneg_left and positivity, then shows flowLimit equals zero by le_antisymm applied to the ciInf definition together with an explicit n = ceil(L.defect/ε) argument. The final step is the one-line application of flow_stable_at_zero to the stability hypothesis and the zero limit.
why it matters
This result supplies the defect-budget step used by hodge_hard_direction_case_A and hard_direction_via_defect_budget in the HodgeHardDirection and HodgeHarmonicForms modules. It realizes the bridge described in the module doc: any class that survives all coarse-grainings must sit at a genuine cost minimum. The theorem therefore advances the hard direction of the RS Hodge conjecture while remaining inside the proved half of the formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.