X_opt

formal source

  75/-- The optimal recognition ratio: X_opt = φ/π.
  76    This is the ratio at which recognition cost and geometric constraint
  77    are in balance. -/
  78noncomputable def X_opt : ℝ := phi / Real.pi
  79
  80theorem X_opt_pos : 0 < X_opt := div_pos phi_pos Real.pi_pos
  81
  82/-- The log-periodic modulation frequency:
  83    Ω₀ = 2π / ln(1/X_opt) = 2π / ln(π/φ).
  84    Numerically: π/φ ≈ 1.942, ln(1.942) ≈ 0.664, so Ω₀ ≈ 9.47.
  85
  86    This produces oscillations in the primordial power spectrum
  87    with period Δln(k) = 2π/Ω₀ ≈ 0.664. -/
  88noncomputable def Omega_0 : ℝ := 2 * Real.pi / Real.log (Real.pi / phi)
  89
  90/-- Ω₀ is positive (π/φ > 1, so ln(π/φ) > 0). -/
  91theorem Omega_0_pos : 0 < Omega_0 := by
  92  unfold Omega_0
  93  apply div_pos (mul_pos (by norm_num) Real.pi_pos)
  94  apply Real.log_pos
  95  rw [one_lt_div phi_pos]
  96  exact lt_of_lt_of_le (by linarith [phi_lt_two]) (le_of_lt Real.pi_gt_three)
  97
  98/-! ## UV Knee -/
  99
 100/-- The UV knee (comoving): k_rec,com ≈ 1.4 × 10⁶ Mpc⁻¹.
 101    Above this scale, the recognition lattice structure becomes visible
 102    and the primordial spectrum softens. -/
 103def k_rec_com : ℝ := 1.4e6
 104
 105/-- The curvature bound at the recognition event R0:
 106    |R| ≤ 1/λ_rec² = 1 (in RS-native units). -/
 107theorem curvature_bounded_at_R0 : (1 : ℝ) / ell0 ^ 2 = 1 := by
 108  simp [ell0]