value_sub
plain-language theorem explainer
Subtraction of rich certified-analytic expressions displays as ordinary real subtraction. Anyone proving ring-homomorphism or closure facts for RichRegistry values cites this. The proof is a one-line simp reducing through eval to the native Protocol subtraction law.
Claim. For any rich registry $R$ and any finite rich expressions $a,b$, the displayed real value of the subtraction node equals the difference of the displayed values: $\mathrm{val}_R(a-b)=\mathrm{val}_R(a)-\mathrm{val}_R(b)$.
background
In the certified-analytic layer, a Protocol is a Delta-real witness whose forgetful display is a classical real. A RichRegistry packages countably many constant protocols together with unary and binary protocol transformers. RichExpr is the free finite expression language over that registry: rationals, constants, negation, addition, subtraction, and the unary/binary transformer applications.
The map value evaluates an expression to a Protocol then takes its real display. The thinner Registry/Expr stack already records that native subtraction remains subtraction under display. This lemma is the same identity lifted to the richer expression type that admits binary transformers.
Local setting: CertifiedAnalyticTransformers builds the rich closure theorem that binary and unary transformers still generate only countably many display values, each protocol-witnessed, blocking continuum smuggling of analytic content.
proof idea
One-line simp proof. Unfold the rich value (eval then Protocol.value) and the recursive eval clause for the subtraction constructor; the goal reduces exactly to Protocol.value_sub, the native law $(x-y).\mathrm{value}=x.\mathrm{value}-y.\mathrm{value}$ already proved on Delta-real protocols.
why it matters
Feeds rich_transformer_closure, the rich analogue of transcendental protocol closure: countability of the value set plus rational embedding and ring-homomorphism identities for add/neg (and, via this lemma, sub). Downstream DeltaReal consumers (display_real_forgetful, value_surjective, protocol-level value_sub) treat classical $\mathbb{R}$ as the forgetful display of a countable protocol carrier; preserving subtraction under display is part of that ring-faithfulness story.
In the Recognition foundation this keeps analytic content inside certified countable registries rather than bare continuum carriers, consistent with the broader program that physical constants and ladder quantities arise from discrete recognition structure (phi-ladder, eight-tick octave) rather than uncountable smuggling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.