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