GmTwoContribution
plain-language theorem explainer
GmTwoContribution enumerates the five canonical contributions to the electron anomalous magnetic moment in the Recognition Science treatment. Physicists modeling g-2 would cite it to fix the count of QED, hadronic, and electroweak terms at the configuration dimension D=5. The declaration is an inductive type whose five constructors directly yield Fintype.card equal to 5.
Claim. The inductive type of contributions to the anomalous magnetic moment consists of five elements: the one-loop QED term, the two-loop QED term, the three-loop QED term, the hadronic term, and the electroweak term.
background
The module treats the electron g-2 as α/π plus corrections, with the RS model supplying α ≈ 2/17 × correction and J(φ) ≈ 0.118. Five canonical contributions are listed explicitly: QED 1-loop, QED 2-loop, QED 3-loop, hadronic, and electroweak. These are identified with configDim D = 5, matching the framework's use of five terms to reproduce the observed structure in RS-native units.
proof idea
The declaration is an inductive definition introducing exactly five constructors. No lemmas or tactics are applied; the type is introduced directly and its cardinality is recovered by the Fintype instance derived from the constructors.
why it matters
The definition supplies the five_contributions field of GMTwoCert and is counted by the theorem gmTwoCount. It thereby anchors the g-2 expansion to the RS claim that α/π arises from 2/(17π) structure and supports the downstream wolfensteinA = 9/11 relation for α_s predictions. It fills the enumeration step required by the five-dimensional configuration space in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.