phiInv_lt_phi
The inequality 1/φ < φ holds for the golden ratio φ > 1. Cross-domain modelers assembling invariants for decay rates and mixing angles cite this to confirm that the canonical negative-rung attractor stays below φ itself. The proof is a two-step calculation chain that first places 1/φ below 1 and then chains to φ using the definition of phi inverse together with the lemma one_lt_phi.
claim$1/φ < φ$, where φ is the golden ratio satisfying φ > 1.
background
The module C22 treats 1/φ ≈ 0.618 as the canonical attractor for negative-rung quantities including decay rates, dampings, target ratios, and optimal share fractions. The definition phiInv sets this value explicitly to 1/φ. Upstream, the lemma one_lt_phi proves 1 < φ via square-root comparisons in Constants, while phi_pos supplies the positivity needed for division inequalities. The local setting quotes the universal lemma that 1/φ < 1 (since φ > 1) and 1/φ > 0 (since φ > 0).
proof idea
The term proof unfolds phiInv to 1/φ, then applies a calc block. It first invokes (div_lt_one h).mpr with h from phi_pos and hone from one_lt_phi to obtain 1/φ < 1, then chains the second step 1 < φ directly from hone. No additional tactics or lemmas beyond these two upstream facts are required.
why it matters in Recognition Science
The result is collected inside the PhiInverseInvariantsCert structure that bundles all 1/φ inequalities and identities for cross-domain use. It supports the module claim that 1/φ is the attractor for senolytic ratios, Gini ceilings, and stem-cell decay. Within the Recognition framework it aligns with the forcing chain step T6 where φ is forced as the self-similar fixed point, and it closes one of the universal lemmas listed in the module documentation.
scope and limits
- Does not prove the Fibonacci identity 1/φ = φ - 1.
- Does not quantify the numerical gap φ - 1/φ.
- Does not extend the inequality to other algebraic numbers or fields.
- Does not address dynamical convergence rates involving 1/φ.
formal statement (Lean)
41theorem phiInv_lt_phi : phiInv < phi := by
proof body
Term-mode proof.
42 have h := phi_pos
43 have hone := one_lt_phi
44 unfold phiInv
45 calc 1 / phi < 1 := (div_lt_one h).mpr hone
46 _ < phi := hone
47
48/-- 1/φ = φ - 1 (Fibonacci-phi identity).
49 Proof: φ·(φ-1) = φ² - φ = (φ+1) - φ = 1, so φ-1 = 1/φ. -/