phi_pow_neg377_lower_proved
plain-language theorem explainer
Establishes 0.1629 < φ^{-3.77} for the golden ratio φ. Lepton generation necessity proofs cite this bound to anchor the lower estimate on the tau residue. The tactic proof obtains tight log φ bounds, applies nlinarith and exp monotonicity to control the exponent, rewrites the power via rpow_def_of_pos, and closes by numeric comparison.
Claim. The inequality $0.1629 < φ^{-3.77}$ holds, where $φ$ denotes the golden ratio.
background
Module T10 proves the lepton ladder forced from the electron structural mass (T9) and geometric constants derived from cube faces, passive edges, and wallpaper groups. The declaration discharges the hypothesis that φ^{-3.77} exceeds 0.1629, with φ the self-similar fixed point from T6. Upstream log_phi_bounds supplies the interval (0.481211, 0.481212) for log φ; exp_181416924_upper supplies the companion exponential bound.
proof idea
Unfolds the hypothesis. Simpa pulls log φ bounds from ElectronMass.Necessity.log_phi_bounds. Nlinarith yields 3.77 log φ < 1.81416924. Real.exp_lt_exp and lt_trans with exp_181416924_upper bound the exponential below 6.1385. One_div_lt_one_div_of_lt produces the reciprocal inequality. A calc block rewrites φ^{-3.77} via Real.rpow_def_of_pos, ring, and Real.exp_neg. Norm_num and lt_trans finish the comparison.
why it matters
Discharges the numeric hypothesis that feeds phi_pow_residue_tau_lower, which bounds the predicted tau residue from below. This advances the T10 goal of replacing axioms with proven inequalities for muon and tau masses. The bound closes a gap in the phi-ladder mass formula while preserving the eight-tick octave and Recognition Composition Law structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.