phi_hierarchy_exponential
plain-language theorem explainer
The declaration asserts that the golden ratio exceeds unity, which forces Recognition Science complexity hierarchies to expand exponentially with rung index. Complexity theorists classifying RS-derived physics computations would cite it to place high-tier mass spectra in EXPTIME. The proof is a direct one-line wrapper referencing the upstream inequality one_lt_phi.
Claim. The golden ratio fixed point satisfies $1 < phi$, implying that RS complexity hierarchies grow exponentially with rung number.
background
The module IC-005 examines where physics sits in the complexity zoo under Recognition Science. J-cost is the convex function J(x) = (x + 1/x)/2 - 1 whose unique minimum lies at x = 1; local 8-tick dynamics remain O(1) per step while ground-state verification is linear. The phi-hierarchy encodes discrete mass rungs that scale as phi to the rung power, so high-rung states require exponentially many operations. This theorem rests on the upstream lemma one_lt_phi, which proves 1 < phi by comparing square roots of 1 and 5.
proof idea
The proof is a one-line wrapper that directly applies the lemma one_lt_phi from the Constants module.
why it matters
The result supplies the exponential-growth premise for the module's claim that phi-rung computation lies in EXPTIME. It aligns with framework landmark T6, where phi is forced as the self-similar fixed point, and supports the mass formula yardstick * phi^(rung - 8 + gap(Z)). No downstream theorems are recorded, so the declaration closes a foundational step rather than feeding a larger parent result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.