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

phi_gt_onePointSixOne

show as:
view Lean formalization →

The golden ratio satisfies 1.61 < phi. Recognition Science applications that need a concrete numerical floor on phi, such as frequency bands on the phi-ladder or J-cost intervals, cite this bound. The proof is a short tactic sequence that unfolds the definition of phi, proves a square-root comparison by squaring, and closes with linarith.

claim$1.61 < phi$

background

In the Recognition framework phi is the self-similar fixed point forced at step T6 of the unified forcing chain, satisfying phi = 1 + 1/phi and appearing in the eight-tick octave and the phi-ladder mass formula. The Constants module supplies elementary real-arithmetic bounds on this number once its definition is fixed. Upstream results such as OptionAEmpiricalProgram.is and SimplicialLedger.EdgeLengthFromPsi.is supply the surrounding empirical and geometric setting in which the bound is later applied, though the present lemma itself uses only the definition of phi together with real-number comparison tactics.

proof idea

The proof unfolds the definition of phi via simp, then proves 2.22 < sqrt(5) by showing 2.22 squared is less than 5 with norm_num, rewriting the square-root inequality, and finishing with linarith.

why it matters in Recognition Science

This lemma supplies the lower half of the tight numerical interval (1.61, 1.62) used by forty downstream declarations, including optimalT60_band (which places reverberation time inside the Beranek band), Jphi_numerical_band (which locates J(phi) inside (0.11, 0.12)), phi_eighth_in_gamma_band (which places phi^8 inside the gamma EEG range), and E_PBM_bounds. It therefore supports the concrete numerical predictions that follow from the eight-tick octave and the phi-ladder once phi is fixed as the T6 fixed point. No open scaffolding questions are discharged here.

scope and limits

Lean usage

have h1 : (1.61 : ℝ) < phi := phi_gt_onePointSixOne

formal statement (Lean)

  97lemma phi_gt_onePointSixOne : (1.61 : ℝ) < phi := by

proof body

Tactic-mode proof.

  98  simp only [phi]
  99  have h5 : (2.22 : ℝ) < Real.sqrt 5 := by
 100    have h : (2.22 : ℝ)^2 < 5 := by norm_num
 101    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.22)]
 102    exact Real.sqrt_lt_sqrt (by norm_num) h
 103  linarith
 104
 105/-- φ² is between 2.5 and 2.7.
 106    φ² = φ + 1 ≈ 2.618 (exact: (3 + √5)/2). -/

used by (40)

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

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.