transcendental_protocol_closure
plain-language theorem explainer
Any countably indexed registry of certified analytic constants and unary transformers generates only countably many real values, each witnessed by a Delta-real protocol, and the native rational, add, neg, and sub constructors evaluate as expected on the real display. Analysts building a countable carrier for transcendental content cite this package. The proof is a six-component term pairing the existing countability, witness, and homomorphism lemmas.
Claim. For every countable registry $R$ of certified analytic protocol ingredients, the set of real values generated by finite expressions over $R$ is countable; every such value is the display of some Delta-real protocol; rational literals evaluate to their embeddings in $\mathbb{R}$; and evaluation intertwines addition, negation, and subtraction with the corresponding real operations.
background
The module builds a certified analytic layer on top of Delta-real protocols. A Registry is a countable package: a sequence of constant protocols and a sequence of unary protocol transformers. Binary analytic operations beyond the native additive structure are deferred to unary transforms on paired protocols.
Finite expressions over a registry form an inductive tree with constructors for rationals, registered constants, negation, addition, subtraction, and registered unary transforms. Evaluation of an expression returns a protocol (never an uncountable graph); the real display of that protocol is the expression's value. The set of all such values is the analytic content generated by the registry.
Upstream, every registry value already has a protocol witness by construction (evaluate the witnessing expression). Separate lemmas record that rational literals, addition, and negation are preserved under the value display, using the corresponding Delta-real protocol identities.
proof idea
One-line term proof: the six conjuncts are exactly the six already-proved siblings values_countable, every_value_has_protocol, value_rat, value_add, value_neg, and value_sub, packaged as a single product. No new reasoning; the theorem is the closed surface those lemmas jointly form.
why it matters
This is the certified-analytic entry in the strong Delta-native closure certificate. Downstream, strongClosureCertificate plugs the theorem in as certifiedAnalytic, so any later argument that the analytic layer stays countable and protocol-witnessed cites this package rather than the six lemmas separately.
Philosophically it records the module's central claim: the continuum is not the carrier of analytic content; a certified countable protocol registry is. That stance fits the Recognition foundation's preference for countable, protocol-level carriers over bare real sets, and it keeps transcendental constants inside the same Delta-real witness discipline used for the rest of the primitive recognition calculus.
It does not itself force particular constants (phi, periods, etc.); it only certifies that whatever countable registry one installs remains closed under the native additive expression language with protocol witnesses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.