`alpha_attractor_eq_phi_plus_one`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.Inflation
domain: Gravity
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.Inflation on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  34    setting the curvature scale. -/
  35noncomputable def alpha_attractor : ℝ := phi ^ 2
  36
  37theorem alpha_attractor_eq_phi_plus_one : alpha_attractor = phi + 1 := phi_sq_eq
  38
  39theorem alpha_attractor_pos : 0 < alpha_attractor := pow_pos phi_pos 2
  40
  41theorem alpha_attractor_bounds : 2.5 < alpha_attractor ∧ alpha_attractor < 2.7 :=
  42  phi_squared_bounds
  43
  44/-! ## Spectral Predictions -/
  45
  46/-- Spectral index: n_s ≈ 1 - 2/N (standard slow-roll result). -/
  47noncomputable def spectral_index (N : ℝ) : ℝ := 1 - 2 / N
  48
  49/-- Tensor-to-scalar ratio: r ≈ 12α/N² = 12φ²/N².
  50    This is the RS-SPECIFIC prediction: the standard α-attractor formula
  51    with α = φ² (not a free parameter). -/
  52noncomputable def tensor_to_scalar (N : ℝ) : ℝ := 12 * alpha_attractor / N ^ 2
  53
  54/-- For N = 55 e-foldings: r ≈ 12 * 2.618 / 3025 ≈ 0.0104. -/
  55theorem r_at_55_bounds : tensor_to_scalar 55 > 0 := by
  56  unfold tensor_to_scalar
  57  apply div_pos
  58  · exact mul_pos (by norm_num) alpha_attractor_pos
  59  · positivity
  60
  61/-- For N = 55: n_s ≈ 0.964. -/
  62theorem n_s_at_55 : 0.96 < spectral_index 55 ∧ spectral_index 55 < 0.97 := by
  63  unfold spectral_index; constructor <;> norm_num
  64
  65/-- The tensor ratio r is in the range detectable by LiteBIRD/CMB-S4.
  66    For α = φ² and N ∈ [50, 60]: r ∈ (0.005, 0.02). -/
  67theorem r_in_detectable_range :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.