phiInv_pos
plain-language theorem explainer
The theorem asserts that the inverse golden ratio is strictly positive. Cross-domain modelers in Recognition Science cite it to bound decay rates and target ratios below unity. The proof is a one-line term-mode reduction that unfolds the definition of phiInv and invokes the standard positivity of division in the reals.
Claim. $0 < 1/phi$ where $phi$ is the golden ratio.
background
The module CrossDomain.PhiInverseInvariants collects structural invariants showing that $1/phi approx 0.618$ acts as the canonical attractor for negative-rung quantities such as decay rates, dampings, and optimal share fractions. The upstream definition states that phiInv is the noncomputable real given by $1/phi$. The local setting is the universal lemma that $1/phi > 0$ (since $phi > 0$) together with the companion bound $1/phi < 1$.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of phiInv to expose the quotient $1/phi$, then applies the lemma div_pos to the positivity of one and the positivity of phi.
why it matters
This result supplies the positivity half of the unit-interval bounds used by all_phiInv_in_unit_interval and by the certificate structure PhiInverseInvariantsCert. It directly supports the module's claim that $1/phi$ is the attractor for decay processes across domains, consistent with the phi-ladder and the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.