phi_sq_gt_2_5
The golden ratio squared exceeds 2.5. Analysts of Recognition Science constant predictions cite this result when bundling lower bounds on derived quantities from the phi ladder. The proof substitutes the identity φ² = φ + 1, invokes the lower bound φ > 1.5, and closes the inequality with nlinarith.
claim$φ^2 > 2.5$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies calculated proofs for bounds on constants predicted by the Recognition Science framework, including the fine-structure constant, the speed of light in native units, and the Boltzmann analog. This declaration adds a lower bound on the square of the golden ratio to that collection. Upstream, the lemma phi_gt_onePointFive states a tighter lower bound: φ > 1.5 (since √5 > 2, so (1 + √5)/2 > 1.5). The identity phi_sq_eq asserts that the square of the golden ratio equals the golden ratio plus one, from the defining equation x² - x - 1 = 0.
proof idea
The proof first obtains φ² = φ + 1 from phi_sq_eq. It then applies the bound φ > 1.5 from phi_gt_onePointFive. The tactic nlinarith combines the rewritten expression with the strict inequality to conclude the result.
why it matters in Recognition Science
This bound is assembled into the certificate constants_predictions_cert_exists that collects proved predictions for α, c, and the Boltzmann analog. It supports the calculated status for registry items listed in the module. Within the Recognition Science framework the golden ratio appears as the self-similar fixed point forced by the J-uniqueness step in the forcing chain.
scope and limits
- Does not establish an upper bound on φ².
- Does not derive φ from the functional equation of Recognition Science.
- Does not connect the inequality to specific physical constants beyond the phi ladder.
formal statement (Lean)
192theorem phi_sq_gt_2_5 : phi^2 > (2.5 : ℝ) := by
proof body
Term-mode proof.
193 have h1 : phi^2 = phi + 1 := phi_sq_eq
194 rw [h1]
195 have h2 : phi > 1.5 := phi_gt_onePointFive
196 nlinarith
197
198/-- **CALCULATED**: φ² < 2.7. -/