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

phi_squared_bounds

show as:
view Lean formalization →

The golden ratio squared satisfies 2.5 < phi^2 < 2.7. Researchers modeling J-cost bands, orbital gap ratios, spin-glass freezing, and stellar abundances cite this interval to obtain concrete numerical constraints. The proof reduces the claim via the quadratic identity for phi and closes both sides of the conjunction by linear arithmetic on the tighter bounds 1.5 < phi < 1.62.

claim$2.5 < phi^2 < 2.7$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.

background

The Constants module supplies numerical bounds on phi, the positive root of x^2 - x - 1 = 0 that appears as the self-similar fixed point in the Recognition Science forcing chain. Upstream lemma phi_sq_eq records the identity phi^2 = phi + 1. The supporting bounds are given by phi_gt_onePointFive (phi > 1.5, since sqrt(5) > 2) and phi_lt_onePointSixTwo (phi < 1.62, since sqrt(5) < 2.24). These facts sit inside the module that also defines the fundamental RS time quantum tau_0 = 1 tick.

proof idea

The term proof rewrites the goal with phi_sq_eq, obtaining the equivalent statement 2.5 < phi + 1 < 2.7. It then pulls in the two phi bounds via have statements. The constructor splits the conjunction and linarith discharges both inequalities by arithmetic.

why it matters in Recognition Science

This lemma supplies the numerical band (2.5, 2.7) invoked by r_orbit_gap_skip_band for planetary gap-skip ratios, by freezingRatio2D_band for 2D Ising freezing ratios, by criticalDamkohler_in_empirical_band for combustion timescales, and by evenOddAbundanceRatio_in_range for stellar abundances. It concretizes the phi fixed point forced at T6 of the UnifiedForcingChain and feeds the phi-ladder mass formula used across the framework.

scope and limits

Lean usage

have h : phi ^ 2 < 2.7 := phi_squared_bounds.2

formal statement (Lean)

 107lemma phi_squared_bounds : (2.5 : ℝ) < phi^2 ∧ phi^2 < 2.7 := by

proof body

Term-mode proof.

 108  rw [phi_sq_eq]
 109  have h1 := phi_gt_onePointFive
 110  have h2 := phi_lt_onePointSixTwo
 111  constructor <;> linarith
 112
 113/-! ### Fibonacci power identities for φ -/
 114
 115/-- Key identity: φ³ = 2φ + 1 (Fibonacci recurrence).
 116    φ³ = φ × φ² = φ(φ + 1) = φ² + φ = (φ + 1) + φ = 2φ + 1. -/

used by (15)

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

depends on (9)

Lean names referenced from this declaration's body.