Foundation Primitive Recognition Calculus Certified Analytic Protocols Transcend

The countable registry

In mathematics, a countable set is one whose elements can be listed, even if the list never ends. The rational numbers are countable; the real numbers are not. A theorem in the Recognition Science framework's machine-checked library of formal theorems shows that a certain kind of analytic expression can only ever produce countably many real values. The theorem is called transcendental_protocol_closure, and it is a statement about what a registry of certified analytic protocols can generate.

The framework models a registry, a discrete record of events, as a countable list of constants and unary transformers. From this registry, finite expression trees are built: rational numbers, registered constants, negation, addition, subtraction, and unary transforms. Each expression evaluates to a protocol, and each protocol displays a real value. The theorem proves that the set of all such values is countable, and that every value in that set has a protocol witness, meaning a concrete protocol whose displayed value equals the given real number.

The proof is direct. Expressions are finite trees over countable labels, so there are only countably many expressions. The set of values is the range of a function from expressions to reals, and the range of a function from a countable set is countable. This is the countability fact that blocks what the framework calls continuum smuggling, the illicit import of uncountable structure through analytic operations.

The theorem also preserves the native arithmetic operations. Rational literals evaluate to their rational values; addition, negation, and subtraction of expressions evaluate to the corresponding operations on real values. These are simple lemmas, but they close the loop: the countable registry is closed under the basic operations that matter.

In Recognition Science, the theorem supports the claim that the continuum is not the carrier of analytic content. A certified countable protocol registry is. The practical consequence is that any analytic object built from the registry can be inspected, computed, and reasoned about finitely, without invoking an uncountable background.

/-- 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)

/-- 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⟩

/-- Rational literals evaluate to their rational values. -/
@[simp] theorem value_rat (R : Registry) (q : ℚ) :
    value R (.rat q) = (q : ℝ) := by
  simp [value, eval, Protocol.value_ofRat]

/-- Native addition remains addition under the value display. -/
theorem value_add (R : Registry) (a b : Expr) :
    value R (.add a b) = value R a + value R b := by
  simp [value, eval, Protocol.value_add]

/-- Native negation remains negation under the value display. -/
theorem value_neg (R : Registry) (a : Expr) :
    value R (.neg a) = - value R a := by
  simp [value, eval, Protocol.value_neg]

/-- Native subtraction remains subtraction under the value display. -/
theorem value_sub (R : Registry) (a b : Expr) :
    value R (.sub a b) = value R a - value R b := by
  simp [value, eval, Protocol.value_sub]

What this page does not claim

The theorem does not claim that all real numbers are generated by any registry. It does not claim that the registry itself is unique or that its constants are derived. It does not claim that the continuum is eliminated from the framework, only that it is not the carrier of analytic content.

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: