phi_inv_lt_one
plain-language theorem explainer
The inequality 1/φ < 1 holds for the golden ratio φ arising as the self-similar fixed point. Researchers citing convergence arguments in φ-emergence or lexicon-ratio calculations would reference it to justify geometric series. The proof is a short term-mode sequence that pulls phi_gt_one and phi_pos, rewrites via div_lt_one, and closes with linarith.
Claim. Let φ > 1 be the golden ratio. Then 1/φ < 1.
background
The Φ-Emergence module derives the golden ratio from J-cost minimization in the Recognition Science setting. It relies on phi_pos (φ > 0) and phi_gt_one (φ > 1) established in Constants and upstream results. The present theorem restates the contraction 1/φ < 1 already shown in LexiconRatio.phi_inv_lt_one, where phi_inv is unfolded as the reciprocal and the same division inequality is applied.
proof idea
The term proof obtains phi_gt_one and phi_pos from the environment, rewrites the goal with div_lt_one applied to the positivity hypothesis, and finishes by linarith.
why it matters
It is used directly by phi_series_sum to confirm that ∑ (1/φ)^{n+1} converges to φ, completing the geometric-series step in the T6 fixed-point emergence. The same fact appears in lexicon_ratio_lt_one and passive_fraction_pos for linguistic applications. Within the T5–T8 chain it supplies the contraction needed for the eight-tick octave and the subsequent emergence of D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.