sub
plain-language theorem explainer
Subtraction on Delta-reals is defined by adding the additive inverse: x − y := x + (−y). Anyone building arithmetic on nested rational-interval protocols cites this. The body is a one-line abbreviation through the existing add and neg operations on Protocol.
Claim. For Delta-real protocols $x$ and $y$ (nested rational-interval families with width at most $1/(n+1)$ at precision $n$), define subtraction by $x - y := x + (-y)$, where $-y$ is the pointwise interval negation of $y$.
background
A Protocol (Delta-real) is a nested family of rational intervals approx : ℕ → RatInterval with approx(n+1) ⊆ approx(n) and width bound width(approx n) ≤ 1/(n+1). The intended real is the unique point in the intersection of all intervals.
Negation of a protocol flips each interval: if approx n = [a,b] then (-x).approx n = [-b,-a], preserving nesting and the width bound. Interval negation itself is the standard map [a,b] ↦ [-b,-a] from the numerics layer; the same pattern appears for logic integers and rationals upstream.
This module builds a constructive real arithmetic layer for the primitive recognition calculus, so the four field operations on protocols are introduced as structure-preserving maps on the approximating intervals.
proof idea
Pure definitional abbreviation: sub x y is definitionally add x (neg y). No proof obligations are discharged here; well-formedness of the result inherits from the already-constructed add and neg on Protocol.
why it matters
Completes the additive group operations on Delta-reals alongside addition and negation, so differences of recognition-derived quantities can be formed inside the nested-interval model. No downstream uses are recorded yet in the graph; the natural consumers are later lemmas on linearity, continuity of arithmetic, and comparison of protocols. In the Recognition foundation this is scaffolding for real-valued observables (costs, defects, ladder coordinates) rather than a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.