phi_squared_bounds
plain-language theorem explainer
φ² lies in the open interval (2.5, 2.7). Recognition Science models of orbital gaps, Damköhler numbers, spin-glass freezing, and stellar abundances cite this interval to constrain their ratios. The proof is a term-mode reduction that rewrites via the identity φ² = φ + 1, invokes the companion bounds 1.5 < φ < 1.62, and closes both sides with linear arithmetic.
Claim. $2.5 < φ^2 ∧ φ^2 < 2.7$, where φ denotes the golden ratio obeying the quadratic relation φ² = φ + 1.
background
The Constants module fixes the RS time quantum at one tick. φ is the positive root of x² − x − 1 = 0, the self-similar fixed point forced by the Recognition Composition Law at step T6 of the UnifiedForcingChain.
proof idea
Rewrite the goal with phi_sq_eq to replace φ² by φ + 1. Obtain the two inequalities via phi_gt_onePointFive and phi_lt_onePointSixTwo. Constructor splits the conjunction; linarith discharges both sides by arithmetic on the reals.
why it matters
Fifteen downstream results depend on this interval, including r_orbit_gap_skip_band (gap-skip ratio in planetary formation), criticalDamkohler_in_empirical_band, freezingRatio2D_band, and evenOddAbundanceRatio_in_range. It supplies the numerical content for the T6 self-similar fixed point in the forcing chain T0–T8 and leaves open the required alignment of Recognition Science constants with the observed α⁻¹ band (137.03, 137.04).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.