Pith. sign in
module module moderate

IndisputableMonolith.Physics.AnomalousMoments

show as:
view Lean formalization →

Module for lepton anomalous magnetic moments on the φ-ladder. Equal charge index Z forces the same dimensionless target, so electron and tau share one RS prediction. Builds a from the Schwinger piece plus an RS gap correction. Cite when comparing RS a_e to PDG. Structure is definitions plus a short universality identity.

claimLeptons with the same charge index $Z$ share one dimensionless anomalous moment on the $\varphi$-ladder: $a_\ell = \mathrm{Schwinger}(\alpha) + \delta_{\mathrm{RS}}(Z_\ell)$, hence $a_e = a_\tau$ when $Z_e = Z_\tau$.

background

Recognition Science places fermion masses and moments on a φ-ladder whose rungs are fixed by a charge-indexed integer Z and a gap display. The RSBridge Anchor module supplies the bridge: twelve SM fermions, $Z_i = \tilde q^2 + \tilde q^4$ (plus 4 for quarks), and $F(Z) = \ln(1+Z/\varphi)/\ln(\varphi)$. Masses sit at an anchor scale via that gap.

Anomalous moments sit one layer up. The classical QED seed is the Schwinger term $\alpha/(2\pi)$. RS adds a dimensionless correction built from the same Z and gap data, so species with equal Z are forced to the same target. Constants and Alpha supply the RS-native $\alpha$ band and the tick $\tau_0$.

The module therefore only needs lepton labels, their Z and gap, the Schwinger piece, the RS correction, and the assembled $a_\ell$, plus a universality statement for equal-Z pairs and hooks to PDG $a_e$.

proof idea

Definition-heavy module, not a deep proof stack. Lepton, Z_lepton, and gap_lepton package the Anchor data for e, μ, τ. schwinger and rs_correction are the two additive pieces; anomalous_moment is their sum. anomalous_e_tau_universal is the one-line identity that equal Z implies equal dimensionless a. pdg_a_e and predicted_a_e are numeric comparison hooks. No multi-step tactic proof is required beyond unfolding equal-Z equality.

why it matters in Recognition Science

Closes the lepton g−2 display in the physics layer: same Z on the φ-ladder yields one dimless target, matching the module doc-comment on universality. Feeds direct comparison of predicted_a_e against PDG without re-deriving α or the gap. Sits downstream of Anchor (ZOf, gap) and Constants.Alpha; no further used_by edges are recorded yet, so this is a leaf prediction module rather than an intermediate lemma. Ties to the broader RS mass formula (yardstick times φ to a rung shifted by gap) by reusing the same Z and F(Z) that fix lepton masses.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (9)