Protocol
plain-language theorem explainer
A Delta-real is a nested sequence of closed rational intervals whose widths shrink at least as fast as 1/(n+1). The unique real in the total intersection is the intended value. Anyone building certified analytic expressions, registries, or measurement carriers in the Primitive Recognition Calculus cites this structure. It is pure data: three fields packaging the approximation map with nesting and width axioms.
Claim. A protocol is a map $n \mapsto I_n$ from naturals to closed rational intervals such that $I_{n+1} \subseteq I_n$ for every $n$ and $\mathrm{width}(I_n) \le 1/(n+1)$. The intended quantity is the unique real lying in every $I_n$.
background
This module builds reals constructively from rational data rather than as a completed continuum. A closed rational interval is a pair of rationals $(\ell,h)$ with $\ell \le h$; its width is $h-\ell$. Interval inclusion $I \subseteq J$ means $J$ contains both endpoints of $I$.
A protocol packages a precision-indexed family of such intervals. Nesting forces the sequence to be decreasing under inclusion. The width bound $1/(n+1)$ forces diameters to zero, so the intersection is a singleton real. That real is the value the protocol certifies.
The local setting is the Primitive Recognition Calculus foundation: analytic content is carried by countable certified protocols, not by uncountable graphs of reals. Related width notions appear in certification intervals elsewhere in the stack, but here width is strictly rational.
proof idea
Structure definition with empty proof body. Three fields: an approximation map $\mathbb{N}\to$ rational intervals, a nesting axiom (each successor interval is a subset of the previous), and a uniform width bound $\mathrm{width}(I_n)\le 1/(n+1)$. No lemmas are applied; the axioms are the content.
why it matters
This is the carrier type for Delta-reals in the foundation layer. Downstream, certified analytic evaluation maps finite expression trees over a registry to protocols (eval), and every registry value is witnessed by some protocol (every_value_has_protocol). Transcendental protocol closure then records that any countable registry of certified constants and transformers yields only countably many reals, each protocol-witnessed: the continuum is not the analytic carrier; a countable protocol registry is.
Native arithmetic on protocols (add, neg, rational literals) preserves displayed values, so the structure underwrites additive closure of certified content. Measurement-mechanism material also references protocols when stating pre-measurement uncoupling. In the broader Recognition stack this keeps analytic and measurement objects countable and certificate-friendly, aligned with constructive extraction rather than classical continuum primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.