sub
plain-language theorem explainer
This definition supplies subtraction for closed rational intervals by the rule [a,b] minus [c,d] equals [a-d, b-c]. Code that propagates bounds through differences in the Recognition Science numerics layer cites it when enclosing J-costs or phi-ladder quantities. The body is a direct structure literal whose sole proof obligation is discharged by a single linarith call on the two input validity hypotheses.
Claim. Let $I=[a,b]$ and $J=[c,d]$ be closed intervals with rational endpoints satisfying $a≤b$ and $c≤d$. Their difference is the interval whose lower endpoint is $a-d$, upper endpoint is $b-c$, and whose validity follows from the ordering of the four rationals.
background
The module implements verified interval arithmetic over the rationals so that bounds on real or transcendental expressions remain machine-checkable. The central structure Interval consists of a lower rational, an upper rational, and a proof that the lower does not exceed the upper. Subtraction is one of the primitive operations (with addition and negation) that allow bounds to be propagated through composite expressions without loss of rigor.
proof idea
The definition constructs a fresh Interval record by setting the lower field to I.lo minus J.hi and the upper field to I.hi minus J.lo. The validity field is filled by the linarith tactic applied to the two input hypotheses I.valid and J.valid, which rearranges the inequalities to obtain the required lower ≤ upper relation.
why it matters
The operation appears in forty downstream sites, among them the convexity theorem for the J-action on admissible paths, the proof that the golden-division ratio is less than one, and bounds on pulsar bimodal ratios and noble-gas atomic numbers. It therefore forms part of the certified arithmetic layer that supports the Recognition Science forcing chain and the enclosure of constants such as alpha inverse. The definition closes a basic gap in the numerics scaffolding required for phi-ladder calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.