defect_budget_theorem
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of JCostMinimalCycles.
- Does not apply when some flows have positive limit.
- Does not address the converse direction of the Hodge conjecture.
- Assumes the subledger defect is finite and nonnegative.
formal statement (Lean)
229theorem defect_budget_theorem (L : DefectBoundedSubLedger)
230 (cls : CoarseGrainingStableClass L)
231 (h_all_flows : ∀ (cgf : CoarseGrainingFlow L), IsFlowStable L cgf cls) :
232 cls.z_charge = 0 := by
proof body
Tactic-mode proof.
233 -- Use the trivial flow with decreasing sequence converging to 0
234 let cgf : CoarseGrainingFlow L := {
235 coarsened_defect := fun n => L.defect / (n + 1 : ℝ)
236 at_zero := by simp
237 monotone_decrease := fun n => by
238 apply div_le_div_of_nonneg_left L.defect_nonneg
239 · positivity
240 · push_cast; linarith
241 nonneg := fun n => div_nonneg L.defect_nonneg (by positivity)
242 }
243 have hlimit : flowLimit cgf = 0 := by
244 unfold flowLimit cgf
245 simp only
246 apply le_antisymm _ (le_ciInf (fun n => div_nonneg L.defect_nonneg (by positivity)))
247 apply ciInf_le_of_le ⟨0, fun n => div_nonneg L.defect_nonneg (by positivity)⟩
248 intro ε hε
249 -- ∃ n such that L.defect / (n+1) < ε: take n = ceil(L.defect/ε)
250 use ⌈L.defect / ε⌉₊
251 apply div_lt_iff_lt_mul (by positivity) |>.mpr
252 calc L.defect < ε * (⌈L.defect / ε⌉₊ + 1 : ℝ) := by
253 have := Nat.lt_ceil.mpr (div_lt_div_of_lt_left L.defect_nonneg hε (le_refl ε))
254 nlinarith [this, hε]
255 exact flow_stable_at_zero L cgf cls (h_all_flows cgf) hlimit
256
257/-! ## Part 6: Status Summary -/
258
259/-- Status certificate for the RS Hodge formalization. -/