phiInv
plain-language theorem explainer
Defines the real number 1/φ as the canonical attractor for negative-rung quantities such as decay rates, dampings, and target ratios. Cross-domain researchers cite it when bounding invariants like senolytic ratios and Gini ceilings inside the unit interval. The definition is a direct noncomputable assignment of the reciprocal of the golden ratio.
Claim. Define $1/φ ∈ ℝ$ by $1/φ := 1/φ$, where $φ$ is the golden ratio satisfying $φ = 1 + 1/φ$.
background
The module CrossDomain.PhiInverseInvariants develops claim C22 on 1/φ invariants. It treats 1/φ ≈ 0.618 as the attractor for negative-rung quantities: decay rates, dampings, target ratios, and optimal share fractions. Listed instances are the senolytic target ratio, Gini coefficient ceiling, amplitude decay per rung in aging, Cabibbo mixing angle ≈ 1/φ³, counter-cyclical policy balance, internet spectral gap decay, and stem-cell reserve decay per rung.
proof idea
The declaration is a one-line definition that directly assigns the reciprocal of phi in the reals.
why it matters
This definition supplies the base value for the PhiRing structure, where PhiInt pairs integer coefficients a + bφ, and for the canonicalPhiRingObj in RecognitionCategory. It supports downstream theorems such as all_phiInv_in_unit_interval that places five quantities in (0,1) and circadianDecay. In the Recognition framework it realizes the C22 claim, connecting to the phi-ladder and the T6 self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.