Gravity Inflation Alpha Attractor Bounds

The alpha attractor bound

The declaration alpha_attractor_bounds in the framework's machine-checked library of formal theorems proves a narrow numerical fact: the alpha-attractor parameter, a positive number that shapes how fast the early universe expanded during inflation, lies strictly between 2.5 and 2.7. The theorem states this as a conjunction of two inequalities, 2.5 < alpha_attractor and alpha_attractor < 2.7, and its proof rests on a prior result about the square of the golden ratio. In plain terms, the framework derives that this parameter is not a free choice but a fixed number in a tight interval.

The alpha-attractor parameter itself is defined as the square of the golden ratio, phi squared, which equals phi plus one, approximately 2.618. The framework reaches this value through a self-similarity condition on its cost functional, the mathematical object that measures the price of recognition events in its ledger model. The parameter's positivity is also proved separately. The bounds theorem thus certifies that the derived value sits in the expected range for a slow-roll inflationary model, consistent with the framework's broader claim that its constants emerge from structure rather than being inserted by hand.

What the declaration does not claim is equally important. It does not assert that the alpha-attractor parameter matches any specific astronomical observation; the theorem is purely a statement about the framework's own derived quantity. It does not claim that the spectral index or tensor-to-scalar ratio, which are defined elsewhere in the same file using this parameter, are measured or confirmed by data. Those are separate predictions, not part of the bounds theorem. The declaration also does not claim that the parameter's value is unique or that no other derivation could produce a different number; it only establishes the interval for the specific definition given.

The practical consequence is that the framework's inflationary model has a concrete, provable anchor for its central parameter. A reader can verify the bounds without trusting any experimental result, because the proof is internal to the formal system. This makes the declaration a building block for further work, such as checking whether the derived tensor-to-scalar ratio falls in a detectable range, instead of being an end in itself.

theorem alpha_attractor_bounds : 2.5 < alpha_attractor ∧ alpha_attractor < 2.7 :=
  phi_squared_bounds

/-- The α-attractor parameter: α = φ².
    In RS, this arises from the self-similarity condition of the
    cost functional: the inflaton potential inherits the quadratic
    character of J(x) near x = 1, with the φ² = φ + 1 identity
    setting the curvature scale. -/
noncomputable def alpha_attractor : ℝ := phi ^ 2

theorem alpha_attractor_eq_phi_plus_one : alpha_attractor = phi + 1 := phi_sq_eq

theorem alpha_attractor_pos : 0 < alpha_attractor := pow_pos phi_pos 2

What this page does not claim

This theorem does not claim any match with astronomical observations. This theorem does not establish the spectral index or tensor-to-scalar ratio as measured facts. This theorem does not prove the uniqueness of the alpha-attractor value.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Inflation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: