width
plain-language theorem explainer
The width of a closed rational interval is the difference of its upper and lower endpoints. Anyone working with nested rational approximations (protocols) in the primitive recognition calculus cites this as the basic size measure. The definition is a one-line subtraction on the endpoint fields.
Claim. For a closed rational interval $I = [\ell, h]$ with $\ell \le h$, the width is $\mathrm{width}(I) := h - \ell \in \mathbb{Q}$.
background
In the primitive recognition calculus, real numbers are presented by protocols: nested sequences of closed rational intervals whose widths shrink at a controlled rate. The carrier type is RatInterval, a structure with rational endpoints lo, hi and a proof lo ≤ hi.
Width is the elementary size functional on that carrier. It is the rational analogue of the real interval width used in the certification layer (I.hi - I.lo on real intervals). Downstream arithmetic on protocols (addition, negation, constant embeddings) repeatedly unfolds this definition to discharge width bounds of the form width(approx n) ≤ 1/(n+1).
The local module builds a constructive real type from these nested rational intervals; width is the first scalar invariant attached to each stage of the approximation.
proof idea
Pure definitional abbreviation: subtract the lower rational endpoint from the upper. No lemmas, no tactics. Call sites typically unfold RatInterval.width (or rely on simp) and then cancel or bound the resulting difference.
why it matters
Width is the size measure that makes the protocol construction work. Constant rational protocols have width zero at every precision (ofRat); addition reads operands at doubled precision so the summed widths still meet the 1/(n+1) budget; negation merely swaps and signs endpoints, preserving width. Overlap and nestedness arguments compare widths to decide when two approximations can still represent the same real.
Those arithmetic lemmas feed the whole DeltaReal stack. Outside the foundation layer the same name appears in certification and in band-consistency checks (e.g. Hubble-tension falsifiers that compare a measurement offset to band width), so the concept is reused wherever RS states a quantitative tolerance. It is scaffolding infrastructure rather than a forcing-chain step (T0–T8), but every constructive real identity in the monolith ultimately rests on controlling this quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.