all_phiInv_in_unit_interval
plain-language theorem explainer
Recognition Science cross-domain analysis establishes that the senolytic target ratio lies strictly between zero and one. Modelers of decay processes and target fractions cite this bound when confirming unit-interval membership for 1/φ attractors. The proof is a direct term pairing of the positivity and upper-bound results for the reciprocal of phi.
Claim. Let $r$ denote the senolytic target ratio, identified with $1/φ$ where $φ$ is the golden ratio. Then $0 < r ∧ r < 1$.
background
The module treats $1/φ$ as the canonical attractor for negative-rung quantities such as decay rates, dampings, target ratios, and optimal share fractions. The senolytic target ratio is defined exactly as phiInv, which equals $1/φ$. Upstream results supply the definition phiInv := $1/φ$ together with the separate theorems that $0 < phiInv$ and $phiInv < 1$, each proved from the positivity and ordering properties of $φ$.
proof idea
The proof is a term-mode construction that directly supplies the conjunction from the two upstream theorems phiInv_pos and phiInv_lt_one, using the definitional equality between senolyticTargetRatio and phiInv.
why it matters
This result instantiates the module claim that all five listed invariants remain bounded in (0,1). It supports the structural assertion that $1/φ$ attracts senolytic targets, Gini ceilings, amplitude decays, and related quantities. The bound is consistent with the self-similar fixed point $φ$ arising in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.