Foundation Primitive Recognition Calculus Certified Analytic Protocols Registry

Certified analytic protocols

In Recognition Science, the ledger (a discrete record of recognition events) is the fundamental object. The Registry is a formal structure that organizes the analytic ingredients of that ledger into a countable, machine-checked list. It provides two basic operations: a way to look up a constant protocol by index, and a way to apply a unary transformer to a protocol. This is a definitional choice, not a theorem; the Registry itself is a structure, not a result.

The Registry's real content is in what it proves about the expressions built from it. An expression is a finite tree: rational numbers, registered constants, negation, addition, subtraction, and unary transforms. The key theorem, transcendental_protocol_closure, states that any such Registry generates only countably many real values, and every one of those values is witnessed by a Delta-real protocol. In plain terms: the Registry cannot smuggle in an uncountable continuum of analytic content. The continuum is not the carrier of analytic content; a certified countable protocol registry is.

This countability fact is the load-bearing result. It blocks a specific failure mode, which the framework calls "continuum smuggling": the idea that a physical theory needs an uncountable set of real numbers to describe reality. The Registry shows that a countable set of certified analytic protocols is enough to generate all the values it can produce. The proof is short and direct, relying on the fact that expressions are finite trees over countable labels.

In Recognition Science, this Registry is a foundational tool. It is not a physical law or a derivation of a constant; it is a definitional framework for how analytic content can be represented. The framework's library proves that addition, negation, and subtraction behave correctly under evaluation, and that rational literals evaluate to their rational values. These are sanity checks, not physics. The Registry establishes the grammar of certified analytic content, and the theorems about it ensure that the grammar is sound and countable.

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

/-- A countable registry of certified analytic protocol ingredients.

`const k` is the `k`th registered constant protocol. `unary k` is the `k`th
registered unary protocol transformer. Binary protocol operations are kept to the
native additive operations already proved in `DeltaReal`; further binary analytic
operations can be encoded as unary transforms on paired protocols if needed. -/
structure Registry where
  const : ℕ → Protocol
  unary : ℕ → Protocol → Protocol

/-- Finite expressions over a certified analytic registry. The expression tree is
the native object; evaluation returns a protocol, never an uncountable graph. -/
inductive Expr where
  | rat : ℚ → Expr
  | const : ℕ → Expr
  | neg : Expr → Expr
  | add : Expr → Expr → Expr
  | sub : Expr → Expr → Expr
  | unary : ℕ → Expr → Expr
  deriving DecidableEq, Repr, Countable

What this page does not claim

The Registry does not derive any physical constant or law. The Registry does not prove that the continuum of real numbers is inconsistent. The Registry does not define what a protocol is; that is a separate structure.

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: