flowLimit_nonneg
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.