gmTwoCount
plain-language theorem explainer
The Recognition Science model enumerates exactly five contributions to the electron anomalous magnetic moment. A physicist working on g-2 anomalies would cite this to confirm the count of QED, hadronic, and electroweak terms matches the standard decomposition. The proof is a one-line decision procedure that inspects the inductive definition of the contribution type.
Claim. The finite set of canonical contributions to the electron anomalous magnetic moment (QED 1-loop, QED 2-loop, QED 3-loop, hadronic, electroweak) has cardinality 5.
background
The module treats the anomalous magnetic moment via g-2 = α/π plus corrections, with RS expressing the leading term through J(φ)/φ⁴. Five canonical contributions are isolated: QED 1-loop, QED 2-loop, QED 3-loop, hadronic, and electroweak. These are formalized as the inductive type GmTwoContribution whose constructors are exactly those five cases, each deriving Fintype so that cardinality is decidable. Upstream results supply the active-edge count A = 1 from IntegrationGap, Masses.Anchor, and Modal.Actualization, together with the same inductive type, to anchor the enumeration inside the broader forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic evaluates Fintype.card directly on the inductive type by enumerating its five constructors and confirming the finite cardinality equals 5.
why it matters
This theorem supplies the five_contributions field of the downstream gmTwoCert certificate. It fills the enumeration step required for the RS g-2 formula that links α/π structure to the five-term decomposition, consistent with configDim D = 5 and the eight-tick octave in the T0-T8 forcing chain. The result closes the counting prerequisite before any numerical evaluation of the moment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.