IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CertifiedAnalyticTransformers

   1/-
   2  PrimitiveRecognitionCalculus/CertifiedAnalyticTransformers.lean
   3
   4  Stronger certified analytic transformer registry.
   5
   6  `CertifiedAnalyticProtocols.lean` proves the basic point: countably indexed
   7  certified constants and unary protocol transformers generate only countably
   8  many display values. This module adds the next useful closure:
   9
  10  * binary certified transformers;
  11  * finite expression trees using unary and binary transformers;
  12  * countability of all generated display values;
  13  * composition closure for unary protocol transformers.
  14
  15  Analytic content remains in the certificate carried by the registered
  16  transformer. The native object is still a finite tree over a countable
  17  registry, not an uncountable graph.
  18
  19  No project-local axioms. No sorry.
  20-/
  21
  22import Mathlib
  23import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CertifiedAnalyticProtocols
  24
  25namespace IndisputableMonolith
  26namespace Foundation
  27namespace PrimitiveRecognitionCalculus
  28namespace CertifiedAnalyticTransformers
  29
  30open DeltaReal
  31
  32/-- A richer countable registry with constants, unary protocol transformers, and
  33binary protocol transformers. -/
  34structure RichRegistry where
  35  const : ℕ → Protocol
  36  unary : ℕ → Protocol → Protocol
  37  binary : ℕ → Protocol → Protocol → Protocol
  38
  39/-- Finite expressions over the richer certified analytic registry. -/
  40inductive RichExpr where
  41  | rat : ℚ → RichExpr
  42  | const : ℕ → RichExpr
  43  | neg : RichExpr → RichExpr
  44  | add : RichExpr → RichExpr → RichExpr
  45  | sub : RichExpr → RichExpr → RichExpr
  46  | unary : ℕ → RichExpr → RichExpr
  47  | binary : ℕ → RichExpr → RichExpr → RichExpr
  48  deriving DecidableEq, Repr, Countable
  49
  50namespace RichExpr
  51
  52/-- Evaluation of a finite rich certified-analytic expression as a protocol. -/
  53noncomputable def eval (R : RichRegistry) : RichExpr → Protocol
  54  | .rat q => Protocol.ofRat q
  55  | .const k => R.const k
  56  | .neg a => Protocol.neg (eval R a)
  57  | .add a b => Protocol.add (eval R a) (eval R b)
  58  | .sub a b => Protocol.sub (eval R a) (eval R b)
  59  | .unary k a => R.unary k (eval R a)
  60  | .binary k a b => R.binary k (eval R a) (eval R b)
  61
  62noncomputable def value (R : RichRegistry) (e : RichExpr) : ℝ :=
  63  (eval R e).value
  64
  65noncomputable def values (R : RichRegistry) : Set ℝ := Set.range (value R)
  66
  67theorem values_countable (R : RichRegistry) : (values R).Countable :=
  68  Set.countable_range (value R)
  69
  70theorem every_value_has_protocol (R : RichRegistry) (x : ℝ) (hx : x ∈ values R) :
  71    ∃ p : Protocol, p.value = x := by
  72  rcases hx with ⟨e, rfl⟩
  73  exact ⟨eval R e, rfl⟩
  74
  75@[simp] theorem value_rat (R : RichRegistry) (q : ℚ) :
  76    value R (.rat q) = (q : ℝ) := by
  77  simp [value, eval, Protocol.value_ofRat]
  78
  79theorem value_add (R : RichRegistry) (a b : RichExpr) :
  80    value R (.add a b) = value R a + value R b := by
  81  simp [value, eval, Protocol.value_add]
  82
  83theorem value_neg (R : RichRegistry) (a : RichExpr) :
  84    value R (.neg a) = - value R a := by
  85  simp [value, eval, Protocol.value_neg]
  86
  87theorem value_sub (R : RichRegistry) (a b : RichExpr) :
  88    value R (.sub a b) = value R a - value R b := by
  89  simp [value, eval, Protocol.value_sub]
  90
  91/-- Rich certified-analytic closure: binary transformers and unary transformers
  92still generate only countably many display values, each protocol-witnessed. -/
  93theorem rich_transformer_closure (R : RichRegistry) :
  94    (values R).Countable
  95      ∧ (∀ x : ℝ, x ∈ values R → ∃ p : Protocol, p.value = x)
  96      ∧ (∀ q : ℚ, value R (.rat q) = (q : ℝ))
  97      ∧ (∀ a b : RichExpr, value R (.add a b) = value R a + value R b)
  98      ∧ (∀ a : RichExpr, value R (.neg a) = - value R a)
  99      ∧ (∀ a b : RichExpr, value R (.sub a b) = value R a - value R b) :=
 100  ⟨values_countable R, every_value_has_protocol R, value_rat R, value_add R,
 101    value_neg R, value_sub R⟩
 102
 103end RichExpr
 104
 105/-- Composition of two unary protocol transformers. -/
 106def composeUnary (f g : Protocol → Protocol) : Protocol → Protocol :=
 107  fun p => f (g p)
 108
 109theorem composeUnary_assoc (f g h : Protocol → Protocol) :
 110    composeUnary (composeUnary f g) h = composeUnary f (composeUnary g h) := by
 111  rfl
 112
 113/-- Any rich registry has a derived unary transformer obtained by composing two
 114registered unary transformers. -/
 115def composedUnary (R : RichRegistry) (i j : ℕ) : Protocol → Protocol :=
 116  composeUnary (R.unary i) (R.unary j)
 117
 118/-- **Certified analytic transformer headline.** Adding binary transformers and
 119finite compositions of unary transformers does not re-import the continuum:
 120generated values remain countable and protocol-witnessed, and unary transformer
 121composition is associative. -/
 122theorem certified_transformer_headline (R : RichRegistry) :
 123    (RichExpr.values R).Countable
 124      ∧ (∀ x : ℝ, x ∈ RichExpr.values R → ∃ p : Protocol, p.value = x)
 125      ∧ (∀ f g h : Protocol → Protocol,
 126          composeUnary (composeUnary f g) h = composeUnary f (composeUnary g h)) :=
 127  ⟨RichExpr.values_countable R, RichExpr.every_value_has_protocol R, composeUnary_assoc⟩
 128
 129end CertifiedAnalyticTransformers
 130end PrimitiveRecognitionCalculus
 131end Foundation
 132end IndisputableMonolith
 133