Foundation Primitive Recognition Calculus Certified Analytic Protocols Expr

The expression tree

In mathematics, an expression is a finite arrangement of symbols that stands for a value: 2 + 3, or x² - 1, or sin(π/4). The Recognition Science framework defines a particular kind of expression, called Expr, which is a finite tree built from rational numbers, registered constants, and a small set of operations: negation, addition, subtraction, and applying a registered unary transformer. The tree is the native object; evaluation turns it into a protocol, never into an uncountable graph. This is a definitional choice, a MODEL, not a theorem about the world.

The framework's library, a machine-checked collection of formal theorems, then proves what this definition delivers. The central result is transcendental_protocol_closure: for any countable registry of constants and transformers, the set of values generated by all finite expressions is countable, and every value is witnessed by a protocol. The proof is short and direct. Because expressions are finite trees over countable labels, there are only countably many of them, and each evaluates to one value. The continuum, the uncountable set of real numbers, is not the carrier of analytic content; a certified countable protocol registry is. This is the countability fact that blocks what the framework calls continuum smuggling: the attempt to import uncountable structure through the back door of evaluation.

The library also proves that the operations behave as expected under evaluation. Rational literals evaluate to their rational values. Addition, negation, and subtraction in the expression tree become ordinary addition, negation, and subtraction of real values. These are the algebraic facts that make the expression tree a usable language for building protocols, and they are all THEOREMs in the machine-checked library.

What Expr does not claim is as important as what it proves. It does not claim that every real number is expressible; the countability theorem says the opposite. It does not claim that the registry itself is canonical or unique; any countable registry of constants and transformers works. And it does not claim that the framework's physical constants, such as the golden ratio or the fine-structure constant, are derived from this expression tree. The expression tree is a language for building and reasoning about protocols, not a source of physical content.

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

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

Expr does not claim that every real number is expressible; the countability theorem says the opposite. Expr does not claim that the registry itself is canonical or unique. Expr does not claim that the framework's physical constants are derived from this expression tree.

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: