PhiInverseInvariantsCert
plain-language theorem explainer
The structure bundles positivity, ordering, and algebraic identities for the inverse golden ratio together with cross-domain equality assertions. It certifies that the senolytic target ratio, Gini ceiling, policy balance, stem-cell decay, and circadian decay are identical, and that the Cabibbo factor is positive but smaller than the inverse golden ratio. Modelers applying Recognition Science predictions across domains would cite the certificate to invoke these invariants at once. The declaration is a structure definition that aggregates prior S
Claim. Let $phi^{-1}$ denote the inverse golden ratio. The certificate asserts $0 < phi^{-1}$, $phi^{-1} < 1$, $phi^{-1} < phi$, the identity $phi^{-1} = phi - 1$, the relations $phi^{-2} = 2 - phi$ and $phi^{-3} = 2 phi - 3$, equality among the senolytic target ratio, Gini ceiling, policy balance, stem-cell decay, and circadian decay, and the bound $0 < $ Cabibbo factor $< phi^{-1}$.
background
In the CrossDomain.PhiInverseInvariants module the inverse golden ratio is defined as $1/phi$, where $phi$ is the self-similar fixed point. The module sets senolyticTargetRatio, giniCeiling, policyBalance, stemCellDecay, and circadianDecay each equal to this value, while cabibboFactor is set to $1/phi^3$. Module documentation states that $1/phi approx 0.618$ is the canonical attractor for negative-rung quantities such as decay rates and target ratios, with the universal lemma that $1/phi < 1$ and $1/phi > 0$ plus the identity $1/phi = phi - 1$. Upstream theorems establish $phi^{-1} > 0$, $phi^{-1} < 1$, and $phi^{-1} < phi$ directly from the definition and the fact that $phi > 1$.
proof idea
The declaration is a structure definition whose fields reference upstream theorems for positivity and ordering together with sibling lemmas supplying the Fibonacci and reciprocal-power identities. The five-instances equality follows at once from the common definition of each quantity as $phi^{-1}$. The Cabibbo bound follows from the definition of cabibboFactor as $1/phi^3$ combined with the ordering $phi^{-1} < 1$. No tactics or reductions are performed; the structure simply collects the properties.
why it matters
This certificate consolidates the cross-domain $1/phi$ invariants described in the module documentation for C22, enabling uniform application across the listed domains. It is instantiated by the downstream definition that constructs an explicit instance of the certificate. Within the Recognition Science framework it supports the self-similar fixed point $phi$ by exhibiting its inverse in multiple settings, consistent with the forcing chain that fixes $phi$ and the spatial dimension $D=3$. It touches no open questions but completes the invariant collection for this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.