Foundation Primitive Recognition Calculus Certified Analytic Protocols Every Val

The protocol witness

In mathematics, a set of numbers is often described by a rule, but the rule may not tell you how to produce any particular member. The declaration every_value_has_protocol closes that gap for a specific kind of registry. A registry here is a countable list of constant protocols and unary protocol transformers, where a protocol is a discrete, step-by-step recipe for producing a real number. The declaration states that if a real number belongs to the set of values generated by such a registry, then there exists a protocol whose value is exactly that number. The proof is immediate: membership in the value set is defined by the existence of a finite expression tree, and evaluating that tree yields the protocol.

The deeper content is a countability result. A registry's expressions are finite trees built from rational literals, registered constants, negation, addition, subtraction, and unary transformers. Because the labels are countable, the set of all such expressions is countable, and therefore the set of values they produce is countable. This is the fact that blocks what the framework calls continuum smuggling: the idea that a countable registry could secretly generate an uncountable collection of numbers. The theorem transcendental_protocol_closure packages this: the value set is countable, every value has a protocol witness, and the basic arithmetic operations behave as expected under evaluation.

In Recognition Science, this declaration is a structural guarantee about the ledger. The ledger, a discrete record of recognition events, only ever needs to name countably many numbers, and each named number comes with a recipe. The framework's library, a machine-checked collection of formal theorems, proves this for any registry one can define. The practical consequence is that the framework never has to appeal to an uncountable continuum as a source of analytic content; a certified countable registry is enough.

What the declaration does not claim: it does not say every real number has a protocol, only every number in a registry's value set. It does not say the protocol is efficient, or that the registry is complete, or that any particular transcendental constant like π or e is included. It is a statement about the relationship between a value and its witness, not about which values exist. The countability theorem is the load-bearing part, and the witness theorem is a direct consequence of how membership is defined.

/-- Every registry value has a protocol witness, by construction. -/
theorem every_value_has_protocol (R : Registry) (x : ℝ) (hx : x ∈ values R) :
    ∃ p : Protocol, p.value = x := by
  rcases hx with ⟨e, rfl⟩
  exact ⟨eval R e, rfl⟩

/-- Registry values are countable because expressions are finite trees over
countable labels. This is the countability fact that blocks continuum smuggling. -/
theorem values_countable (R : Registry) : (values R).Countable :=
  Set.countable_range (value R)

/-- **Transcendental protocol closure.** Any countably indexed registry of certified
analytic constants and protocol transformers generates only countably many real
values, and every value is witnessed by a Delta-real protocol. The continuum is not
the carrier of analytic content; a certified countable protocol registry is. -/
theorem transcendental_protocol_closure (R : Registry) :
    (values R).Countable
      ∧ (∀ x : ℝ, x ∈ values R → ∃ p : Protocol, p.value = x)
      ∧ (∀ q : ℚ, value R (.rat q) = (q : ℝ))
      ∧ (∀ a b : Expr, value R (.add a b) = value R a + value R b)
      ∧ (∀ a : Expr, value R (.neg a) = - value R a)
      ∧ (∀ a b : Expr, value R (.sub a b) = value R a - value R b) :=
  ⟨values_countable R, every_value_has_protocol R, value_rat R, value_add R,
    value_neg R, value_sub R⟩

What this page does not claim

Not every real number has a protocol, only those in a registry's value set. The registry is not claimed to be complete or to include any specific transcendental constant. The declaration says nothing about the efficiency or computability cost of the protocol witness.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/CertifiedAnalyticProtocols.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: