IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.GenerableReal

   1/-
   2  PrimitiveRecognitionCalculus/GenerableReal.lean
   3
   4  Phase 2 of the Delta-Native Analysis frontier: the generable reals.
   5
   6  The protocol-reals of `DeltaReal` are the analysis interface, and their value
   7  map lands onto all of ℝ (`Protocol.value_surjective`). That surjection is the
   8  display: the full classical continuum is reachable as protocol values. But the
   9  ontology physics actually uses is smaller. The generable reals are the ones
  10  produced from a countable family of named constants by the field operations.
  11  They are countable, hence a proper subset of ℝ.
  12
  13  This is the anti-smuggling guard. It pins exactly where uncountability is a
  14  formal display artifact (the protocol value map onto ℝ) and where finite
  15  generation lives (the countable generable field).
  16
  17  What is proved (relative to a countable constant family `κ : ℕ → ℝ`):
  18
  19  * `genField_countable` : the generable reals are countable;
  20  * `rat_mem`, `const_mem` : ℚ and every named constant are generable;
  21  * closure under `+`, `-`, `*`, `⁻¹` (the field operations RS uses);
  22  * `genField_proper` : the generable reals are a proper subset of ℝ;
  23  * `display_exceeds_generation` : THE guard. There is a real that is a protocol
  24    value (reachable by the analysis display) yet not generable. The continuum the
  25    display reaches strictly exceeds the countable ontology, so any apparent need
  26    for uncountably many reals is display, not generation.
  27
  28  Reuses `MinimalField.subfield_closure_countable_of_countable` and
  29  `DeltaReal.Protocol.value_surjective`.
  30
  31  No project-local axioms. No sorry.
  32-/
  33
  34import Mathlib
  35import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMinimalField
  36import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal
  37
  38namespace IndisputableMonolith
  39namespace Foundation
  40namespace PrimitiveRecognitionCalculus
  41namespace GenerableReal
  42
  43/-- The generable reals relative to a countable family of named constants `κ`:
  44the subfield of ℝ generated by the constants. Equivalently, everything obtainable
  45from the constants and rationals by finitely many field operations. -/
  46noncomputable def genField (κ : ℕ → ℝ) : Subfield ℝ := Subfield.closure (Set.range κ)
  47
  48/-- The generable reals are countable: only countably many finite descriptions
  49exist. -/
  50theorem genField_countable (κ : ℕ → ℝ) : (genField κ : Set ℝ).Countable :=
  51  MinimalField.subfield_closure_countable_of_countable (Set.countable_range κ)
  52
  53/-- Every rational is generable (the prime field sits inside). -/
  54theorem rat_mem (κ : ℕ → ℝ) (q : ℚ) : (q : ℝ) ∈ genField κ :=
  55  SubfieldClass.ratCast_mem (genField κ) q
  56
  57/-- Every named constant is generable. -/
  58theorem const_mem (κ : ℕ → ℝ) (n : ℕ) : κ n ∈ genField κ :=
  59  Subfield.subset_closure ⟨n, rfl⟩
  60
  61/-- The generable reals are a proper subset of ℝ: countability rules out the whole
  62continuum. -/
  63theorem genField_proper (κ : ℕ → ℝ) : (genField κ : Set ℝ) ≠ Set.univ := by
  64  intro h
  65  exact Cardinal.not_countable_real (h ▸ genField_countable κ)
  66
  67/-- **Phase 2 headline: display exceeds generation.** For any countable constant
  68family, there is a real that is the value of a Delta-real protocol (so the
  69analysis display reaches it) yet is not generable. The protocol value map lands
  70onto the full continuum, while the ontology is the countable generable field; the
  71gap is exactly the reals that exist only as display, never as finite generation.
  72This is the guard against smuggling uncountable ontology in through the analysis
  73interface. -/
  74theorem display_exceeds_generation (κ : ℕ → ℝ) :
  75    ∃ r : ℝ, (∃ x : DeltaReal.Protocol, x.value = r) ∧ r ∉ genField κ := by
  76  obtain ⟨r, hr⟩ := (Set.ne_univ_iff_exists_notMem _).mp (genField_proper κ)
  77  exact ⟨r, DeltaReal.Protocol.value_surjective r, hr⟩
  78
  79/-- The generable field is closed under the field operations and contains the
  80rationals and the named constants: it is a genuine operational carrier, not a bare
  81set. -/
  82theorem genField_is_operational_carrier (κ : ℕ → ℝ) :
  83    (∀ q : ℚ, (q : ℝ) ∈ genField κ)
  84      ∧ (∀ n : ℕ, κ n ∈ genField κ)
  85      ∧ (∀ a b : ℝ, a ∈ genField κ → b ∈ genField κ → a + b ∈ genField κ)
  86      ∧ (∀ a b : ℝ, a ∈ genField κ → b ∈ genField κ → a * b ∈ genField κ)
  87      ∧ (∀ a : ℝ, a ∈ genField κ → -a ∈ genField κ)
  88      ∧ (∀ a : ℝ, a ∈ genField κ → a⁻¹ ∈ genField κ)
  89      ∧ (genField κ : Set ℝ).Countable :=
  90  ⟨rat_mem κ, const_mem κ,
  91    fun _ _ ha hb => add_mem ha hb, fun _ _ ha hb => mul_mem ha hb,
  92    fun _ ha => neg_mem ha, fun _ ha => inv_mem ha, genField_countable κ⟩
  93
  94end GenerableReal
  95end PrimitiveRecognitionCalculus
  96end Foundation
  97end IndisputableMonolith
  98