one_plus_1332_div_phi_lower
plain-language theorem explainer
The theorem asserts the numerical inequality 824.2 < 1 + 1332 / 1.618034. Researchers deriving forced values for the electron mass in Recognition Science cite it as an anchor for logarithmic bounds. The proof is a short tactic sequence that establishes positivity, rearranges via multiplication, rewrites the division, and closes with linear arithmetic.
Claim. $824.2 < 1 + 1332 / 1.618034$
background
The module shows that the electron mass formula is forced from T8 ledger quantization and the geometric constants obtained earlier. The decimal 1.618034 approximates the golden ratio phi, the self-similar fixed point forced at T6 in the chain. This inequality supplies a concrete numerical step that later results use to bound logarithms appearing in the mass topology.
proof idea
Norm_num establishes positivity of the denominator. Nlinarith produces the rearranged multiplication inequality 1.618034 * 823.2 < 1332. The division form is recovered by rewriting with the positivity fact, after which linarith finishes the argument.
why it matters
The result is invoked inside the proof of log_824_lower to chain an exponential upper bound through to a logarithmic lower bound. This supports the T9 claim that the electron mass is forced by the Recognition Science constants, including the phi-ladder mass formula and the alpha band. It closes a numerical gap without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.