c1_half
plain-language theorem explainer
The declaration verifies that the leading coefficient in the known expansion of the electron anomalous magnetic moment equals one half. Researchers matching QED perturbative results to the Recognition Science phi-ladder cite this as the base case. The proof is a direct unfolding of the coefficient definition followed by numerical normalization.
Claim. The first coefficient in the known QED expansion of the anomalous magnetic moment satisfies $a_1 = 1/2$.
background
The module develops the electron anomalous magnetic moment from the RS phi-ladder, following the paper RS_Electron_g_minus_2.tex. The function known_ae_coeffs maps each order n to the corresponding standard QED coefficient, with the explicit cases 0.5 for n=1, -0.32848 for n=2, 1.18124 for n=3, and zero otherwise. This supplies the perturbative benchmarks against which RS-derived terms are compared.
proof idea
The proof is a one-line wrapper that unfolds the definition of known_ae_coeffs and applies norm_num to confirm the equality at input 1.
why it matters
This base case anchors the g-2 series in the RS framework and supplies the starting point for sibling results such as schwinger_term and schwinger_is_alpha_over_2pi. It aligns with the Recognition Science constants (alpha inverse in the 137.03 band) and the overall phi-ladder mass and coupling structure. No open scaffolding remains for this specific equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.