zpow_sum3
plain-language theorem explainer
The lemma establishes that for nonzero real x and integers a, b, c the product x^a x^b x^c equals x to the sum of the exponents. It supports exponent simplifications inside the lepton mass formulas of the verification module. The proof is a one-line wrapper applying the two-exponent addition rule twice.
Claim. $x^a x^b x^c = x^{a+b+c}$ for $x$ real and nonzero, with $a,b,c$ integers.
background
The module compares machine-generated lepton masses against PDG 2024 values. The central formula is m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) in MeV, with B_pow = -22 and r0 = 62. This identity is the algebraic tool that collapses products of powers arising when the rung index r is expressed through summed integer offsets.
proof idea
One-line wrapper that applies the two-argument exponent-addition rule for nonzero bases, first to the initial pair and then to the result with the third factor.
why it matters
The lemma supplies the minimal algebraic reduction required to keep the integer-rung predictions inside the lepton sector fully explicit and machine-checkable. It sits inside the verification layer that imports the phi-ladder constants and interval bounds, allowing direct comparison of predicted m_e, m_mu, m_tau with experimental anchors. No downstream theorems are recorded, so its role remains strictly local to the mass-equality auxiliaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.