width
plain-language theorem explainer
The width function returns the length of a closed real interval by subtracting its lower endpoint from its upper endpoint. Certification and interval-arithmetic arguments in Recognition Science cite this definition when bounding differences inside intervals, for example in symmetry proofs or rung-gap calculations. The definition is a direct one-line field subtraction with no auxiliary lemmas.
Claim. For a closed interval $I$ with real endpoints satisfying $lo_I ≤ hi_I$, the width is $hi_I - lo_I$.
background
The Interval structure is a closed interval on the reals whose fields are lo, hi and the proof lo ≤ hi. This local Interval differs from the rational-endpoint version in Numerics.Interval.Basic and from the spacetime interval defined in Unification.SpacetimeEmergence. The definition sits inside the Certification module that supplies interval primitives for Recognition Science proofs.
proof idea
The declaration is a direct definition that performs the subtraction I.hi - I.lo. No lemmas or tactics are invoked; it is the primitive operation that extracts interval length from the structure.
why it matters
Width supplies the basic length measure used by thirty downstream declarations, including pleasure_symmetric (Aesthetics), two_rung_gap_eq_phi_squared (Astrophysics), ferromagnet_positive_J (Chemistry) and the SAT-gadget encodings (Complexity). It therefore underpins interval bounds required for J-cost symmetry, phi-ladder rung gaps and the Recognition Composition Law applications that appear in the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.