one_plus_1332_div_phi_upper
plain-language theorem explainer
The inequality 1 plus 1332 divided by the golden ratio is strictly less than 824.2218 holds over the reals. Researchers deriving forced electron mass values under T9 Necessity cite this bound to control logarithmic upper limits on mass ratios. The proof is a short tactic sequence that asserts positivity, rearranges the target via multiplication, applies the division inequality rule, and closes with linear arithmetic.
Claim. $1 + 1332 / 1.618033 < 824.2218$, where $1.618033$ approximates the golden ratio forced as the self-similar fixed point.
background
The module addresses T9 Necessity, proving the electron mass formula is forced from T8 ledger quantization and geometric constants derived earlier. The golden ratio enters via the phi-ladder mass formula (yardstick times phi to the power of rung minus 8 plus gap of Z) and the eight-tick octave at T7. This numerical bound supplies an anchor for expressions involving 1332 and 824.2218 that appear in the electron mass topology.
proof idea
The tactic proof first asserts positivity of 1.618033 with norm_num. It then invokes nlinarith to obtain the rearranged form 1332 less than 823.2218 times 1.618033. The div_lt_iff0 rule rewrites the division inequality, after which linarith completes the proof.
why it matters
This result feeds directly into log_824_upper, which applies the logarithm inequality to bound Real.log of the expression below 6.7145. It supports the T9 claim that the electron mass is forced, connecting to the phi-ladder and the alpha inverse band inside (137.030, 137.039). The proof is complete with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.