value_sub
plain-language theorem explainer
Native subtraction of Delta-real protocols is compatible with the forgetful real display: the value of the difference equals the difference of the values. Anyone assembling the protocol ring laws or the Phase-1 forgetful map to classical ℝ cites this. The proof unfolds subtraction as addition of a negation, then reduces by the add and neg value lemmas plus ring.
Claim. Let $x$ and $y$ be Delta-real protocols (nested rational-interval families with width bound $1/(n+1)$). Writing $x-y$ for the protocol obtained by the native interval subtraction rule, the displayed real values satisfy $(x-y)^{\mathrm{val}}=x^{\mathrm{val}}-y^{\mathrm{val}}$.
background
A Protocol (Delta-real) is a nested family of rational intervals approx : ℕ → RatInterval with width(approx n) ≤ 1/(n+1). The intended quantity is the unique real common to all intervals; value is that forgetful real display.
Protocol arithmetic is defined by interval rules. Subtraction is not primitive: it is addition of a negation. Upstream, value_add and value_neg already state that native addition and negation remain addition and negation under the display map. The same pattern is re-exported for expression registries in CertifiedAnalyticProtocols and CertifiedAnalyticTransformers, where value is evaluation followed by protocol display.
Local setting is the Primitive Recognition Calculus construction of ℝδ: classical reals appear only as the forgetful values of certified nested-interval protocols, not as a primitive continuum carrier.
proof idea
Term-style tactic proof, three steps. Unfold the definition of protocol subtraction (sub is add of neg). Rewrite the goal with the already-proved lemmas value_add and value_neg, obtaining an equality of the form x.value + (-y.value) = x.value - y.value. Close by ring on ℝ.
why it matters
Closes the subtraction leg of the protocol ring display laws. Downstream, CertifiedAnalyticProtocols.value_sub and CertifiedAnalyticTransformers.value_sub are one-line wrappers that simp through evaluation to this lemma; they feed transcendental_protocol_closure and rich_transformer_closure, which assert that countable certified-analytic registries generate only countably many reals, each protocol-witnessed, while preserving add/neg (and via this, sub).
In-module, it supports display_real_forgetful (Phase-1 headline: classical ℝ is the forgetful value of ℝδ, with native operations matching the ring) and the surrounding value_surjective / obsEq infrastructure. Framework role: keeps analytic content on countable protocol carriers rather than an uncountable continuum, consistent with the Recognition stance that display values are derived, not primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.