phi_gt_one
plain-language theorem explainer
The theorem establishes that the golden ratio φ exceeds 1 in Recognition Science. Researchers bounding φ-ladder costs or irrational-precision requirements in computation limits would cite it as a basic inequality. The proof is a direct one-line application of the upstream lemma one_lt_phi.
Claim. The golden ratio φ, the self-similar fixed point of the Recognition Science J-cost, satisfies $φ > 1$.
background
Module IC-002 derives fundamental computation limits from RS temporal discreteness (tick τ₀ as minimum time quantum), irrational constants such as φ, and Landauer erasure costs. The golden ratio φ appears as the fixed point forced by the J-uniqueness relation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and the phi-ladder for mass rungs. Upstream lemma one_lt_phi proves the inequality by comparing √5 to 2 via the real square-root function and norm_num tactics.
proof idea
The proof is a one-line wrapper that applies the upstream lemma one_lt_phi from Constants, which itself reduces the claim to the ordering 1 < √5 and algebraic rearrangement.
why it matters
This result anchors the irrational-constants source of computation limits in the module (IC-002), ensuring φ-based states require transcendental precision and that costs grow without bound at high rungs. It supports sibling results on phi_not_rational and no_exact_phi_computation. The inequality is a prerequisite for the eight-tick octave and D=3 spatial structure in the broader T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.