IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSCarrier

   1/-
   2  PrimitiveRecognitionCalculus/FRSCarrier.lean
   3
   4  Phase 3 of the Delta-Native Analysis frontier: the F_RS carrier as an explicit
   5  finite-description syntax.
   6
   7  `PRCMinimalField` proved that every named RS constant value lives in one
   8  countable subfield `rsField ⊊ ℝ`, generated abstractly by `Subfield.closure`.
   9  This module gives the carrier a concrete face: an inductive term language whose
  10  closed terms are exactly the finite expressions over the RS constant inventory
  11  and the rationals, with an evaluation into ℝ.
  12
  13  The point is finite description. A term of `FRSExpr` is a literally finite tree.
  14  Its value is a real. We prove every value lands in the countable `rsField`, so
  15  the syntax never escapes the carrier; and we exhibit the constant inventory
  16  (φ, π, e, α⁻¹) and the rationals as terms.
  17
  18  Honest boundary (inherited from `PRCMinimalField`). The arithmetic operations of
  19  the syntax are `+, −, ×, ⁻¹`. The genuinely transcendental constants (π, e, α⁻¹)
  20  enter as PRIMITIVE inventory symbols, not as finite arithmetic of simpler terms,
  21  because the transcendental functions that produce them are not finite arithmetic.
  22  The syntax captures finite generation over a fixed inventory; it does not claim
  23  to generate the transcendental functions themselves.
  24
  25  What is proved:
  26
  27  * `eval_mem`        : every term evaluates into `rsField` (soundness);
  28  * inventory lemmas  : φ, π, e, α⁻¹ and every rational are terms;
  29  * `value_countable` : the set of term values is countable (a proper subset of ℝ);
  30  * `has_protocol_display` : every term value is the value of a Delta-real protocol,
  31                        so the finite-description carrier has a protocol display in
  32                        the `ℝδ` interface;
  33  * `frs_carrier`     : the headline conjunction.
  34
  35  No project-local axioms. No sorry.
  36-/
  37
  38import Mathlib
  39import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMinimalField
  40import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal
  41
  42namespace IndisputableMonolith
  43namespace Foundation
  44namespace PrimitiveRecognitionCalculus
  45namespace FRSCarrier
  46
  47/-- The F_RS carrier expression syntax: a finite term over the rationals and the
  48RS constant inventory, closed under field operations. -/
  49inductive FRSExpr where
  50  | rat : ℚ → FRSExpr
  51  | phi : FRSExpr
  52  | pi : FRSExpr
  53  | e : FRSExpr
  54  | alphaInv : FRSExpr
  55  | neg : FRSExpr → FRSExpr
  56  | add : FRSExpr → FRSExpr → FRSExpr
  57  | mul : FRSExpr → FRSExpr → FRSExpr
  58  | inv : FRSExpr → FRSExpr
  59  deriving DecidableEq, Repr
  60
  61/-- Evaluation of a carrier term into ℝ. -/
  62noncomputable def eval : FRSExpr → ℝ
  63  | .rat q => (q : ℝ)
  64  | .phi => Real.goldenRatio
  65  | .pi => Real.pi
  66  | .e => Real.exp 1
  67  | .alphaInv => MinimalField.alphaInv
  68  | .neg a => -(eval a)
  69  | .add a b => eval a + eval b
  70  | .mul a b => eval a * eval b
  71  | .inv a => (eval a)⁻¹
  72
  73/-- **Soundness.** Every carrier term evaluates into the countable field `rsField`.
  74The finite-description syntax never escapes the carrier. -/
  75theorem eval_mem (ex : FRSExpr) : eval ex ∈ MinimalField.rsField := by
  76  induction ex with
  77  | rat q => exact SubfieldClass.ratCast_mem MinimalField.rsField q
  78  | phi => simpa [eval] using MinimalField.rsField_mem_phi
  79  | pi => simpa [eval] using MinimalField.rsField_mem_pi
  80  | e => simpa [eval] using MinimalField.rsField_mem_e
  81  | alphaInv => simpa [eval] using MinimalField.rsField_mem_alphaInv
  82  | neg a ih => simpa [eval] using neg_mem ih
  83  | add a b iha ihb => simpa [eval] using add_mem iha ihb
  84  | mul a b iha ihb => simpa [eval] using mul_mem iha ihb
  85  | inv a ih => simpa [eval] using inv_mem ih
  86
  87/-! ### Constant inventory -/
  88
  89theorem rat_is_term (q : ℚ) : eval (FRSExpr.rat q) = (q : ℝ) := rfl
  90theorem phi_is_term : eval FRSExpr.phi = Real.goldenRatio := rfl
  91theorem pi_is_term : eval FRSExpr.pi = Real.pi := rfl
  92theorem e_is_term : eval FRSExpr.e = Real.exp 1 := rfl
  93theorem alphaInv_is_term : eval FRSExpr.alphaInv = MinimalField.alphaInv := rfl
  94
  95/-- The set of all values produced by the carrier syntax. -/
  96noncomputable def carrierValues : Set ℝ := Set.range eval
  97
  98/-- The carrier value set sits inside `rsField`. -/
  99theorem carrierValues_subset : carrierValues ⊆ (MinimalField.rsField : Set ℝ) := by
 100  rintro x ⟨ex, rfl⟩
 101  exact eval_mem ex
 102
 103/-- The carrier value set is countable: only countably many finite terms exist. -/
 104theorem carrierValues_countable : carrierValues.Countable :=
 105  (MinimalField.rsField_countable).mono carrierValues_subset
 106
 107/-- The carrier values are a proper subset of ℝ. -/
 108theorem carrierValues_proper : carrierValues ≠ Set.univ := by
 109  intro h
 110  exact Cardinal.not_countable_real (h ▸ carrierValues_countable)
 111
 112/-- **Protocol display.** Every carrier term value is the value of a Delta-real
 113protocol, so the finite-description carrier renders into the `ℝδ` interface. -/
 114theorem has_protocol_display (ex : FRSExpr) :
 115    ∃ x : DeltaReal.Protocol, x.value = eval ex :=
 116  DeltaReal.Protocol.value_surjective (eval ex)
 117
 118/-- **Phase 3 headline.** The F_RS carrier is an explicit finite-description
 119syntax: every term evaluates into the countable field `rsField` (soundness), the
 120constant inventory (φ, π, e, α⁻¹) and the rationals are terms, the term values are
 121countable and a proper subset of ℝ, and every term value has a protocol display in
 122the `ℝδ` interface. The carrier the framework actually computes on is finite
 123generation over a fixed inventory, not the uncountable continuum. -/
 124theorem frs_carrier :
 125    (∀ ex : FRSExpr, eval ex ∈ MinimalField.rsField)
 126      ∧ eval FRSExpr.phi = Real.goldenRatio
 127      ∧ eval FRSExpr.pi = Real.pi
 128      ∧ eval FRSExpr.e = Real.exp 1
 129      ∧ eval FRSExpr.alphaInv = MinimalField.alphaInv
 130      ∧ carrierValues.Countable
 131      ∧ carrierValues ≠ Set.univ
 132      ∧ (∀ ex : FRSExpr, ∃ x : DeltaReal.Protocol, x.value = eval ex) :=
 133  ⟨eval_mem, phi_is_term, pi_is_term, e_is_term, alphaInv_is_term,
 134    carrierValues_countable, carrierValues_proper, has_protocol_display⟩
 135
 136end FRSCarrier
 137end PrimitiveRecognitionCalculus
 138end Foundation
 139end IndisputableMonolith
 140