g2Default
plain-language theorem explainer
Defines the canonical Recognition Spec value of the muon anomalous magnetic moment as $\varphi^{-5}$. Spec authors and dimensionless-pack constructors cite it when wiring the universal dimless pack and the honest-closure certificate. The body is a one-line algebraic abbreviation, marked simp.
Claim. For a real parameter $\varphi$, the default muon $g-2$ entry of the Recognition Spec is $g_{2}^{\mathrm{default}}(\varphi) := \varphi^{-5}$.
background
RecogSpec assembles the dimensionless observables that Recognition Science claims are fixed by the golden ratio $\varphi$. Among them sits the muon anomalous magnetic moment $a_\mu = (g-2)/2$, carried in the pack as a single real slot rather than a full QED expansion.
In RS-native units the same power appears as $\hbar = \varphi^{-5}$. The present definition therefore reuses that algebraic token as a toy, spec-level stand-in for the muon $g-2$ entry: pure inverse fifth power of $\varphi$, with no loop corrections or hadronic vacuum polarization.
Sibling defaults in the same module (alphaDefault, massRatiosDefault, mixingAnglesDefault) play the same role for the fine-structure constant, mass ratios, and mixing angles. Together they feed the explicit universal dimless pack.
proof idea
Pure definitional abbreviation. The right-hand side is the field expression $1/\varphi^5$ (Nat exponent), tagged @[simp] so downstream rewrites unfold it automatically. No lemmas are invoked.
why it matters
Supplies the g2Muon / g2Muon0 field of dimlessPack_explicit and UD_explicit, the concrete witnesses that every dimensionless observable in the pack is a closed expression in $\varphi$. Those packs are then consumed by HonestClosureCert, whose Part A requires all observables to be $\varphi$-closed.
In the broader framework this is the same power that appears as $\hbar = \varphi^{-5}$ in RS-native units (primer constants). It is explicitly labelled a toy formula at the CERT(definitional) level: a placeholder that keeps the pack well-typed and $\varphi$-closed while a sharper $g-2$ derivation is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.