phi_ge_one
The lemma establishes that the golden ratio satisfies 1 ≤ phi. Researchers bounding the phi-ladder for mass formulas or proving monotonicity of impulses and bonuses cite it. The proof is a one-line wrapper that converts the strict inequality from one_lt_phi via le_of_lt.
claim$1 ≤ ϕ$, where ϕ denotes the golden ratio fixed point of the Recognition Composition Law.
background
The Constants module defines phi as the positive self-similar fixed point satisfying ϕ = 1 + 1/ϕ. Upstream one_lt_phi proves the strict inequality 1 < phi by showing sqrt(1) < sqrt(5) and hence 2 < 1 + sqrt(5). The module doc identifies τ₀ = 1 tick as the RS-native time quantum, placing these inequalities at the base of the forcing chain.
proof idea
This is a one-line wrapper that applies le_of_lt to the lemma one_lt_phi.
why it matters in Recognition Science
It supplies the base inequality required by ladder_agrees_at_half_rung in PlanetaryFormationFromJCost and by impulse_after_octaves_mono_decay in VolcanicForcingAsJCostImpulse. The result anchors the phi-ladder at rung 8, consistent with T6 where phi is forced as the self-similar fixed point and with the eight-tick octave structure.
scope and limits
- Does not compute a numerical approximation of phi.
- Does not prove irrationality of phi.
- Does not apply to the negative root of the quadratic.
Lean usage
have h1 : (1 : ℝ) ≤ phi := phi_ge_oneformal statement (Lean)
39lemma phi_ge_one : 1 ≤ phi := le_of_lt one_lt_phi