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

IndisputableMonolith.Unification.GaugeCouplingsComplete

show as:
view Lean formalization →

GaugeCouplingsComplete assembles derivations of the electromagnetic coupling α from D=3 cubic geometry, the strong coupling α_s from planar ledger symmetries, and the Weinberg angle from φ-structure. Physicists studying geometric origins of Standard Model parameters would cite the module for its first-principles values and PDG-bound certifications. The module organizes content through imports from AlphaDerivation, StrongForce, and WeinbergAngle plus sibling definitions that certify the results.

claimThe module establishes the electromagnetic coupling via $α = 1/α_{inv}$ where $α_{inv} = 4π·11·exp(f_{gap}/(4π·11))$, the strong coupling $α_s(M_Z)$ from planar symmetries of the ledger, and the weak mixing angle satisfying $sin²θ_W ≈ 0.2229$ at the $M_Z$ scale.

background

The module operates in the Unification domain, combining gauge couplings from upstream derivations. AlphaDerivation supplies the constructive origin of α^{-1} ≈ 137.036 from vertex deficits of the cubic ledger Q_3 via Gauss-Bonnet, yielding the structural 4π factor. StrongForce formalizes α_s(M_Z) as coupling to planar symmetries, distinct from the full edge geometry used for α. WeinbergAngle derives θ_W from RS φ-structure with sin²(θ_W) ≈ 0.2229 at the M_Z scale.

proof idea

This is a definition module, no proofs. It imports Alpha, AlphaDerivation, StrongForce, and WeinbergAngle to define sibling results such as alpha_coupling_derived, alpha_s_coupling_derived, weak_mixing_phi_based, and gauge_unification_hint.

why it matters in Recognition Science

The module completes the gauge couplings sector, realizing C-014.1 for the electromagnetic coupling and extending to strong and weak sectors. It feeds broader Recognition Science unification by grounding Standard Model parameters in the T0-T8 forcing chain and Recognition Composition Law, with constants in RS-native units where c=1 and ħ=φ^{-5}.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (11)