pith. sign in
module module high

IndisputableMonolith.Unification.GaugeCouplingsComplete

show as:
view Lean formalization →

The GaugeCouplingsComplete module assembles derivations of the electromagnetic coupling α, strong coupling α_s, and Weinberg angle θ_W from Recognition Science geometry. A physicist modeling unification would cite it for the complete low-energy gauge sector obtained without free parameters. The module composes imported results from AlphaDerivation, StrongForce, and WeinbergAngle to certify the full set under the C-014.1 geometric seed.

claimThe fine-structure constant satisfies $α = [4π·11·exp(f_gap/(4π·11))]^{-1}$ with $α^{-1}≈137.036$, the strong coupling $α_s(M_Z)$ follows from planar ledger symmetries, and the weak mixing angle obeys $sin^2θ_W≈0.2229$ from φ-structure, all derived from D=3 cube geometry.

background

This module sits in the unification domain and imports the cubic ledger derivation of α from AlphaDerivation, where 4π arises via Gauss-Bonnet on vertex deficits of Q3. StrongForce supplies the planar-symmetry origin of α_s while distinguishing it from the full-edge 4π·11 geometry used for α. WeinbergAngle contributes the φ-based electroweak mixing with target sin²θ_W≈0.2229 at the M_Z scale. The DOC_COMMENT states the explicit gap-corrected formula and notes that positivity follows directly from the geometric seed.

proof idea

This is a composition module with no internal proofs. It imports the four upstream modules and assembles their results to realize the complete gauge-coupling set under C-014.1.

why it matters in Recognition Science

The module completes the gauge sector under C-014.1 and supplies the explicit values for α, α_s, and θ_W that feed downstream unification claims. It realizes the D=3 and φ-ladder landmarks by delivering the alpha band (137.030,137.039) and related constants from the forcing chain without adjustable parameters. No downstream declarations are listed, so its immediate role is to certify the low-energy coupling predictions.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (11)