phiInv_lt_phi
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.