pith. sign in
module module high

IndisputableMonolith.Physics.AnomalousMoments

show as:
view Lean formalization →

The AnomalousMoments module defines RS-derived anomalous magnetic moments for leptons, establishing that equal Z on the phi-ladder yields identical dimensionless targets. Precision QED researchers would cite it when matching g-2 predictions to PDG data. The module consists of definitions for the Schwinger term, RS corrections via the gap function, and an explicit universality statement for electron and tau.

claimThe anomalous magnetic moment satisfies $a = a_S + a_{RS}(Z)$ where $a_S = α/(2π)$ is the Schwinger term and $a_{RS}$ depends on the gap function of $Z$ on the φ-ladder, with universality $a_e = a_τ$ whenever $Z_e = Z_τ$.

background

Recognition Science obtains lepton properties from the phi-ladder and Z-index supplied by the RSBridge.Anchor module. That upstream module defines ZOf as the charge-indexed integer Z_i = q̃² + q̃⁴ (+4 for quarks) and the gap display function F(Z) = ln(1 + Z/φ)/ln(φ). The present module imports the RS time quantum τ₀ = 1 tick and the fine-structure constant α from Constants and Constants.Alpha, then introduces Lepton, Z_lepton, gap_lepton together with schwinger, rs_correction, anomalous_moment and anomalous_e_tau_universal.

proof idea

This is a definition module, no proofs. It assembles the Schwinger term, adds the RS correction constructed from the gap function of Z, defines the general anomalous_moment, and states the universality result anomalous_e_tau_universal that follows directly from equal Z on the φ-ladder.

why it matters in Recognition Science

The module supplies the anomalous-moment definitions imported by the ParticleSummary module to derive Standard Model parameters from Recognition Science. It implements the universality principle stated in the module doc-comment: same dimensionless target from equal Z on the φ-ladder. This supplies the RS link to precision lepton g-2 measurements.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (9)