phiInv_lt_one
plain-language theorem explainer
phiInv_lt_one establishes that the inverse golden ratio satisfies 1/φ < 1. Workers on cross-domain invariants cite this bound when placing decay rates and target ratios inside the open unit interval. The proof is a direct term-mode reduction that unfolds the definition of phiInv and invokes the division lemma together with the prior result 1 < φ.
Claim. $1/φ < 1$ where $φ$ denotes the golden ratio.
background
The module develops structural invariants for the quantity 1/φ across domains. Module documentation states that 1/φ ≈ 0.618 acts as the canonical attractor for negative-rung quantities such as decay rates, dampings, and target ratios, with listed instances including senolytic target ratio, Gini coefficient ceiling, and stem-cell reserve decay. The definition phiInv := 1/phi supplies the concrete real number, while the upstream lemma one_lt_phi asserts 1 < phi.
proof idea
The proof unfolds phiInv to 1/phi. It then applies the Mathlib lemma div_lt_one (under the hypothesis 0 < phi) in modus-ponens form with the upstream result one_lt_phi : 1 < phi.
why it matters
This theorem supplies one of the two bounds required for unit-interval membership of phiInv. It is invoked directly in all_phiInv_in_unit_interval to establish 0 < phiInv < 1 and appears in the certificate structure PhiInverseInvariantsCert. Within the Recognition framework it closes the universal lemma for 1/φ invariants stated in the module documentation for C22, supporting placement of quantities such as Cabibbo mixing angle inside (0,1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.