phi_pow_neg375_upper_proved
plain-language theorem explainer
The inequality φ^{-3.75} < 0.165 holds for the golden ratio φ. Lepton mass calculations in the Recognition Science framework cite this bound to control the tau residue. The proof chains interval bounds on log φ through exponential inequalities and the definition of real exponentiation.
Claim. $φ^{-3.75} < 0.165$, where $φ = (1 + √5)/2$ is the golden ratio.
background
In the lepton generations necessity module the lepton ladder is forced from the electron mass (T9) together with geometric constants from cube structure and the golden ratio φ from T4. The definition phi_pow_neg375_upper_hypothesis encodes the numeric claim that the golden ratio raised to -3.75 lies below 0.165. This bound is required to close the upper estimate on the predicted tau residue. Upstream results supply the interval (0.481211, 0.481212) for log φ together with the inequality exp(1.80454125) > 6.07.
proof idea
The proof unfolds the hypothesis definition and obtains the log φ bounds via simpa from ElectronMass.Necessity.log_phi_bounds. It then uses nlinarith to establish 1.80454125 < 3.75 * log φ, applies Real.exp_lt_exp to obtain the corresponding exponential inequality, and chains with the pre-proved exp_180454125_lower via lt_trans. The power is rewritten using the exponential definition of real exponentiation, after which the reciprocal inequality is combined with a numeric comparison 1/6.07 < 0.165.
why it matters
This result discharges the numeric hypothesis needed for the tau upper bound theorem phi_pow_residue_tau_upper, which in turn supports the overall proof that the lepton masses are forced (T10). It sits inside the chain that replaces the original axioms in LeptonGenerations.lean with derived inequalities, using the eight-tick octave and φ-ladder structure from the Recognition Science foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.