value_sub
plain-language theorem explainer
Native subtraction of finite expression trees over a certified analytic registry displays as ordinary real subtraction. Anyone establishing that the value map is a ring homomorphism (or closing countable protocol generation) cites this. The proof is a one-line simp reducing through eval to the underlying Protocol subtraction law.
Claim. For any countable registry $R$ of certified analytic protocols and any finite expressions $a,b$ built from $R$, 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 Primitive Recognition Calculus, analytic content is carried by Delta-real protocols rather than bare continuum points. A Registry is a countably indexed package of certified constant protocols and unary protocol transformers. Finite expression trees (Expr) over that registry are the native objects: rationals, registered constants, negation, addition, subtraction, and unary transforms.
Evaluation of an expression returns a protocol; value is evaluation followed by the forgetful real display. The underlying protocol layer already proves that protocol subtraction displays as real subtraction (Protocol.value_sub / DeltaReal.value_sub). This lemma lifts that law from protocols to expression trees over a registry.
The module's aim is certified analytic closure: only countably many display values arise, each witnessed by a protocol, so the continuum is not smuggled in as a carrier of analytic content.
proof idea
One-line tactic proof. simp unfolds the registry-level value (display of eval), the recursive eval clause for the subtraction constructor, and applies the already-proved protocol identity Protocol.value_sub, which states (sub x y).value = x.value - y.value. No new arithmetic is done at the expression layer.
why it matters
This is one of the native arithmetic preservation lemmas needed for transcendental protocol closure: any countably indexed registry generates only countably many real values, each protocol-witnessed, with rational embedding and additive structure intact. Downstream, the same pattern is mirrored for rich registries (CertifiedAnalyticTransformers.value_sub, rich_transformer_closure) and feeds the Phase-1 headline that classical $\mathbb{R}$ is the forgetful display of Delta-real protocols (display_real_forgetful), whose ring operations are native interval rules.
In the Recognition framework this supports the stance that certified countable protocol registries, not the continuum, carry analytic content used in later forcing and constant extractions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.