phi_12_div_2
plain-language theorem explainer
The golden ratio satisfies |φ¹²/2 − 161| < 1. This pins the Recognition Science prediction m_π/m_e ≈ 273 for the pion-electron ratio. Particle physicists calibrating φ-ladder rungs for light mesons cite the bound. The proof derives the closed recurrence φ¹² = 144φ + 89 from φ² = φ + 1, then applies the supplied interval 1.61 < φ < 1.62 and linear arithmetic to bound the deviation.
Claim. $ |φ^{12}/2 - 161| < 1 $ where φ is the golden ratio satisfying φ² = φ + 1.
background
The PionMasses module derives π⁺, π⁻, π⁰ masses from Recognition Science by placing pions on the φ-ladder. The module states that m_π/m_e ≈ 273 ≈ φ¹²/2 follows from quark binding and the φ-ladder rung assignment. The golden ratio φ is defined by its minimal polynomial, yielding the identity φ² = φ + 1 that generates all higher powers via Fibonacci recurrence.
proof idea
The tactic proof invokes the upstream bounds phi > 1.61 and phi < 1.62 together with phi_sq_eq. It computes successive powers by repeated substitution: φ⁴ = 3φ + 2, φ⁶ = 8φ + 5, then φ¹² = 144φ + 89. Substituting the closed form, dividing by 2, and applying linarith shows the expression lies strictly between 160 and 162; abs_lt and constructor finish the inequality.
why it matters
The theorem supplies the numerical anchor for the pion-electron ratio inside the PionMasses module and its sibling predictions (pionElectronRatioPredicted, pionMassPredicted_eV). It realizes the φ-ladder placement step that follows from T6 (self-similar fixed point) and the eight-tick octave. No downstream declarations yet consume it, leaving open its integration into the full hadron spectrum or the alpha-band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.