phi_lower
plain-language theorem explainer
The forced golden ratio φ satisfies 1.618033 < φ, certified as the rational lower bracket 1618033/1000000 < φ inside ℤ[φ]. Anyone assembling the sigma0 ladder-ratio bundle or its real-side display cites this. The proof is a one-line kernel decide on the decidable positivity witness for that comparison.
Claim. Let $\varphi$ be the golden ratio realized in $\mathbb{Z}[\varphi]$. Then $\frac{1618033}{1000000} < \varphi$ (equivalently $1.618033 < \varphi$), where the comparison is the decidable integer predicate that $q\cdot x - p$ is positive for $p=1618033$, $q=1000000$, $x=\varphi$.
background
Recognition Science forces a single dimensionless ratio φ (T6: the self-similar fixed point). The mass law places spectrum rungs on the φ-ladder, so integer rung gaps become exact powers φ^k. This module certifies those ratios without the continuum: elements of ℤ[φ] (GoldenInt) carry the arithmetic, and concrete inequalities close by integer sign tests.
RatLt p q x asserts that the rational p/q lies strictly below x. It is defined as positivity of the witness q·x − p under the sigma0 predicate IsPos. Because √5-irrationality makes ties impossible, IsPos is decidable by comparing integer squares, with no Real.sqrt, Float, or native_decide.
The local setting is sigma0 DELTA_FORCED: every bracket here must close inside {propext, Quot.sound}. The companion upper bracket is φ < 1618034/1000000; together they pin φ to six decimal places by pure integer arithmetic.
proof idea
One-line tactic proof: by decide. Unfolding RatLt reduces the goal to IsPos on the GoldenInt witness 1000000·φ − 1618033. That positivity predicate is decidable via the √5-irrationality machinery already proved for ℤ[φ] (compare s² against 5t² on the cleared witness). The kernel therefore closes the comparison by computation alone; no classical choice and no real analysis enter.
why it matters
This is the lower half of the primitive forced-ratio bracket in the Delta Forcing Spectrum program. It is packaged with the matching upper bound and the φ⁵, φ⁸ rung brackets into ladder_ratio_brackets, the sigma0 bundle that pins φ and the representative ladder powers by choice-free integer arithmetic.
Downstream, ladder_ratio_real_brackets (GoldenIntReal) reads the same inequalities under evaluation into ℝ, so the classical golden ratio inherits 1618033/1000000 < φ < 1618034/1000000. That bridge is the only sigma1 step; the arithmetic decision itself stays at sigma0.
Framework landmark: T6 forces φ as the unique self-similar fixed point. Certified rational brackets make that forced ratio auditable by both decide and #eval, which is the module's verdict target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.