IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCChainBridge

   1/-
   2  PrimitiveRecognitionCalculus/PRCChainBridge.lean
   3
   4  Item 3 of the δ frontier: the δ → RS-chain bridge.
   5
   6  The RS forcing chain (T5 unique J → T6 φ → T7 eight-tick → T8 D = 3 → the
   7  constants) is anchored at the recognition cost `Cost.Jcost`. The δ framework
   8  forces the cost FORM (the `cosh(c·t) − 1` gauge family, `Calibration`) and
   9  pins the minimal countable field the constants live in (`MinimalField`). What
  10  was missing was the explicit weld: that the chain's cost entry IS the
  11  calibrated δ cost, and that the chain's first physical output (φ) lives inside
  12  the countable δ field rather than requiring the continuum.
  13
  14  This module supplies that weld:
  15
  16  * `jcost_log_eq_clog_one`:   `Cost.Jcost` in log coordinates is the c = 1
  17                               member of the δ-forced family.
  18  * `jcost_logCurvature_one`:  `Cost.Jcost` is calibrated (log-curvature 1 at the
  19                               unit), i.e. it is exactly the gauge-fixed δ cost.
  20  * `phi_in_minimal_field`:    the T6 output φ lies in the countable RS field.
  21  * `delta_cost_feeds_rs_chain`: the headline weld.
  22
  23  HONEST SCOPING. The φ-forcing itself (every minimal self-similar hierarchy has
  24  base ratio φ) is `UnifiedForcingChain.minimalHierarchy_ratio_eq_phi`, and the
  25  two-sided assembly is `UniversalForcing.OneLaw.one_law_forces_arithmetic_and_phi`.
  26  This module does not re-prove those. It adds the two facts that turn the
  27  assembly into a wiring: (i) the chain's cost is the calibrated δ cost (not just
  28  "the same cost up to a constant c"), and (ii) the φ output is a countable-field
  29  element. The remaining rungs (eight-tick = 2³, D = 3, the transcendental
  30  constants) run downstream of φ on the same field; verifying each output value
  31  is itself a countable-field element is the natural continuation (the eight-tick
  32  and dimension outputs are integers, hence trivially in the field; the
  33  transcendental constants are covered by `MinimalField.rs_physics_below_continuum`).
  34
  35  No project-local axioms. No sorry.
  36-/
  37
  38import Mathlib
  39import IndisputableMonolith.Cost
  40import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationTarget
  41import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMinimalField
  42
  43namespace IndisputableMonolith
  44namespace Foundation
  45namespace PrimitiveRecognitionCalculus
  46namespace ChainBridge
  47
  48/-- `Cost.Jcost` in log coordinates is the `c = 1` member of the δ-forced cost
  49family: `Jcost(eᵗ) = cosh(1·t) − 1`. -/
  50theorem jcost_log_eq_clog_one (t : ℝ) :
  51    Cost.Jcost (Real.exp t) = Real.cosh (1 * t) - 1 := by
  52  simp only [Cost.Jcost, one_mul, Real.cosh_eq, Real.exp_neg]
  53
  54/-- The RS chain's cost entry is the *calibrated* δ cost: its log-curvature at the
  55unit is exactly 1. So `Cost.Jcost` is not merely a member of the δ-forced gauge
  56family; it is the gauge-fixed (unit = 1) member that `Calibration` singles out as
  57J. -/
  58theorem jcost_logCurvature_one :
  59    deriv (deriv (fun t => Cost.Jcost (Real.exp t))) 0 = 1 := by
  60  have hfun : (fun t => Cost.Jcost (Real.exp t))
  61      = (fun t => Real.cosh (1 * t) - 1) := by
  62    funext t; exact jcost_log_eq_clog_one t
  63  rw [hfun, Calibration.logCurvature 1]
  64  norm_num
  65
  66/-- The T6 output φ is a countable-field element: it lives in the minimal RS
  67field, never requiring the uncountable continuum. -/
  68theorem phi_in_minimal_field : Real.goldenRatio ∈ MinimalField.rsField :=
  69  MinimalField.rsField_mem_phi
  70
  71/-- **Item 3 headline (the weld).** The RS forcing chain's cost entry is the
  72calibrated δ cost, and the chain's first physical output φ lives in the countable
  73RS field, which is strictly below the continuum. The chain is therefore fed by the
  74δ cost and runs on a countable carrier at the J and φ rungs. -/
  75theorem delta_cost_feeds_rs_chain :
  76    deriv (deriv (fun t => Cost.Jcost (Real.exp t))) 0 = 1
  77      ∧ Real.goldenRatio ∈ MinimalField.rsField
  78      ∧ (MinimalField.rsField : Set ℝ).Countable :=
  79  ⟨jcost_logCurvature_one, phi_in_minimal_field, MinimalField.rsField_countable⟩
  80
  81/-- **Item 3, sharpened: every chain output lands in the countable field.** The
  82calibrated δ cost feeds the chain, and each of the chain's named outputs, the base
  83ratio φ (T6), the eight-tick cadence 8 = 2³ (T7), and the spatial dimension 3
  84(T8), is an element of the countable RS field. The forcing chain runs end to end on
  85a countable carrier; the continuum is never the home of any rung. -/
  86theorem rs_chain_all_rungs_in_field :
  87    deriv (deriv (fun t => Cost.Jcost (Real.exp t))) 0 = 1
  88      ∧ Real.goldenRatio ∈ MinimalField.rsField
  89      ∧ (8 : ℝ) ∈ MinimalField.rsField
  90      ∧ (3 : ℝ) ∈ MinimalField.rsField
  91      ∧ (MinimalField.rsField : Set ℝ).Countable :=
  92  ⟨jcost_logCurvature_one, phi_in_minimal_field,
  93    MinimalField.rsField_eight_tick, MinimalField.rsField_dimension,
  94    MinimalField.rsField_countable⟩
  95
  96end ChainBridge
  97end PrimitiveRecognitionCalculus
  98end Foundation
  99end IndisputableMonolith
 100