pith. machine review for the scientific record. sign in
theorem proved term proof high

phi_squared_bounds

show as:
view Lean formalization →

The theorem establishes that the square of the golden ratio satisfies 2.59 < φ² < 2.62. Researchers deriving scaling relations for orbital gaps, Damköhler numbers, and spin-glass ratios cite the result to anchor numerical bands. The proof substitutes the algebraic identity φ² = φ + 1, imports the tightened interval 1.61 < φ < 1.62, and discharges both conjuncts by nonlinear arithmetic.

claim$2.59 < φ^2 ∧ φ^2 < 2.62$

background

Recognition Science obtains φ as the unique positive fixed point of the self-similar map J(x) = (x + x^{-1})/2 - 1. The identity φ² = φ + 1 follows at once from the quadratic x² - x - 1 = 0. The module assembles calculated proofs for cosmological registry items (primordial spectrum, dark-energy density, Hubble parameter) that all rest on explicit numerical intervals for powers of φ.

proof idea

The argument invokes the identity lemma phi_sq_eq to replace φ² by φ + 1. It then obtains the bounding lemmas 1.61 < φ < 1.62 and splits the target conjunction. Each conjunct is settled by a single nlinarith tactic.

why it matters in Recognition Science

Fifteen downstream declarations invoke the bound, including the gap-skip ratio in planetary formation and the critical Damköhler interval in combustion stabilization. The result supplies the concrete window required to place scaling factors inside the empirical bands demanded by the Recognition Composition Law and the eight-tick octave. It thereby completes one of the calculated items listed for the cosmological predictions registry.

scope and limits

formal statement (Lean)

  91theorem phi_squared_bounds : (2.59 : ℝ) < phi^2 ∧ phi^2 < (2.62 : ℝ) := by

proof body

Term-mode proof.

  92  have h1 : phi ^ 2 = phi + 1 := phi_sq_eq
  93  rw [h1]
  94  have h2 : phi > (1.61 : ℝ) := phi_gt_onePointSixOne
  95  have h3 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
  96  constructor
  97  · nlinarith
  98  · nlinarith
  99
 100/-- **CALCULATED**: φ⁴ = (φ²)² bounds.
 101    
 102    With 2.59 < φ² < 2.62: 6.7 < φ⁴ < 6.9 -/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.