phi_sq_gt_2_5
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.