all_phiInv_in_unit_interval
The declaration proves that the senolytic target ratio, identified with the reciprocal of the golden ratio, lies strictly between zero and one. Cross-domain modelers in Recognition Science cite this when confirming bounds on decay rates and target fractions in biological and policy models. The proof is a one-line term that pairs the positivity and upper-bound lemmas for the reciprocal.
claim$0 < 1/φ < 1$, where φ denotes the golden ratio and the senolytic target ratio is defined as this reciprocal.
background
The module treats 1/φ as the canonical attractor for negative-rung quantities including decay rates, dampings, and target ratios. phiInv is defined as 1/φ and senolyticTargetRatio is defined identically as phiInv. Upstream lemmas establish positivity of phiInv via division of positives and the strict upper bound via the fact that φ exceeds one.
proof idea
The proof is a term-mode construction that directly pairs the two upstream lemmas phiInv_pos and phiInv_lt_one. It is a one-line wrapper that applies these results to the definition of senolyticTargetRatio.
why it matters in Recognition Science
This result packages the universal bounds for 1/φ invariants, supporting the module claim that 1/φ attracts negative-rung quantities across domains. It aligns with the Recognition Science framework where φ is the self-similar fixed point and enters mass formulas and decay thresholds. No downstream uses are recorded yet.
scope and limits
- Does not establish the bound for quantities outside the listed instances.
- Does not derive the ratio from empirical data in specific domains.
- Does not address stability under perturbations or model variations.
- Does not connect to the forcing chain steps T0-T8 or spatial dimension D=3.
formal statement (Lean)
105theorem all_phiInv_in_unit_interval :
106 0 < senolyticTargetRatio ∧ senolyticTargetRatio < 1 := ⟨phiInv_pos, phiInv_lt_one⟩
proof body
Term-mode proof.
107
108/-- Cabibbo factor is in (0, 1) (smaller than phiInv). -/