phi_pow_neg45_lower
plain-language theorem explainer
The numerical inequality asserts that phi raised to -4.5 exceeds 0.1147. Charm quark mass bounds under the quarter-ladder hypothesis cite this lower bound to pin the predicted interval. The tactic proof compares the target against 0.11472 via norm_num and closes the gap with linarith.
Claim. $0.1147 < phi^{-4.5}$
background
Module T12 formalizes quark masses via the Quarter-Ladder Hypothesis: quarks occupy the same structural base as leptons but sit at quarter-integer rungs on the phi-ladder. Charm is placed at rung -4.50 = -18/4. The phi-ladder supplies the mass formula yardstick * phi^(rung - 8 + gap(Z)) in RS-native units where phi is the golden-ratio fixed point from the forcing chain.
proof idea
One-line wrapper that applies norm_num to obtain 0.1147 < 0.11472 and then linarith, using the external numeric fact that phi^(-4.5) ≈ 0.11471.
why it matters
The bound is invoked inside charm_mass_pred_bounds to close the interval (1245, 1247) for the predicted charm mass. It supplies the lower edge required by the T12 quarter-ladder derivation, consistent with the Recognition Science mass ladder and the phi-power spacing between generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.