phiInv_lt_one
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 in Recognition Science
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).
scope and limits
- Does not establish positivity of phiInv.
- Does not derive the Fibonacci identity phiInv = phi - 1.
- Does not quantify approximation error to 0.618.
- Does not apply the bound to any concrete physical domain.
Lean usage
theorem unit_interval_example : 0 < phiInv ∧ phiInv < 1 := ⟨phiInv_pos, phiInv_lt_one⟩formal statement (Lean)
37theorem phiInv_lt_one : phiInv < 1 := by
proof body
Term-mode proof.
38 unfold phiInv
39 exact (div_lt_one phi_pos).mpr one_lt_phi
40