flowLimit
plain-language theorem explainer
flowLimit defines the asymptotic defect of any coarse-graining flow as the infimum of its monotone decreasing coarsened_defect sequence. Researchers formalizing the Recognition Science translation of the Hodge conjecture cite it when establishing stability of cohomology classes under data-processing inequalities. The definition is a direct one-line infimum construction over the sequence supplied by the CoarseGrainingFlow structure.
Claim. Let $L$ be a defect-bounded sub-ledger and $cgf$ a coarse-graining flow on $L$. The flow limit is defined as the infimum $inf_n cgf.coarsened_defect(n)$.
background
A CoarseGrainingFlow on a DefectBoundedSubLedger models repeated zooming out to larger voxels. Its fields require that coarsened_defect is a sequence in ℝ that is monotone decreasing, nonnegative, and equals the ledger defect at scale zero. This supplies the RS analog of heat flow or data-processing inequality in classical Hodge theory.
proof idea
One-line definition that applies the infimum operator directly to the coarsened_defect sequence of the input CoarseGrainingFlow.
why it matters
The definition is invoked by defect_budget_theorem to conclude that any class stable under all flows has zero charge, and by flow_stable_at_zero when the limit is zero. It anchors the asymptotic triviality hypothesis in HodgeHardDirection.hodge_hard_direction_case_A and the hard-direction certification structure. The module documentation identifies this limit as the key object in the defect-budget bridge for the RS Hodge conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.