phi_pow_ge_one
plain-language theorem explainer
The lemma establishes that the golden ratio raised to any natural power satisfies φ^n ≥ 1. Researchers proving monotonicity of gap costs and J-costs on the phi-ladder cite it when bounding costs from below in the local cache forcing arguments. The proof proceeds by induction on the exponent, multiplying the inductive hypothesis by phi > 1 at each successor step.
Claim. For every natural number $n$, $1 ≤ ϕ^n$, where ϕ is the golden ratio satisfying $1 < ϕ$.
background
The Local Cache Forcing module proves that J-cost minimization on connected graphs forces hierarchical local caching, closing Gap G1 in the brain holography proof. It relies on the fact that phi > 1, stated upstream as 'φ > 1: The golden ratio is strictly greater than 1' in PhiSupport and Constants. The phi-ladder indexes rung costs via successive powers of phi; this lemma supplies the base lower bound used in monotonicity arguments for those powers.
proof idea
Proof by induction on n. The zero case simplifies directly to 1 ≤ 1. In the successor step, rewrite ϕ^(k+1) as ϕ^k * ϕ via pow_succ, then apply mul_le_mul to the inductive hypothesis together with le_of_lt one_lt_phi, using norm_num and positivity for the remaining hypotheses.
why it matters
It is invoked in gapCost_mono ('Gap costs grow monotonically: larger gaps have larger J-cost') and Jcost_phi_pow_strictMono ('J(φ^m) < J(φ^n) FOR m < n') inside PhiLadderStability and the present module. These results support the local_cache_forcing_certificate that establishes forced hierarchical caching. The bound anchors phi-ladder stability required for the self-similar fixed point in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.