width_nonneg
plain-language theorem explainer
For any closed rational interval, the width (upper minus lower endpoint) is nonnegative. Interval and band constructions in the Recognition stack cite this as the basic positivity fact on rational widths. The proof is a one-line linear-arithmetic step from the interval's built-in endpoint ordering.
Claim. For every closed rational interval $I=[\ell,h]$ with $\ell\le h$, one has $0\le h-\ell$.
background
In the primitive recognition calculus, a closed rational interval is a pair of rationals $\ell\le h$ packaged with that ordering witness. Its width is the rational difference $h-\ell$.
The module builds a minimal real-from-rationals layer for recognition protocols: intervals, containment, overlap, and monotone endpoint maps. Width is the first derived quantity; nonnegativity is the first structural lemma.
Upstream, the ordering on the endpoints is the standard rational order (internally tied to the signed-orbit and logic-nat orders used elsewhere in the foundation). Certification and numerics layers use an analogous real width $h-\ell$ on floating intervals; this lemma is the rational counterpart.
proof idea
Term-mode proof in three micro-steps: pull the structure field $\ell\le h$, unfold width to $h-\ell$, then discharge $0\le h-\ell$ by linarith. No external lemmas beyond the interval's own ordering witness.
why it matters
Gives the positivity invariant every later width argument needs. Downstream, the RecogSpec band type defines real bands with the same $h-\ell$ width; rational interval widths feed certified band constructions and containment checks in the recognition specification layer.
In the foundation stack this sits under PrimitiveRecognitionCalculus before forcing-chain physics (T5–T8, RCL, phi-ladder). It is bookkeeping, not a physical claim, but without it band and protocol lemmas cannot state that widths are nonnegative measures of uncertainty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.