IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CertifiedAnalyticProtocols

   1/-
   2  PrimitiveRecognitionCalculus/CertifiedAnalyticProtocols.lean
   3
   4  Second pass on the Delta-Native Analysis frontier: closing the "transcendental
   5  functions without ambient continuum" gap at the correct layer.
   6
   7  The first pass showed that the named RS constant values live in a countable
   8  field, while the classical continuum is a protocol display. The remaining
   9  objection was sharper: the transcendental functions used to name constants
  10  (`exp`, `log`, π-producing procedures, etc.) look like ambient-continuum objects.
  11
  12  The closure here is not "all transcendental functions as uncountable graphs".
  13  That would re-import the continuum. The native object is a *certified protocol
  14  registry*: a countable list of rational-interval constants and countable lists of
  15  protocol transformers. Expressions over that registry are finite trees; their
  16  evaluation is a Delta-real protocol; and the value set of all such expressions is
  17  countable. The analytic content is the certificate carried by each registered
  18  protocol/transformer, not an uncountable function graph.
  19
  20  This resolves the ambient-continuum objection in the only honest form: RS may
  21  use transcendental operations when they are supplied as countably indexed
  22  certified protocol transformers. It does not need a completed continuum as the
  23  domain of all analytic functions.
  24
  25  No project-local axioms. No sorry.
  26-/
  27
  28import Mathlib
  29import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal
  30
  31namespace IndisputableMonolith
  32namespace Foundation
  33namespace PrimitiveRecognitionCalculus
  34namespace CertifiedAnalyticProtocols
  35
  36open DeltaReal
  37
  38/-- A countable registry of certified analytic protocol ingredients.
  39
  40`const k` is the `k`th registered constant protocol. `unary k` is the `k`th
  41registered unary protocol transformer. Binary protocol operations are kept to the
  42native additive operations already proved in `DeltaReal`; further binary analytic
  43operations can be encoded as unary transforms on paired protocols if needed. -/
  44structure Registry where
  45  const : ℕ → Protocol
  46  unary : ℕ → Protocol → Protocol
  47
  48/-- Finite expressions over a certified analytic registry. The expression tree is
  49the native object; evaluation returns a protocol, never an uncountable graph. -/
  50inductive Expr where
  51  | rat : ℚ → Expr
  52  | const : ℕ → Expr
  53  | neg : Expr → Expr
  54  | add : Expr → Expr → Expr
  55  | sub : Expr → Expr → Expr
  56  | unary : ℕ → Expr → Expr
  57  deriving DecidableEq, Repr, Countable
  58
  59namespace Expr
  60
  61/-- Evaluation of a finite certified-analytic expression as a Delta-real protocol. -/
  62noncomputable def eval (R : Registry) : Expr → Protocol
  63  | .rat q => Protocol.ofRat q
  64  | .const k => R.const k
  65  | .neg a => Protocol.neg (eval R a)
  66  | .add a b => Protocol.add (eval R a) (eval R b)
  67  | .sub a b => Protocol.sub (eval R a) (eval R b)
  68  | .unary k a => R.unary k (eval R a)
  69
  70/-- Evaluation followed by display as a real value. -/
  71noncomputable def value (R : Registry) (e : Expr) : ℝ :=
  72  (eval R e).value
  73
  74/-- The set of values generated by a registry. -/
  75noncomputable def values (R : Registry) : Set ℝ := Set.range (value R)
  76
  77/-- Registry values are countable because expressions are finite trees over
  78countable labels. This is the countability fact that blocks continuum smuggling. -/
  79theorem values_countable (R : Registry) : (values R).Countable :=
  80  Set.countable_range (value R)
  81
  82/-- Every registry value has a protocol witness, by construction. -/
  83theorem every_value_has_protocol (R : Registry) (x : ℝ) (hx : x ∈ values R) :
  84    ∃ p : Protocol, p.value = x := by
  85  rcases hx with ⟨e, rfl⟩
  86  exact ⟨eval R e, rfl⟩
  87
  88/-- Rational literals evaluate to their rational values. -/
  89@[simp] theorem value_rat (R : Registry) (q : ℚ) :
  90    value R (.rat q) = (q : ℝ) := by
  91  simp [value, eval, Protocol.value_ofRat]
  92
  93/-- Native addition remains addition under the value display. -/
  94theorem value_add (R : Registry) (a b : Expr) :
  95    value R (.add a b) = value R a + value R b := by
  96  simp [value, eval, Protocol.value_add]
  97
  98/-- Native negation remains negation under the value display. -/
  99theorem value_neg (R : Registry) (a : Expr) :
 100    value R (.neg a) = - value R a := by
 101  simp [value, eval, Protocol.value_neg]
 102
 103/-- Native subtraction remains subtraction under the value display. -/
 104theorem value_sub (R : Registry) (a b : Expr) :
 105    value R (.sub a b) = value R a - value R b := by
 106  simp [value, eval, Protocol.value_sub]
 107
 108/-- **Transcendental protocol closure.** Any countably indexed registry of certified
 109analytic constants and protocol transformers generates only countably many real
 110values, and every value is witnessed by a Delta-real protocol. The continuum is not
 111the carrier of analytic content; a certified countable protocol registry is. -/
 112theorem transcendental_protocol_closure (R : Registry) :
 113    (values R).Countable
 114      ∧ (∀ x : ℝ, x ∈ values R → ∃ p : Protocol, p.value = x)
 115      ∧ (∀ q : ℚ, value R (.rat q) = (q : ℝ))
 116      ∧ (∀ a b : Expr, value R (.add a b) = value R a + value R b)
 117      ∧ (∀ a : Expr, value R (.neg a) = - value R a)
 118      ∧ (∀ a b : Expr, value R (.sub a b) = value R a - value R b) :=
 119  ⟨values_countable R, every_value_has_protocol R, value_rat R, value_add R,
 120    value_neg R, value_sub R⟩
 121
 122end Expr
 123end CertifiedAnalyticProtocols
 124end PrimitiveRecognitionCalculus
 125end Foundation
 126end IndisputableMonolith
 127