Pith. sign in
module module high

IndisputableMonolith.Unification.GaugeCouplingsComplete

show as:
view Lean formalization →

This module assembles the complete set of gauge couplings in Recognition Science by importing derivations for the electromagnetic, strong, and weak sectors. A physicist constructing low-energy Standard Model parameters from cubic ledger geometry would cite it for the unified constants. The structure composes prior results from AlphaDerivation, StrongForce, and WeinbergAngle without introducing new proofs.

claim$\alpha = 1/(4\pi \cdot 11 \cdot \exp(f_{\rm gap}/(4\pi \cdot 11)))$ with $\alpha^{-1} \approx 137.036$, $\alpha_s(M_Z)$ from planar symmetries, and $\sin^2 \theta_W ≈ 0.2229$ from $\phi$-structure.

background

The module sits inside the cubic ledger geometry of AlphaDerivation, where 4π emerges from Gauss-Bonnet applied to vertex deficits of the 3-cube. It contrasts the full edge geometry used for the fine-structure constant with the planar symmetries that govern the strong coupling in StrongForce. The weak sector enters via the ϕ-based derivation of the Weinberg angle in the imported WeinbergAngle module, targeting the electroweak mixing parameter at the MZ scale.

proof idea

This is a definition module, no proofs. The argument proceeds by importing the four source modules and exposing their combined results through sibling declarations that certify each coupling and the overall C-014 certificate.

why it matters in Recognition Science

The module supplies the complete low-energy gauge couplings that close the C-014.1 electromagnetic derivation and support the broader unification program. It directly incorporates the cubic-geometry origin of α, the planar-symmetry origin of αs, and the ϕ-structure origin of θW, feeding these into any downstream unification statement.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (11)