IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCostOnField

   1/-
   2  PrimitiveRecognitionCalculus/PRCCostOnField.lean
   3
   4  Items 1 + 3 of the δ frontier, unified: the cost function and every physics
   5  constant share ONE countable field.
   6
   7  Two strands had been proved separately:
   8
   9  * `PRCExpLogField`: a single countable subfield `T ⊂ ℝ`, closed under field
  10    operations and `exp`/`log`, containing π, φ, e, and α⁻¹. The CONSTANTS live there.
  11  * `PRCChainBridge`: the RS chain's cost entry is the calibrated δ cost
  12    `Cost.Jcost`. The COST FORM is fixed.
  13
  14  What was missing is the weld between them: that the canonical cost function itself
  15  maps the countable field into the countable field, so the cost SIDE and the
  16  constant SIDE are not two different carriers but one. This module supplies it.
  17
  18  `Cost.Jcost x = (x + x⁻¹)/2 − 1` is a field expression, so on any subfield it is
  19  closed:
  20
  21  * `jcost_mem_T`: `x ∈ T → Cost.Jcost x ∈ T`.
  22  * `jcost_iterate_mem_T`: the entire forward orbit of a `T`-point under repeated
  23    cost evaluation stays in `T`. The recognition COST DYNAMICS never leave the
  24    countable field.
  25  * `cost_and_constants_share_one_countable_field`: ONE countable field `T`, strictly
  26    below the continuum, that is closed under field operations, `exp`, `log`, AND the
  27    canonical cost `Jcost`, and already contains π, φ, e, and α⁻¹.
  28
  29  This is the end-to-end form of Item 3 ("the RS chain running on the countable field
  30  fed by the δ cost"): the cost function, the operations the constants are built
  31  from, and the constants themselves all live on a single countable carrier. The
  32  continuum is required nowhere in the loop, only (at most) as the ambient where the
  33  standard `exp`/`log` are written down.
  34
  35  No project-local axioms. No sorry.
  36-/
  37
  38import IndisputableMonolith.Cost
  39import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCExpLogField
  40
  41namespace IndisputableMonolith
  42namespace Foundation
  43namespace PrimitiveRecognitionCalculus
  44namespace CostOnField
  45
  46open ExpLogField
  47
  48/-- The canonical cost `Cost.Jcost x = (x + x⁻¹)/2 − 1` maps the countable field `T`
  49into itself: it is a field expression, and `T` is a subfield (closed under `+`, `⁻¹`,
  50`/`, `−`, and containing `1` and `2`). No positivity or nonzero hypothesis is needed,
  51because `Subfield` inversion is total (`0⁻¹ = 0`). -/
  52theorem jcost_mem_T {x : ℝ} (hx : x ∈ T) : Cost.Jcost x ∈ T := by
  53  have h2 : (2 : ℝ) ∈ T := by exact_mod_cast natCast_mem T 2
  54  unfold Cost.Jcost
  55  exact sub_mem (div_mem (add_mem hx (inv_mem hx)) h2) (one_mem _)
  56
  57/-- **The cost dynamics stay countable.** The entire forward orbit of any
  58`T`-element under repeated application of the cost function remains in `T`. Iterating
  59recognition cost never escapes the countable field. -/
  60theorem jcost_iterate_mem_T {x : ℝ} (hx : x ∈ T) (n : ℕ) :
  61    (Cost.Jcost^[n] x) ∈ T := by
  62  induction n with
  63  | zero => simpa using hx
  64  | succ k ih =>
  65      rw [Function.iterate_succ_apply']
  66      exact jcost_mem_T ih
  67
  68/-- The cost of every named constant is itself a `T`-element. -/
  69theorem jcost_pi_mem_T : Cost.Jcost Real.pi ∈ T := jcost_mem_T pi_mem_T
  70theorem jcost_phi_mem_T : Cost.Jcost Real.goldenRatio ∈ T := jcost_mem_T phi_mem_T
  71theorem jcost_alphaInv_mem_T : Cost.Jcost MinimalField.alphaInv ∈ T :=
  72  jcost_mem_T alphaInv_mem_T
  73
  74/-- **The unified headline (Items 1 + 3).** There is ONE countable subfield `T` of ℝ,
  75strictly below the continuum, that simultaneously
  76  * is closed under field operations, `exp`, and `log`;
  77  * is closed under the canonical recognition cost `Cost.Jcost`;
  78  * contains the seeds π and φ and the derived constants `e` and `α⁻¹`.
  79The cost function, the operations the constants are built from, and the constants
  80themselves therefore share a single countable carrier. "A single primitive for
  81physics runs on the countable field fed by the δ cost" is literally true: nowhere in
  82the cost-and-constants loop is the uncountable continuum required. -/
  83theorem cost_and_constants_share_one_countable_field :
  84    ∃ K : Subfield ℝ,
  85      (K : Set ℝ).Countable
  86        ∧ (∀ x ∈ K, Real.exp x ∈ K)
  87        ∧ (∀ x ∈ K, Real.log x ∈ K)
  88        ∧ (∀ x ∈ K, Cost.Jcost x ∈ K)
  89        ∧ Real.pi ∈ K
  90        ∧ Real.goldenRatio ∈ K
  91        ∧ Real.exp 1 ∈ K
  92        ∧ MinimalField.alphaInv ∈ K
  93        ∧ (K : Set ℝ) ≠ Set.univ :=
  94  ⟨T, T_countable,
  95    fun _ hx => T_exp_closed hx,
  96    fun _ hx => T_log_closed hx,
  97    fun _ hx => jcost_mem_T hx,
  98    pi_mem_T, phi_mem_T, e_mem_T, alphaInv_mem_T, T_proper⟩
  99
 100end CostOnField
 101end PrimitiveRecognitionCalculus
 102end Foundation
 103end IndisputableMonolith
 104