pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Experimental.MuonGMinusTwo

show as:
view Lean formalization →

This module assembles Recognition Science definitions for the muon g-2 anomaly built on the derived fine-structure constant. Experimental physicists testing RS predictions against Fermilab data would cite the alpha_em and a_mu_rs_prediction objects. The module proceeds through a chain of definitions establishing the Schwinger term, gap factors, and the RS excess over the Standard Model reference value.

claimThe module supplies the RS fine-structure constant $α_{em} ≈ 1/137.036$ together with the muon anomalous moment prediction $a_μ^{RS}$ and the comparison $a_μ^{RS} > a_μ^{SM}$ via the counter-term and gap factor on the phi-ladder.

background

The module imports the RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants and operates in the experimental domain. It introduces the electromagnetic coupling α_em constrained to the interval whose inverse lies in (137.030, 137.039), the positive Schwinger term, the muon rung on the phi-ladder, and the gap_1332_factor that enters the mass formula yardstick · φ^(rung − 8 + gap(Z)). The local setting is the Recognition Composition Law and the eight-tick octave that fix D = 3 and the alpha band.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete RS prediction for the muon g-2 anomaly that tests the framework against experiment. It connects to the T8 forcing chain through the value of alpha and the eight-tick octave. No parent theorems are listed in the used-by graph yet; the definitions stand ready for downstream comparison lemmas.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)