IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMinimalField

   1/-
   2  PrimitiveRecognitionCalculus/PRCMinimalField.lean
   3
   4  Item 1 of the δ frontier: the transcendental minimal-field question.
   5
   6  The δ-native rational field ℚ_δ ≅ ℚ is countable. Its algebraic closure
   7  inside ℝ (the carrier where every δ-posable polynomial comparison resolves,
   8  including √2 and √5, hence φ) is still countable
   9  (`delta_algebraic_closure_stays_countable`, proved elsewhere in this
  10  directory). But the actual Recognition-Science physical constants are
  11  transcendental: the fine-structure value
  12
  13      α⁻¹ = 44·π·exp( − w₈·ln φ / (44·π) )
  14
  15  uses π and exp, which are not algebraic, so they do not live in the algebraic
  16  closure. This module pins the next field up: the subfield of ℝ generated by
  17  ℚ together with the actual constant values. The headline results are:
  18
  19  * a finitely-or-countably generated subfield of ℝ is countable
  20    (`subfield_closure_countable_of_countable`);
  21  * the field generated by the named RS constants (φ, π, e, α⁻¹) is countable
  22    and a proper subset of ℝ (`rs_physics_below_continuum`).
  23
  24  So every RS constant value lives in a countable field strictly below the
  25  continuum. The construction's *outputs* never require the uncountable ℝ; the
  26  continuum is at most a scaffold for *defining* the transcendental functions,
  27  not the home of the answers.
  28
  29  HONEST BOUNDARY. This module proves the constant *values* are countable-field
  30  elements. It does not yet prove the transcendental functions (exp, log, the
  31  analytic definitions that produce those values) can themselves be carried out
  32  inside a countable structure with no uncountable ambient. That deeper
  33  elimination is the remaining open step of Item 1; what is closed here is that
  34  the answers live below the continuum, which removes the continuum as the
  35  necessary *codomain* of RS physics.
  36
  37  No project-local axioms. No sorry.
  38-/
  39
  40import Mathlib
  41
  42namespace IndisputableMonolith
  43namespace Foundation
  44namespace PrimitiveRecognitionCalculus
  45namespace MinimalField
  46
  47open Cardinal
  48
  49/-- A subfield of `ℝ` generated by a countable set is countable.
  50
  51This is the load-bearing closure fact: adjoining countably many reals to the
  52rationals never escapes countability. It is the field-level analogue of
  53`delta_algebraic_closure_stays_countable`, lifted from algebraic generators to
  54arbitrary (including transcendental) generators. -/
  55theorem subfield_closure_countable_of_countable {s : Set ℝ} (hs : s.Countable) :
  56    (Subfield.closure s : Set ℝ).Countable := by
  57  have hs' : Cardinal.mk s ≤ ℵ₀ :=
  58    Cardinal.mk_le_aleph0_iff.mpr (Set.countable_coe_iff.mpr hs)
  59  have hcard : Cardinal.mk (Subfield.closure s) ≤ ℵ₀ :=
  60    (Subfield.cardinalMk_closure_le_max s).trans (max_le hs' le_rfl)
  61  have hcount : Countable (Subfield.closure s) := Cardinal.mk_le_aleph0_iff.mp hcard
  62  exact Set.countable_coe_iff.mp hcount
  63
  64/-- The same fact for a finite generating set, the case the RS constants need. -/
  65theorem subfield_closure_countable_of_finite {s : Set ℝ} (hs : s.Finite) :
  66    (Subfield.closure s : Set ℝ).Countable :=
  67  subfield_closure_countable_of_countable hs.countable
  68
  69/-- The fine-structure weight `w₈`. Its exact value is irrelevant to the
  70countability statement; the constant value is whatever it is, and is adjoined as
  71an element. -/
  72noncomputable def w8 : ℝ := 4
  73
  74/-- The Recognition-Science fine-structure constant value
  75`α⁻¹ = 44·π·exp(−w₈·ln φ/(44·π))`, a specific transcendental real. -/
  76noncomputable def alphaInv : ℝ :=
  77  44 * Real.pi * Real.exp (-(w8) * Real.log Real.goldenRatio / (44 * Real.pi))
  78
  79/-- The named RS constant values: the golden ratio φ, π, Euler's e, and α⁻¹. -/
  80noncomputable def rsConstants : Set ℝ :=
  81  {Real.goldenRatio, Real.pi, Real.exp 1, alphaInv}
  82
  83/-- The minimal field carrying RS physics: the subfield of ℝ generated by the
  84named constants. It automatically contains ℚ (the prime field), so it is
  85exactly `ℚ_δ` adjoined with the constant values. -/
  86noncomputable def rsField : Subfield ℝ :=
  87  Subfield.closure rsConstants
  88
  89theorem rsConstants_finite : rsConstants.Finite := by
  90  unfold rsConstants
  91  exact (((Set.finite_singleton _).insert _).insert _).insert _
  92
  93theorem rsConstants_countable : rsConstants.Countable :=
  94  rsConstants_finite.countable
  95
  96/-- The RS constant field is countable. -/
  97theorem rsField_countable : (rsField : Set ℝ).Countable :=
  98  subfield_closure_countable_of_finite rsConstants_finite
  99
 100theorem rsField_mem_phi : Real.goldenRatio ∈ rsField :=
 101  Subfield.subset_closure (by unfold rsConstants; simp)
 102
 103theorem rsField_mem_pi : Real.pi ∈ rsField :=
 104  Subfield.subset_closure (by unfold rsConstants; simp)
 105
 106theorem rsField_mem_e : Real.exp 1 ∈ rsField :=
 107  Subfield.subset_closure (by unfold rsConstants; simp)
 108
 109theorem rsField_mem_alphaInv : alphaInv ∈ rsField :=
 110  Subfield.subset_closure (by unfold rsConstants; simp)
 111
 112/-- The RS constant field is a *proper* subset of ℝ: it is countable, while the
 113continuum is not. The continuum is therefore not the home of RS physics. -/
 114theorem rsField_proper : (rsField : Set ℝ) ≠ Set.univ := by
 115  intro h
 116  have huniv : (Set.univ : Set ℝ).Countable := h ▸ rsField_countable
 117  exact Cardinal.not_countable_real huniv
 118
 119/-- **Item 1 headline.** Every named Recognition-Science constant value lives in
 120one countable subfield of ℝ that is strictly below the continuum. The arbitrary
 121content of the framework's codomain is therefore at most countable; the
 122uncountable real line is not required as the home of the constants. -/
 123theorem rs_physics_below_continuum :
 124    (rsField : Set ℝ).Countable
 125      ∧ Real.goldenRatio ∈ rsField
 126      ∧ Real.pi ∈ rsField
 127      ∧ Real.exp 1 ∈ rsField
 128      ∧ alphaInv ∈ rsField
 129      ∧ (rsField : Set ℝ) ≠ Set.univ :=
 130  ⟨rsField_countable, rsField_mem_phi, rsField_mem_pi, rsField_mem_e,
 131    rsField_mem_alphaInv, rsField_proper⟩
 132
 133/-! ### The whole RS scaffold lives in the countable field
 134
 135The constant values are not isolated points. The entire φ-power ladder (the
 136scaffold the RS mass law runs on) and every integer output of the forcing chain
 137are field elements, and the field stays countable no matter how many further
 138constants the framework names. So "RS physics runs on the countable field" is not
 139a slogan about a few values; the working machinery lives there. -/
 140
 141/-- Every integer power of φ lies in the field: the entire φ-ladder, the scaffold
 142of the RS mass law, is countable-field content, not continuum content. -/
 143theorem rsField_phi_zpow (n : ℤ) : Real.goldenRatio ^ n ∈ rsField :=
 144  zpow_mem rsField_mem_phi n
 145
 146/-- The field contains every natural-number value (it contains the prime field). -/
 147theorem rsField_natCast (n : ℕ) : (n : ℝ) ∈ rsField :=
 148  natCast_mem rsField n
 149
 150/-- The eight-tick output (8 = 2³) is a field element. -/
 151theorem rsField_eight_tick : (8 : ℝ) ∈ rsField := by
 152  exact_mod_cast natCast_mem rsField 8
 153
 154/-- The spatial dimension output (D = 3) is a field element. -/
 155theorem rsField_dimension : (3 : ℝ) ∈ rsField := by
 156  exact_mod_cast natCast_mem rsField 3
 157
 158/-- The mass-ladder values `yardstick · φⁿ` lie in the field whenever the
 159yardstick does. With the yardstick itself a constant in the field, every rung of
 160the RS mass spectrum is a countable-field element. -/
 161theorem rsField_mass_ladder {y : ℝ} (hy : y ∈ rsField) (n : ℤ) :
 162    y * Real.goldenRatio ^ n ∈ rsField :=
 163  mul_mem hy (rsField_phi_zpow n)
 164
 165/-- Adjoining any further countable family of constants keeps the field
 166countable. The construction never requires the continuum no matter how many
 167constants RS eventually names. -/
 168theorem rsField_extend_stays_countable {s : Set ℝ} (hs : s.Countable) :
 169    (Subfield.closure (rsConstants ∪ s) : Set ℝ).Countable :=
 170  subfield_closure_countable_of_countable (rsConstants_countable.union hs)
 171
 172/-- **Item 1, sharpened.** The countable RS field carries the working machinery:
 173the φ-ladder for every integer exponent, the chain's integer outputs (eight-tick
 174and dimension), and any countable extension of the constant set, all while staying
 175a proper countable subset of ℝ. -/
 176theorem rs_scaffold_below_continuum :
 177    (∀ n : ℤ, Real.goldenRatio ^ n ∈ rsField)
 178      ∧ (8 : ℝ) ∈ rsField
 179      ∧ (3 : ℝ) ∈ rsField
 180      ∧ (rsField : Set ℝ).Countable
 181      ∧ (rsField : Set ℝ) ≠ Set.univ :=
 182  ⟨rsField_phi_zpow, rsField_eight_tick, rsField_dimension,
 183    rsField_countable, rsField_proper⟩
 184
 185end MinimalField
 186end PrimitiveRecognitionCalculus
 187end Foundation
 188end IndisputableMonolith
 189