phi_pow_neg3760_upper_v2
plain-language theorem explainer
Golden ratio to the power -3.760 is bounded above by 0.16381. Researchers deriving tau lepton mass bounds from the Recognition Science lepton ladder cite this numerical inequality when closing residue estimates. The tactic proof chains a logarithmic lower bound on the golden ratio through exponential monotonicity, reciprocal comparison, and algebraic rewriting of the power.
Claim. $phi^{-3.760} < 0.16381$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
This inequality sits inside the module proving the lepton ladder is forced from the electron structural mass (T9) together with cube geometry and the golden ratio. It supplies a concrete upper bound needed for the tau residue calculation on the phi-ladder. The local setting replaces two earlier axioms with proven inequalities using steps built from passive cube edges, six faces, wallpaper groups, and the eight-tick phase structure.
proof idea
The proof invokes the logarithmic bounds to obtain 1.8093 < 3.760 * log phi via nlinarith. Exponential monotonicity then yields exp(3.760 * log phi) > 6.105. The target power is rewritten as the reciprocal of that exponential using the real rpow definition and negation. Transitivity through the reciprocal inequality and a final numerical comparison closes the bound.
why it matters
It feeds the subsequent upper-bound theorem for the tau residue power, advancing the T10 necessity result that muon and tau masses are forced without extra axioms. In the broader framework the bound reinforces the golden ratio as the self-similar fixed point (T6) that sets the phi-ladder mass formula for leptons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.