flowLimit_nonneg
flowLimit_nonneg establishes that the infimum of the coarsened defect sequence for any CoarseGrainingFlow is nonnegative. Researchers formalizing the RS Hodge conjecture cite it to guarantee that limiting charge measures remain valid lower bounds. The argument is a direct one-line application of the infimum property to the nonnegativity field inside the flow structure.
claimLet $cgf$ be a coarse-graining flow on a defect-bounded sub-ledger $L$. Then $0 ≤ inf_{n∈ℕ} coarsened_defect(n)$, where $coarsened_defect$ is the sequence of apparent defects at successive scales.
background
CoarseGrainingFlow is a structure on a DefectBoundedSubLedger consisting of a map coarsened_defect : ℕ → ℝ together with three fields: at_zero (equals L.defect at scale 0), monotone_decrease (each step weakly lowers the value), and nonneg (every term ≥ 0). The module translates the classical Hodge conjecture by identifying varieties with defect-bounded sub-ledgers, Hodge classes with coarse-graining-stable classes, and algebraic cycles with J-cost-minimal cycles. Upstream results supply the active-edge count A = 1 and the collision-free property used to anchor defect calculations.
proof idea
The proof is a one-line term that applies le_ciInf to the function sending each n to the nonnegativity witness cgf.nonneg n. This directly yields that the greatest lower bound of a family of nonnegative reals is itself nonnegative.
why it matters in Recognition Science
The result supplies the nonnegativity anchor required for the definition of coarse-graining stability (z_charge ≤ flowLimit) and thereby supports the proved direction of the RS Hodge conjecture that every JCostMinimalCycle is a CoarseGrainingStableClass. It fits the defect-budget bridge described in the module documentation and aligns with the T5–T8 forcing chain that fixes D = 3 and the phi-ladder scaling of defects.
scope and limits
- Does not prove that the flow limit is strictly positive.
- Does not compute explicit numerical values for any concrete sub-ledger.
- Does not establish convergence of the coarsened_defect sequence.
- Does not invoke the specific constants phi or alpha.
formal statement (Lean)
211theorem flowLimit_nonneg (cgf : CoarseGrainingFlow L) : 0 ≤ flowLimit cgf :=
proof body
Term-mode proof.
212 le_ciInf (fun n => cgf.nonneg n)
213
214/-- A class is **coarse-graining stable** if its z_charge survives even the
215 infinitely coarsened limit: z_charge ≤ flowLimit. -/