IndisputableMonolith.Constants

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4namespace IndisputableMonolith
   5namespace Constants
   6
   7/-- The fundamental RS time quantum (RS-native). τ₀ = 1 tick. -/
   8@[simp] def tick : ℝ := 1
   9
  10/-- Notation for fundamental tick. -/
  11abbrev τ₀ : ℝ := tick
  12
  13/-- One octave = 8 ticks: the fundamental evolution period. -/
  14def octave : ℝ := 8 * tick
  15
  16/-- Golden ratio φ as a concrete real. -/
  17noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
  18
  19lemma phi_pos : 0 < phi := by
  20  have htwo : 0 < (2 : ℝ) := by norm_num
  21  -- Use that √5 > 0
  22  have hroot_pos : 0 < Real.sqrt 5 := by
  23    have : (0 : ℝ) < 5 := by norm_num
  24    exact Real.sqrt_pos.mpr this
  25  have hnum_pos : 0 < 1 + Real.sqrt 5 := by exact add_pos_of_pos_of_nonneg (by norm_num) (le_of_lt hroot_pos)
  26  simpa [phi] using (div_pos hnum_pos htwo)
  27
  28lemma one_lt_phi : 1 < phi := by
  29  have htwo : 0 < (2 : ℝ) := by norm_num
  30  have hsqrt_gt : Real.sqrt 1 < Real.sqrt 5 := by
  31    simpa [Real.sqrt_one] using (Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 5))
  32  have h2lt : (2 : ℝ) < 1 + Real.sqrt 5 := by
  33    have h1lt : (1 : ℝ) < Real.sqrt 5 := by simpa [Real.sqrt_one] using hsqrt_gt
  34    linarith
  35  have hdiv : (2 : ℝ) / 2 < (1 + Real.sqrt 5) / 2 := (div_lt_div_of_pos_right h2lt htwo)
  36  have hone_lt : 1 < (1 + Real.sqrt 5) / 2 := by simpa using hdiv
  37  simpa [phi] using hone_lt
  38
  39lemma phi_ge_one : 1 ≤ phi := le_of_lt one_lt_phi
  40lemma phi_ne_zero : phi ≠ 0 := ne_of_gt phi_pos
  41lemma phi_ne_one : phi ≠ 1 := ne_of_gt one_lt_phi
  42
  43lemma phi_lt_two : phi < 2 := by
  44  have hsqrt5_lt : Real.sqrt 5 < 3 := by
  45    have h5_lt_9 : (5 : ℝ) < 9 := by norm_num
  46    have h9_eq : Real.sqrt 9 = 3 := by
  47      rw [show (9 : ℝ) = 3^2 by norm_num, Real.sqrt_sq (by norm_num : (3 : ℝ) ≥ 0)]
  48    have : Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) h5_lt_9
  49    rwa [h9_eq] at this
  50  have hnum_lt : 1 + Real.sqrt 5 < 4 := by linarith
  51  have : (1 + Real.sqrt 5) / 2 < 4 / 2 := div_lt_div_of_pos_right hnum_lt (by norm_num)
  52  simp only [phi]
  53  linarith
  54
  55/-! ### φ irrationality -/
  56
  57/-- φ is irrational (degree 2 algebraic, not rational).
  58
  59    Proof: Our φ equals Mathlib's golden ratio, which is proven irrational
  60    via the irrationality of √5 (5 is prime, hence not a perfect square). -/
  61theorem phi_irrational : Irrational phi := by
  62  -- Our phi equals Mathlib's goldenRatio
  63  have h_eq : phi = Real.goldenRatio := rfl
  64  rw [h_eq]
  65  exact Real.goldenRatio_irrational
  66
  67/-! ### φ power bounds -/
  68
  69/-- Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0). -/
  70lemma phi_sq_eq : phi^2 = phi + 1 := by
  71  simp only [phi]
  72  have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
  73  have hsq : (Real.sqrt 5)^2 = 5 := Real.sq_sqrt h5_pos
  74  ring_nf
  75  linear_combination (1/4) * hsq
  76
  77/-- Tighter lower bound: φ > 1.5 (since √5 > 2, so (1 + √5)/2 > 1.5). -/
  78lemma phi_gt_onePointFive : (1.5 : ℝ) < phi := by
  79  simp only [phi]
  80  have h5 : (2 : ℝ) < Real.sqrt 5 := by
  81    have h : (2 : ℝ)^2 < 5 := by norm_num
  82    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  83    exact Real.sqrt_lt_sqrt (by norm_num) h
  84  linarith
  85
  86/-- Tighter upper bound: φ < 1.62 (since √5 < 2.24). -/
  87lemma phi_lt_onePointSixTwo : phi < (1.62 : ℝ) := by
  88  simp only [phi]
  89  have h5 : Real.sqrt 5 < (2.24 : ℝ) := by
  90    have h : (5 : ℝ) < (2.24 : ℝ)^2 := by norm_num
  91    have h24_pos : (0 : ℝ) ≤ 2.24 := by norm_num
  92    rw [← Real.sqrt_sq h24_pos]
  93    exact Real.sqrt_lt_sqrt (by norm_num) h
  94  linarith
  95
  96/-- Even tighter lower bound: φ > 1.61. -/
  97lemma phi_gt_onePointSixOne : (1.61 : ℝ) < phi := by
  98  simp only [phi]
  99  have h5 : (2.22 : ℝ) < Real.sqrt 5 := by
 100    have h : (2.22 : ℝ)^2 < 5 := by norm_num
 101    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.22)]
 102    exact Real.sqrt_lt_sqrt (by norm_num) h
 103  linarith
 104
 105/-- φ² is between 2.5 and 2.7.
 106    φ² = φ + 1 ≈ 2.618 (exact: (3 + √5)/2). -/
 107lemma phi_squared_bounds : (2.5 : ℝ) < phi^2 ∧ phi^2 < 2.7 := by
 108  rw [phi_sq_eq]
 109  have h1 := phi_gt_onePointFive
 110  have h2 := phi_lt_onePointSixTwo
 111  constructor <;> linarith
 112
 113/-! ### Fibonacci power identities for φ -/
 114
 115/-- Key identity: φ³ = 2φ + 1 (Fibonacci recurrence).
 116    φ³ = φ × φ² = φ(φ + 1) = φ² + φ = (φ + 1) + φ = 2φ + 1. -/
 117lemma phi_cubed_eq : phi^3 = 2 * phi + 1 := by
 118  calc phi^3 = phi * phi^2 := by ring
 119    _ = phi * (phi + 1) := by rw [phi_sq_eq]
 120    _ = phi^2 + phi := by ring
 121    _ = (phi + 1) + phi := by rw [phi_sq_eq]
 122    _ = 2 * phi + 1 := by ring
 123
 124/-- Key identity: φ⁴ = 3φ + 2 (Fibonacci recurrence).
 125    φ⁴ = φ × φ³ = φ(2φ + 1) = 2φ² + φ = 2(φ + 1) + φ = 3φ + 2. -/
 126lemma phi_fourth_eq : phi^4 = 3 * phi + 2 := by
 127  calc phi^4 = phi * phi^3 := by ring
 128    _ = phi * (2 * phi + 1) := by rw [phi_cubed_eq]
 129    _ = 2 * phi^2 + phi := by ring
 130    _ = 2 * (phi + 1) + phi := by rw [phi_sq_eq]
 131    _ = 3 * phi + 2 := by ring
 132
 133/-- Key identity: φ⁵ = 5φ + 3 (Fibonacci recurrence).
 134    φ⁵ = φ × φ⁴ = φ(3φ + 2) = 3φ² + 2φ = 3(φ + 1) + 2φ = 5φ + 3. -/
 135lemma phi_fifth_eq : phi^5 = 5 * phi + 3 := by
 136  calc phi^5 = phi * phi^4 := by ring
 137    _ = phi * (3 * phi + 2) := by rw [phi_fourth_eq]
 138    _ = 3 * phi^2 + 2 * phi := by ring
 139    _ = 3 * (phi + 1) + 2 * phi := by rw [phi_sq_eq]
 140    _ = 5 * phi + 3 := by ring
 141
 142/-! ### Bounds from Fibonacci identities -/
 143
 144/-- φ³ is between 4.0 and 4.25.
 145    φ³ = 2φ + 1 ≈ 4.236. -/
 146lemma phi_cubed_bounds : (4.0 : ℝ) < phi^3 ∧ phi^3 < 4.25 := by
 147  rw [phi_cubed_eq]
 148  have h1 := phi_gt_onePointFive
 149  have h2 := phi_lt_onePointSixTwo
 150  constructor <;> linarith
 151
 152/-- φ⁴ is between 6.5 and 6.9.
 153    φ⁴ = 3φ + 2 ≈ 6.854. -/
 154lemma phi_fourth_bounds : (6.5 : ℝ) < phi^4 ∧ phi^4 < 6.9 := by
 155  rw [phi_fourth_eq]
 156  have h1 := phi_gt_onePointFive
 157  have h2 := phi_lt_onePointSixTwo
 158  constructor <;> linarith
 159
 160/-- φ⁵ is between 10.7 and 11.3.
 161    φ⁵ = 5φ + 3 ≈ 11.090. -/
 162lemma phi_fifth_bounds : (10.7 : ℝ) < phi^5 ∧ phi^5 < 11.3 := by
 163  rw [phi_fifth_eq]
 164  have h1 := phi_gt_onePointSixOne
 165  have h2 := phi_lt_onePointSixTwo
 166  constructor <;> linarith
 167
 168/-- Key identity: φ⁶ = 8φ + 5 (Fibonacci recurrence). -/
 169lemma phi_sixth_eq : phi^6 = 8 * phi + 5 := by
 170  calc phi^6 = phi * phi^5 := by ring
 171    _ = phi * (5 * phi + 3) := by rw [phi_fifth_eq]
 172    _ = 5 * phi^2 + 3 * phi := by ring
 173    _ = 5 * (phi + 1) + 3 * phi := by rw [phi_sq_eq]
 174    _ = 8 * phi + 5 := by ring
 175
 176/-- Key identity: φ⁷ = 13φ + 8 (Fibonacci recurrence). -/
 177lemma phi_seventh_eq : phi^7 = 13 * phi + 8 := by
 178  calc phi^7 = phi * phi^6 := by ring
 179    _ = phi * (8 * phi + 5) := by rw [phi_sixth_eq]
 180    _ = 8 * phi^2 + 5 * phi := by ring
 181    _ = 8 * (phi + 1) + 5 * phi := by rw [phi_sq_eq]
 182    _ = 13 * phi + 8 := by ring
 183
 184/-- Key identity: φ⁸ = 21φ + 13 (Fibonacci recurrence). -/
 185lemma phi_eighth_eq : phi^8 = 21 * phi + 13 := by
 186  calc phi^8 = phi * phi^7 := by ring
 187    _ = phi * (13 * phi + 8) := by rw [phi_seventh_eq]
 188    _ = 13 * phi^2 + 8 * phi := by ring
 189    _ = 13 * (phi + 1) + 8 * phi := by rw [phi_sq_eq]
 190    _ = 21 * phi + 13 := by ring
 191
 192/-- Key identity: φ⁹ = 34φ + 21 (Fibonacci recurrence). -/
 193lemma phi_ninth_eq : phi^9 = 34 * phi + 21 := by
 194  calc phi^9 = phi * phi^8 := by ring
 195    _ = phi * (21 * phi + 13) := by rw [phi_eighth_eq]
 196    _ = 21 * phi^2 + 13 * phi := by ring
 197    _ = 21 * (phi + 1) + 13 * phi := by rw [phi_sq_eq]
 198    _ = 34 * phi + 21 := by ring
 199
 200/-- Key identity: φ¹⁰ = 55φ + 34 (Fibonacci recurrence). -/
 201lemma phi_tenth_eq : phi^10 = 55 * phi + 34 := by
 202  calc phi^10 = phi * phi^9 := by ring
 203    _ = phi * (34 * phi + 21) := by rw [phi_ninth_eq]
 204    _ = 34 * phi^2 + 21 * phi := by ring
 205    _ = 34 * (phi + 1) + 21 * phi := by rw [phi_sq_eq]
 206    _ = 55 * phi + 34 := by ring
 207
 208/-- Key identity: φ¹¹ = 89φ + 55 (Fibonacci recurrence). -/
 209lemma phi_eleventh_eq : phi^11 = 89 * phi + 55 := by
 210  calc phi^11 = phi * phi^10 := by ring
 211    _ = phi * (55 * phi + 34) := by rw [phi_tenth_eq]
 212    _ = 55 * phi^2 + 34 * phi := by ring
 213    _ = 55 * (phi + 1) + 34 * phi := by rw [phi_sq_eq]
 214    _ = 89 * phi + 55 := by ring
 215
 216/-! ### Canonical constants derived from φ -/
 217
 218/-- Canonical locked fine-structure constant: α_lock = (1 − 1/φ)/2. -/
 219@[simp] noncomputable def alphaLock : ℝ := (1 - 1 / phi) / 2
 220
 221/-- Useful bridge identity: the “acceleration-parameterized” exponent is `2·alphaLock`.
 222
 223This is purely algebraic (no physics): it just clears the `/2` in the definition. -/
 224lemma two_mul_alphaLock : 2 * alphaLock = 1 - 1 / phi := by
 225  unfold alphaLock
 226  ring_nf
 227
 228lemma alphaLock_pos : 0 < alphaLock := by
 229  have hphi := one_lt_phi
 230  unfold alphaLock
 231  have : 1 / phi < 1 := (div_lt_one phi_pos).mpr hphi
 232  linarith
 233
 234lemma alphaLock_lt_one : alphaLock < 1 := by
 235  have hpos : 0 < phi := phi_pos
 236  unfold alphaLock
 237  have : 1 / phi > 0 := one_div_pos.mpr hpos
 238  linarith
 239
 240/-- Canonical locked C_lag constant: C_lock = φ^{−5}. -/
 241@[simp] noncomputable def cLagLock : ℝ := phi ^ (-(5 : ℝ))
 242
 243lemma cLagLock_pos : 0 < cLagLock := by
 244  have hphi : 0 < phi := phi_pos
 245  unfold cLagLock
 246  exact Real.rpow_pos_of_pos hphi (-(5 : ℝ))
 247
 248/-- The elementary ledger bit cost J_bit = ln φ. -/
 249noncomputable def J_bit : ℝ := Real.log phi
 250
 251/-- Coherence energy in RS units (dimensionless).
 252    By Phase 2 derivation, E_coh = C_lock = φ⁻⁵. -/
 253noncomputable def E_coh : ℝ := cLagLock
 254
 255lemma E_coh_pos : 0 < E_coh := cLagLock_pos
 256
 257/-! ### RS-native fundamental units (parameter-free)
 258
 259The **core theory** is expressed in RS-native units:
 260
 261- `tau0 = 1` tick (time quantum)
 262- `ell0 = 1` voxel (length quantum)
 263- `c = 1` voxel/tick
 264
 265All SI/CODATA anchoring is treated as **external calibration** and lives in
 266separate modules (e.g. `IndisputableMonolith.Constants.Consistency`,
 267`IndisputableMonolith.Constants.Derivation`, `IndisputableMonolith.Constants.Codata`,
 268and `IndisputableMonolith.Constants.RSNativeUnits`). -/
 269
 270/-- The fundamental time unit τ₀ (duration of one tick) in RS-native units. -/
 271@[simp] noncomputable def tau0 : ℝ := tick
 272
 273lemma tau0_pos : 0 < tau0 := by
 274  simp [tau0, tick]
 275
 276/-! ## C-004: Planck's Constant ħ Derivation
 277
 278### The RS Derivation of ħ
 279
 280In Recognition Science, the reduced Planck constant ℏ is not a free parameter
 281but is derived from the fundamental ledger structure:
 282
 2831. **Coherence Energy** (E_coh): The minimal energy quantum for recognition events
 284   E_coh = φ⁻⁵ (from self-similar reciprocal closure on the discrete ledger)
 285
 2862. **Fundamental Time** (τ₀): The duration of one recognition tick
 287   τ₀ = 1 tick (the atomic unit of time in RS)
 288
 2893. **Planck's Identity**: ℏ = E_coh · τ₀ = φ⁻⁵ · 1 = φ⁻⁵
 290
 291This derivation has **zero free parameters** — both E_coh and τ₀ are forced
 292by the RS forcing chain (T0-T8).
 293
 294**Physical Interpretation**: ℏ represents the minimal "action" (energy × time)
 295required for a single recognition event in the ledger. The smallness of ℏ
 296(≈ 0.09 in RS-native units, or ~10⁻³⁴ J·s in SI) reflects the fine-grained
 297nature of the recognition substrate.
 298
 299**SI Conversion**: When mapping to SI units, ℏ acquires its familiar value
 300through the calibration length λ_rec:
 301   ℏ_SI = E_coh_SI · τ₀_SI = (φ⁻⁵ · ℏ_base) · (λ_rec/c)
 302where ℏ_base is the natural unit conversion factor.
 303-/
 304
 305/-- Reduced Planck constant ħ in RS-native units: ħ = E_coh · τ₀ = φ⁻⁵ · 1. -/
 306noncomputable def hbar : ℝ := cLagLock * tau0
 307
 308lemma hbar_pos : 0 < hbar := mul_pos cLagLock_pos tau0_pos
 309
 310/-- **THEOREM C-004.1**: ℏ = φ⁻⁵ in RS-native units.
 311
 312    This is the fundamental identity: ℏ = E_coh · τ₀ = φ⁻⁵ · 1 = φ⁻⁵. -/
 313lemma hbar_eq_phi_inv_fifth : hbar = phi ^ (-(5 : ℝ)) := by
 314  unfold hbar cLagLock tau0 tick
 315  simp
 316
 317/-- **THEOREM C-004.2**: ℏ is positive (required for quantum dynamics). -/
 318theorem hbar_positive : hbar > 0 := hbar_pos
 319
 320/-- **THEOREM C-004.3**: ℏ < 1 (the action quantum is small compared to natural units).
 321
 322    Proof: φ > 1 ⟹ φ⁵ > 1 ⟹ φ⁻⁵ < 1. -/
 323theorem hbar_lt_one : hbar < 1 := by
 324  rw [hbar_eq_phi_inv_fifth]
 325  have h1 : phi ^ (5 : ℝ) > 1 := by
 326    have hphi : phi > 1 := one_lt_phi
 327    have hexp : (5 : ℝ) > 0 := by norm_num
 328    have h1_lt : (1 : ℝ) < phi ^ (5 : ℝ) := by
 329      rw [← Real.one_rpow (5 : ℝ)]
 330      apply Real.rpow_lt_rpow
 331      · norm_num
 332      · linarith
 333      · norm_num
 334    linarith
 335  have h2 : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
 336    rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
 337    rw [Real.rpow_neg]
 338    · ring
 339    · exact le_of_lt phi_pos
 340  rw [h2]
 341  have h3 : phi ^ (5 : ℝ) > 0 := by positivity
 342  apply (div_lt_iff₀ h3).mpr
 343  linarith
 344
 345/-- **THEOREM C-004.4**: ℏ = E_coh · τ₀ (the action quantum identity).
 346
 347    This is the fundamental physical interpretation: Planck's constant
 348    is the minimal action (energy × time) for a recognition event. -/
 349theorem hbar_action_identity : hbar = E_coh * tau0 := rfl
 350
 351/-- **THEOREM C-004.5**: Bounds on ℏ from φ bounds.
 352
 353    With φ ∈ (1.61, 1.62), we get ℏ ∈ (0.088, 0.093). -/
 354theorem hbar_bounds : (0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ) := by
 355  rw [hbar_eq_phi_inv_fifth]
 356  have h1 : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
 357  have h2 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
 358  -- We want 0.088 < φ^(-5) < 0.093
 359  -- Since hbar = 1/φ^5, we need bounds on φ^5
 360  -- Lower bound: φ < 1.62, so φ^5 < 1.62^5, so 1/φ^5 > 1/1.62^5
 361  -- Upper bound: φ > 1.61, so φ^5 > 1.61^5, so 1/φ^5 < 1/1.61^5
 362  have h_phi5_lower : phi ^ (5 : ℝ) > (1.61 : ℝ) ^ (5 : ℝ) := by
 363    apply Real.rpow_lt_rpow
 364    · linarith
 365    · linarith
 366    · norm_num
 367  have h_phi5_upper : phi ^ (5 : ℝ) < (1.62 : ℝ) ^ (5 : ℝ) := by
 368    apply Real.rpow_lt_rpow
 369    · linarith
 370    · linarith
 371    · norm_num
 372  -- Convert to hbar = φ^(-5) bounds
 373  have hbar_lower : phi ^ (-(5 : ℝ)) > (0.088 : ℝ) := by
 374    have h_inv : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
 375      rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
 376      rw [Real.rpow_neg]
 377      · ring
 378      · exact le_of_lt phi_pos
 379    rw [h_inv]
 380    -- Since φ^5 < 1.62^5, we have 1/φ^5 > 1/1.62^5
 381    -- Compute 1.62^5 = 11.158... and 1/11.158 ≈ 0.0896 > 0.088
 382    have h_div : 1 / (phi ^ (5 : ℝ)) > 1 / ((1.62 : ℝ) ^ (5 : ℝ)) := by
 383      apply (one_div_lt_one_div (by positivity) (by positivity)).mpr
 384      linarith [h_phi5_upper]
 385    have h_numeric : 1 / ((1.62 : ℝ) ^ (5 : ℝ)) > (0.088 : ℝ) := by
 386      rw [show (5 : ℝ) = (5 : ℕ) by norm_num, Real.rpow_natCast]
 387      norm_num
 388    linarith
 389  have hbar_upper : phi ^ (-(5 : ℝ)) < (0.093 : ℝ) := by
 390    have h_inv : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
 391      rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
 392      rw [Real.rpow_neg]
 393      · ring
 394      · exact le_of_lt phi_pos
 395    rw [h_inv]
 396    -- Since φ^5 > 1.61^5, we have 1/φ^5 < 1/1.61^5
 397    -- Compute 1.61^5 = 10.817... and 1/10.817 ≈ 0.0924 < 0.093
 398    have h_div : 1 / (phi ^ (5 : ℝ)) < 1 / ((1.61 : ℝ) ^ (5 : ℝ)) := by
 399      apply (div_lt_div_iff₀ (by positivity) (by positivity)).mpr
 400      linarith [h_phi5_lower]
 401    have h_numeric : 1 / ((1.61 : ℝ) ^ (5 : ℝ)) < (0.093 : ℝ) := by
 402      rw [show (5 : ℝ) = (5 : ℕ) by norm_num, Real.rpow_natCast]
 403      norm_num
 404    linarith
 405  exact ⟨hbar_lower, hbar_upper⟩
 406
 407/-- The speed of light c in RS-native units (voxel/tick). -/
 408@[simp] noncomputable def c : ℝ := 1
 409
 410lemma c_pos : 0 < c := by
 411  simp [c]
 412
 413/-- The fundamental length unit ℓ₀ in RS-native units (voxel). -/
 414@[simp] noncomputable def ell0 : ℝ := 1
 415
 416lemma ell0_pos : 0 < ell0 := by
 417  simp [ell0]
 418
 419/-- Light-cone identity: ℓ₀ = c · τ₀ (in RS-native units). -/
 420lemma c_ell0_tau0 : c * tau0 = ell0 := by
 421  simp [c, tau0, ell0, tick]
 422
 423/-- Fundamental recognition wavelength λ_rec.
 424    In the 8-tick cycle, λ_rec = ℓ₀ (in RS-native units). -/
 425noncomputable def lambda_rec : ℝ := ell0
 426
 427lemma lambda_rec_pos : 0 < lambda_rec := by
 428  simp [lambda_rec]
 429
 430/-- Newton's gravitational constant G derived from first principles (RS-native form).
 431    \(G = \lambda_{\text{rec}}^2 c^3 / (\pi \hbar)\). -/
 432noncomputable def G : ℝ := (lambda_rec^2) * (c^3) / (Real.pi * hbar)
 433
 434lemma G_pos : 0 < G := by
 435  unfold G
 436  apply div_pos
 437  · apply mul_pos
 438    · exact pow_pos lambda_rec_pos 2
 439    · exact pow_pos c_pos 3
 440  · apply mul_pos
 441    · exact Real.pi_pos
 442    · exact hbar_pos
 443
 444/-- Einstein coupling constant κ = 8πG/c⁴ in RS-native units.
 445    Using G = λ_rec² c³ / (π ℏ) with λ_rec = c = 1 and ℏ = φ⁻⁵:
 446    κ = 8π · (φ⁵/π) / 1 = 8φ⁵.
 447
 448    This is the coefficient in front of T_μν in the Einstein field equations. -/
 449noncomputable def kappa_einstein : ℝ := 8 * Real.pi * G / (c^4)
 450
 451lemma kappa_einstein_eq : kappa_einstein = 8 * phi ^ (5 : ℝ) := by
 452  unfold kappa_einstein G hbar cLagLock lambda_rec ell0 c tau0 tick
 453  simp only [one_pow, mul_one, div_one]
 454  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 455  field_simp [hpi]
 456  rw [Real.rpow_neg phi_pos.le]
 457  field_simp [phi_ne_zero]
 458
 459lemma kappa_einstein_pos : 0 < kappa_einstein := by
 460  unfold kappa_einstein
 461  apply div_pos
 462  · apply mul_pos
 463    · apply mul_pos
 464      · norm_num
 465      · exact Real.pi_pos
 466    · exact G_pos
 467  · exact pow_pos c_pos 4
 468
 469/-!
 470  ## CODATA / SI constants (quarantined)
 471
 472  The empirical SI/CODATA numeric constants live in
 473  `IndisputableMonolith/Constants/Codata.lean` and are intentionally **excluded**
 474  from the certified surface import-closure.
 475
 476  If you need them for numeric comparisons or empirical reports, import
 477  `IndisputableMonolith.Constants.Codata` explicitly.
 478-/
 479
 480/-- Minimal RS units used in Core. -/
 481structure RSUnits where
 482  tau0 : ℝ
 483  ell0 : ℝ
 484  c    : ℝ
 485  c_ell0_tau0 : c * tau0 = ell0
 486
 487/-- Dimensionless bridge ratio \(K\).
 488
 489Defined (non-circularly) as \(K = \varphi^{1/2}\). -/
 490@[simp] noncomputable def K : ℝ := phi ^ (1/2 : ℝ)
 491
 492@[simp] lemma K_def : K = phi ^ (1/2 : ℝ) := rfl
 493
 494lemma K_pos : 0 < K := by
 495  -- φ > 0, hence φ^(1/2) > 0
 496  simpa [K] using Real.rpow_pos_of_pos phi_pos (1/2 : ℝ)
 497
 498lemma K_nonneg : 0 ≤ K := le_of_lt K_pos
 499
 500/-- Alias matching parallel-work naming convention. -/
 501lemma one_lt_phiPointSixOne : (1.6 : ℝ) < phi := by linarith [phi_gt_onePointSixOne]
 502
 503/-- Alias: phi_gt_one ≡ one_lt_phi, for parallel-work compat. -/
 504lemma phi_gt_one : 1 < phi := one_lt_phi
 505
 506/-- φ ≈ 1.618 (coarse upper bound used in some modules). -/
 507lemma phi_approx : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
 508
 509/-- J(φ) = φ - 3/2 (exact, using φ² = φ + 1). -/
 510lemma Jcost_phi_val : Cost.Jcost phi = phi - 3 / 2 := by
 511  rw [Cost.Jcost_eq_sq phi_ne_zero]
 512  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
 513  rw [div_eq_iff (by linarith [phi_pos] : 2 * phi ≠ 0)]
 514  nlinarith [phi_pos, hphi_sq]
 515
 516/-- J(φ) > 0 -/
 517lemma Jcost_phi_pos : 0 < Cost.Jcost phi :=
 518  Cost.Jcost_pos_of_ne_one _ phi_pos phi_ne_one
 519
 520end Constants
 521end IndisputableMonolith
 522