IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCExpLogField

   1/-
   2  PrimitiveRecognitionCalculus/PRCExpLogField.lean
   3
   4  Item 1 of the δ frontier, the deep half: the *construction*, not just the
   5  *values*, never needs the continuum.
   6
   7  `PRCMinimalField` proved the named RS constant values live in a countable
   8  subfield of ℝ. That leaves an honest residual: the constants are not given as
   9  bare values, they are *built* by the operations
  10
  11      +, −, ×, ÷, exp, log
  12
  13  applied to ℚ, π, and φ. For example
  14
  15      α⁻¹ = 44·π·exp( − w₈·ln φ / (44·π) ).
  16
  17  A reasonable objection is that even if the answers are countable, the
  18  *definitional closure* under those operations might force the uncountable line:
  19  `exp` and `log` are analytic functions on ℝ. This module closes that objection.
  20
  21  We build the smallest subfield of ℝ that contains ℚ, π, φ AND is closed under
  22  `exp` and `log`, as the union of an increasing chain
  23
  24      S₀ = ℚ(π, φ),   S_{n+1} = ℚ( S_n ∪ exp(S_n) ∪ log(S_n) ).
  25
  26  Each stage is a subfield generated by a countable set, hence countable; the
  27  union of the directed chain is a subfield (`Subfield.mem_iSup_of_directed`),
  28  countable (`Set.countable_iUnion`), closed under `exp` and `log` by
  29  construction, and a proper subset of ℝ (the continuum is uncountable).
  30
  31  The headline `rs_operations_below_continuum` then exhibits ONE countable field
  32  `T` that is closed under exactly the operations the RS constants are built from
  33  and that already contains π, φ, e, and α⁻¹. Every step of every RS constant's
  34  definition can be carried out inside `T`; the construction never has to reach
  35  outside a countable structure.
  36
  37  HONEST BOUNDARY (the only residual that survives). `Real.exp` and `Real.log` are
  38  here the standard Mathlib functions, whose *type* is ℝ → ℝ. We do not rebuild
  39  analysis over a countable model; we show the orbit of the RS generators under
  40  those functions is countable and field-closed. The remaining philosophical step,
  41  giving `exp`/`log` themselves a definition with no uncountable ambient (a fully
  42  constructive/computable analysis), is outside this framework and outside RS. What
  43  is eliminated here is the claim that the continuum is needed as the *workspace*
  44  of the construction: it is not; a single countable exp/log-closed field suffices.
  45
  46  No project-local axioms. No sorry.
  47-/
  48
  49import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMinimalField
  50
  51namespace IndisputableMonolith
  52namespace Foundation
  53namespace PrimitiveRecognitionCalculus
  54namespace ExpLogField
  55
  56/-- The generators of the exp/log closure: π and φ. Rationals come for free as the
  57prime field of any subfield, so these two transcendental/algebraic seeds plus the
  58field and exp/log operations reach every RS constant. -/
  59noncomputable def gens : Set ℝ := {Real.pi, Real.goldenRatio}
  60
  61theorem gens_finite : gens.Finite := by
  62  unfold gens
  63  exact (Set.finite_singleton _).insert _
  64
  65/-- One stage of the construction: adjoin the images of the current field under
  66`exp` and `log`, then take the subfield they generate. -/
  67noncomputable def Sstep (K : Subfield ℝ) : Subfield ℝ :=
  68  Subfield.closure ((K : Set ℝ) ∪ Real.exp '' (K : Set ℝ) ∪ Real.log '' (K : Set ℝ))
  69
  70/-- The increasing chain of stages. -/
  71noncomputable def S : ℕ → Subfield ℝ
  72  | 0 => Subfield.closure gens
  73  | (n + 1) => Sstep (S n)
  74
  75/-- Each stage embeds in the next: the chain is increasing. -/
  76theorem S_mono (n : ℕ) : S n ≤ S (n + 1) := by
  77  have hsub : (S n : Set ℝ) ⊆ (S (n + 1) : Set ℝ) := by
  78    intro x hx
  79    have : x ∈ Sstep (S n) := Subfield.subset_closure (Or.inl (Or.inl hx))
  80    exact this
  81  exact SetLike.coe_subset_coe.mp hsub
  82
  83theorem S_monotone : Monotone S := monotone_nat_of_le_succ S_mono
  84
  85theorem S_directed : Directed (· ≤ ·) S := S_monotone.directed_le
  86
  87/-- Every stage is countable: a subfield generated by a countable set. -/
  88theorem S_countable (n : ℕ) : (S n : Set ℝ).Countable := by
  89  induction n with
  90  | zero =>
  91      show (Subfield.closure gens : Set ℝ).Countable
  92      exact MinimalField.subfield_closure_countable_of_finite gens_finite
  93  | succ n ih =>
  94      have hc :
  95          ((S n : Set ℝ) ∪ Real.exp '' (S n : Set ℝ) ∪ Real.log '' (S n : Set ℝ)).Countable :=
  96        (ih.union (ih.image Real.exp)).union (ih.image Real.log)
  97      exact MinimalField.subfield_closure_countable_of_countable hc
  98
  99/-- **The exp/log-closed RS field.** The union of the directed chain. -/
 100noncomputable def T : Subfield ℝ := ⨆ n, S n
 101
 102theorem mem_T_iff {x : ℝ} : x ∈ T ↔ ∃ n, x ∈ S n :=
 103  Subfield.mem_iSup_of_directed S_directed
 104
 105theorem T_coe : (T : Set ℝ) = ⋃ n, (S n : Set ℝ) :=
 106  Subfield.coe_iSup_of_directed S_directed
 107
 108/-- `T` is countable: a countable union of countable stages. -/
 109theorem T_countable : (T : Set ℝ).Countable := by
 110  rw [T_coe]
 111  exact Set.countable_iUnion S_countable
 112
 113/-- `T` is closed under `exp`. -/
 114theorem T_exp_closed {x : ℝ} (hx : x ∈ T) : Real.exp x ∈ T := by
 115  rw [mem_T_iff] at hx ⊢
 116  obtain ⟨n, hn⟩ := hx
 117  refine ⟨n + 1, ?_⟩
 118  have : Real.exp x ∈ Sstep (S n) :=
 119    Subfield.subset_closure (Or.inl (Or.inr ⟨x, hn, rfl⟩))
 120  exact this
 121
 122/-- `T` is closed under `log`. -/
 123theorem T_log_closed {x : ℝ} (hx : x ∈ T) : Real.log x ∈ T := by
 124  rw [mem_T_iff] at hx ⊢
 125  obtain ⟨n, hn⟩ := hx
 126  refine ⟨n + 1, ?_⟩
 127  have : Real.log x ∈ Sstep (S n) :=
 128    Subfield.subset_closure (Or.inr ⟨x, hn, rfl⟩)
 129  exact this
 130
 131theorem pi_mem_T : Real.pi ∈ T :=
 132  mem_T_iff.mpr ⟨0, Subfield.subset_closure (Set.mem_insert _ _)⟩
 133
 134theorem phi_mem_T : Real.goldenRatio ∈ T :=
 135  mem_T_iff.mpr ⟨0, Subfield.subset_closure (Set.mem_insert_of_mem _ rfl)⟩
 136
 137/-- Euler's number is `exp 1`, and `1 ∈ T`, so `e ∈ T` by exp-closure. -/
 138theorem e_mem_T : Real.exp 1 ∈ T := T_exp_closed (one_mem T)
 139
 140/-- **The payoff: α⁻¹ is built entirely inside `T`.** Every operation in
 141`α⁻¹ = 44·π·exp(−w₈·ln φ/(44·π))` (field operations, one `log`, one `exp`) lands in
 142`T`, so the constant is a `T`-element produced without leaving the countable
 143field. -/
 144theorem alphaInv_mem_T : MinimalField.alphaInv ∈ T := by
 145  have hpi : Real.pi ∈ T := pi_mem_T
 146  have hphi : Real.goldenRatio ∈ T := phi_mem_T
 147  have h44 : (44 : ℝ) ∈ T := by exact_mod_cast (natCast_mem T 44)
 148  have hw8 : MinimalField.w8 ∈ T := by
 149    unfold MinimalField.w8
 150    exact_mod_cast (natCast_mem T 4)
 151  have hlogphi : Real.log Real.goldenRatio ∈ T := T_log_closed hphi
 152  have harg :
 153      -(MinimalField.w8) * Real.log Real.goldenRatio / (44 * Real.pi) ∈ T :=
 154    div_mem (mul_mem (neg_mem hw8) hlogphi) (mul_mem h44 hpi)
 155  have hexp :
 156      Real.exp (-(MinimalField.w8) * Real.log Real.goldenRatio / (44 * Real.pi)) ∈ T :=
 157    T_exp_closed harg
 158  unfold MinimalField.alphaInv
 159  exact mul_mem (mul_mem h44 hpi) hexp
 160
 161/-- `T` is a proper subset of ℝ: it is countable, the continuum is not. -/
 162theorem T_proper : (T : Set ℝ) ≠ Set.univ := by
 163  intro h
 164  exact Cardinal.not_countable_real (h ▸ T_countable)
 165
 166/-- **Item 1, deep half.** There is a single countable subfield `T` of ℝ that is
 167closed under exactly the operations the RS constants are built from (field
 168operations, `exp`, `log`), already contains the seeds π and φ, and contains the
 169derived constants `e` and `α⁻¹`. The construction of every RS constant can be
 170performed entirely inside this countable field; the uncountable real line is not
 171required as the workspace, only (at most) as the ambient in which the standard
 172`exp`/`log` happen to be defined. The continuum is removed from the framework's
 173operations, not just its outputs. -/
 174theorem rs_operations_below_continuum :
 175    ∃ K : Subfield ℝ,
 176      (K : Set ℝ).Countable
 177        ∧ (∀ x ∈ K, Real.exp x ∈ K)
 178        ∧ (∀ x ∈ K, Real.log x ∈ K)
 179        ∧ Real.pi ∈ K
 180        ∧ Real.goldenRatio ∈ K
 181        ∧ Real.exp 1 ∈ K
 182        ∧ MinimalField.alphaInv ∈ K
 183        ∧ (K : Set ℝ) ≠ Set.univ :=
 184  ⟨T, T_countable, fun _ hx => T_exp_closed hx, fun _ hx => T_log_closed hx,
 185    pi_mem_T, phi_mem_T, e_mem_T, alphaInv_mem_T, T_proper⟩
 186
 187end ExpLogField
 188end PrimitiveRecognitionCalculus
 189end Foundation
 190end IndisputableMonolith
 191