flow_stable_at_zero
plain-language theorem explainer
A coarse-graining stable class on a defect-bounded sub-ledger has vanishing z-charge when the flow limit is zero. Researchers formalizing the Recognition Science Hodge conjecture cite this to anchor stable classes at genuine cost minima. The proof substitutes the zero limit into the stability inequality and applies antisymmetry of the charge order.
Claim. If a cohomology class $cls$ on a defect-bounded sub-ledger $L$ satisfies $z_{charge} ≤ flowLimit(cgf)$ under a coarse-graining flow $cgf$ with $flowLimit(cgf)=0$, then $cls.z_{charge}=0$.
background
The module translates the classical Hodge conjecture into Recognition Science: a DefectBoundedSubLedger is a finite set of recognition events with total J-cost (defect) bounded by $phi^{44}$, serving as the analog of a smooth projective variety. A CoarseGrainingFlow is a monotone decreasing sequence of apparent defects at successive scales, with the limit modeling infinite coarse-graining. A CoarseGrainingStableClass extends a cohomology class by the condition that its z-charge survives data-processing inequality, i.e., $z_{charge} ≤ L.defect$ and, via IsFlowStable, $z_{charge} ≤ flowLimit(cgf)$.
proof idea
Term-mode proof. Rewrite the IsFlowStable hypothesis with the assumption flowLimit(cgf)=0 to obtain z_charge ≤ 0. Apply le_antisymm from ArithmeticFromLogic to this inequality together with the symmetric bound supplied by the CoarseGrainingStableClass structure.
why it matters
This result is invoked by defect_budget_theorem to conclude that any class stable under every coarse-graining flow has z_charge=0. It supplies the zero-limit case in the defect-budget bridge of the module documentation, showing that surviving classes must be anchored to J-cost minima and thereby supporting the RS claim that coarse-graining-stable classes coincide with algebraic cycles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.