gmTwoCert
plain-language theorem explainer
gmTwoCert constructs the certificate for the anomalous magnetic moment in Recognition Science by populating the GMTwoCert structure with exactly five contributions and the Wolfenstein parameter fixed at 9/11. Physicists deriving g-2 from RS constants would cite it to confirm the term count matches configDim D=5. The definition is a direct record construction that applies the decided cardinality theorem and the reflexivity equality.
Claim. The certificate for the anomalous magnetic moment is the structure requiring the cardinality of GmTwoContribution to equal 5 and the Wolfenstein parameter to equal 9/11.
background
In the module on Anomalous Magnetic Moment from RS, g-2 is expressed via α/π with RS corrections, where five canonical contributions (QED 1-loop through 3-loop, hadronic, EW) match configDim D=5. The structure GMTwoCert requires two fields: five_contributions as Fintype.card GmTwoContribution = 5 and wolfenstein as wolfensteinA = 9/11. The upstream theorem gmTwoCount proves the cardinality by decision procedure. The upstream theorem wolfensteinA_eq proves the parameter equality by reflexivity.
proof idea
The definition constructs an instance of GMTwoCert by direct record assignment, setting five_contributions to the result of gmTwoCount and wolfenstein to the result of wolfensteinA_eq. It is a one-line wrapper that applies the two upstream results with no further reduction.
why it matters
This definition supplies the concrete certificate confirming five contributions and Wolfenstein A = 9/11, closing the structure for RS-derived g-2 calculations that link to the alpha band and the five-dimensional configuration. It fills the module's claim that g-2 = α/π times corrections with J(φ) factors. No downstream theorems are listed, leaving open whether the certificate feeds into a full numerical match with experiment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.