annularCost_nonneg
plain-language theorem explainer
Annular cost is nonnegative for every natural number N and every annular mesh of that size. Researchers deriving collapse scalars from realized defects cite this to guarantee the scalar stays positive. The proof is a direct transitivity step that chains the nonnegativity of the topological floor to the inequality relating the floor to the full annular cost.
Claim. For every natural number $N$ and every annular mesh $m$ of size $N$, the total annular cost satisfies $0$ ≤ annular cost of $m$.
background
The Unified RH module replaces an earlier bounded-total-cost assertion with a three-component T1-bounded realizability architecture: cost divergence for nonzero-charge sensors, Euler trace admissibility, and physically realizable ledgers carrying bounded T1 defects. Annular cost is the accumulated defect functional over the annular mesh; the defect equals the J-cost on positive ratios, where J is the multiplicative recognizer comparator. AnnularMesh N encodes a sensor charge together with a discretization level N drawn from the multiplicative recognizer structure.
proof idea
One-line term proof that applies order transitivity to the nonnegativity of the annular topological floor at the mesh charge and the comparison lemma showing the floor is at most the annular cost.
why it matters
This supplies the nonnegativity step required by realizedDefectCollapseScalar_pos and realizedDefectCollapseBoundaryApproaching_of_nonzero_charge. It anchors the cost-divergence component of the T1 architecture, ensuring the collapse scalar 1/(1 + annular cost) is well-defined and positive before the boundary approach is invoked. The result aligns with the Recognition Science forcing chain by grounding defect accumulation on the phi-ladder without assuming global boundedness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.