phi_pow_neg3762_lower_v2
plain-language theorem explainer
The result establishes the strict lower bound 0.1635 on the golden ratio raised to the power negative 3.762. Researchers assembling forced tau lepton residue estimates in the lepton generations necessity module cite this bound to close the numerical chain. The argument multiplies the logarithm bound on phi by 3.762, invokes the exponential upper bound lemma, rewrites the power via the real exponentiation definition, and applies transitivity.
Claim. $0.1635 < phi^{-3.762}$ where $phi$ is the golden ratio.
background
The module proves that the lepton ladder is forced from the electron mass and geometric constants derived from cube geometry together with the eight-tick structure. The golden ratio enters as the self-similar fixed point fixed by the forcing chain. This bound on the negative power supports residue calculations for the tau lepton by supplying a concrete numerical inequality.
proof idea
The proof first calls the logarithm bounds lemma on phi to obtain 3.762 times log phi less than 1.8104 via nlinarith. It applies the exponential upper bound lemma to reach exp of the product less than 6.114. The reciprocal inequality is formed, the power is rewritten as the reciprocal of the exponential using the rpow definition, ring, and exp_neg, and transitivity with the numerical comparison 0.1635 less than 1 over 6.114 closes the result.
why it matters
This bound is invoked directly by the lower bound theorem for the tau residue phi to the predicted power. It advances the T10 necessity claim that muon and tau masses are determined by the electron mass, cube-derived steps including E_passive equals 11, faces equals 6, W equals 17, alpha, and pi. The step sits inside the phi-ladder mass formula and the recognition composition law that fixes the underlying constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.