hard_direction_for_zero_limit_ledger
plain-language theorem explainer
Under the hypothesis that all coarse-graining flows on a defect-bounded sub-ledger converge to zero, every coarse-graining stable class is realized by a J-cost minimal cycle. Researchers developing the Recognition Science analog of the Hodge conjecture cite this for the vanishing-defect case. The proof is a one-line wrapper that applies the general hard direction via defect budget after verifying flow stability from the zero-limit hypothesis.
Claim. Let $L$ be a defect-bounded sub-ledger. Assume that for every coarse-graining flow on $L$ the flow limit equals zero. Let $cls$ be a coarse-graining stable class on $L$. Then there exists a J-cost minimal cycle $cyc$ on $L$ such that the $z$-charge of the cycle class of $cyc$ equals the $z$-charge of $cls$.
background
In Recognition Science a DefectBoundedSubLedger is a finite collection of recognition events carrying finite total J-cost (the defect), serving as the analog of a smooth projective variety. A CoarseGrainingFlow on such an $L$ records the monotone decrease of apparent defect under successive coarse-graining steps; its flowLimit is the infimum of the coarsened defects and is the RS counterpart of the heat flow in classical Hodge theory. A CoarseGrainingStableClass extends a cohomology class by the condition that its $z$-charge survives the data-processing inequality, i.e., remains anchored to the underlying J-cost structure even after arbitrary zooming out.
proof idea
The proof is a one-line wrapper that applies hard_direction_via_defect_budget to $L$ and $cls$. It then introduces an arbitrary coarse-graining flow, unfolds the IsFlowStable predicate, rewrites the flowLimit to zero using the given hypothesis, and closes with the symmetric property of the stable class.
why it matters
This supplies the hard direction of the RS Hodge conjecture precisely when flows converge to zero defect, feeding the assembly of HarmonicFormTheorem and HodgeDecomposition in the same module. It rests on the upstream structures CoarseGrainingFlow, CoarseGrainingStableClass, and JCostMinimalCycle from the HodgeConjecture module, which translate algebraic cycles to zero-net-defect recognition subgraphs. Within the framework it aligns with J-uniqueness (T5) and the requirement that harmonic (J-cost critical) representatives exist for each cohomology class once persistent defects vanish.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.