k_rec_com

formal source

 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]
 109
 110/-! ## Certificate -/
 111
 112structure InflationCert where
 113  alpha_derived : alpha_attractor = phi + 1
 114  alpha_positive : 0 < alpha_attractor
 115  spectral_ok : 0.96 < spectral_index 55 ∧ spectral_index 55 < 0.97
 116  modulation_positive : 0 < Omega_0
 117  curvature_bounded : (1 : ℝ) / ell0 ^ 2 = 1
 118
 119theorem inflation_cert : InflationCert where
 120  alpha_derived := alpha_attractor_eq_phi_plus_one
 121  alpha_positive := alpha_attractor_pos
 122  spectral_ok := n_s_at_55
 123  modulation_positive := Omega_0_pos
 124  curvature_bounded := curvature_bounded_at_R0
 125
 126end
 127
 128end RSInflation
 129end Gravity
 130end IndisputableMonolith