Pith. sign in
module module high

IndisputableMonolith.Unification.GaugeCouplingsComplete

show as:
view Lean formalization →

Packages the RS gauge-coupling suite: positivity of the electromagnetic α construction (inverse band 137.030–137.039), a φ-structured strong coupling α_s, and the Weinberg angle from φ. Includes geometric-factor identities, PDG-bound checks, a low-energy distinction, and a C-014 certificate. Downstream the Unified Forcing Chain imports it. Content is assembled from Alpha, StrongForce, and WeinbergAngle rather than re-proved from scratch.

claimModule collecting RS gauge couplings: positivity of the electromagnetic construction with $\alpha^{-1}\in(137.030,137.039)$; a derived strong coupling $\alpha_s(M_Z)$ from planar ledger symmetries; a $\varphi$-based weak mixing angle $\sin^2\theta_W$; plus geometric-factor relations, PDG-bound membership, low-energy coupling distinction, and a unification hint under certificate C-014.

background

Recognition Science treats gauge couplings as ledger geometry dressed by $\varphi$, not as free Standard-Model inputs. The electromagnetic seed is assembled as $4\pi\cdot 11$ from cubic-ledger edge combinatorics (AlphaDerivation). That construction supplies an $O(4\pi)$ recognition-scale skeleton and $\varphi$-dressing; it is explicitly not a first-principles derivation of the measured infrared $\alpha^{-1}(0)$, which remains an open boundary datum (AlphaGenesis).

The strong coupling is handled separately (StrongForce, T15): $\alpha_s$ couples to planar symmetries of the ledger, whereas $\alpha$ uses the full edge geometry. The Weinberg angle module (SM-004) targets $\sin^2\theta_W\approx 0.2229$ at the $M_Z$ scale from $\varphi$-structure alone.

This unification module sits above those three developments. Its honest status (2026-07-06) is narrow for electromagnetism: only positivity of the $\alpha$ construction is proved; the exact measured value is excluded by the construction’s first-order prediction at $>30{,}000\sigma$ and is treated as free boundary data.

proof idea

Not a single theorem: a packaging module. It imports Constants.Alpha, AlphaDerivation, Physics.StrongForce, and StandardModel.WeinbergAngle, then exposes sibling results: positivity of the $\alpha$ construction; derived $\alpha_s$ and its numeric value; $\varphi$-based weak mixing with bounds; geometric-factor and formula-distinction lemmas; PDG-bound membership for $\alpha_s$; a gauge-unification hint; low-energy coupling distinction; and the C-014 certificate. Each claim is discharged in its upstream home or by thin wrappers here; the module’s job is assembly and honest status, not a new forcing argument.

why it matters in Recognition Science

Feeds Foundation.UnifiedForcingChain, the top-level module that claims T0–T8 are forced from the Recognition Composition Law and cost foundation. Gauge couplings are the phenomenological bridge from that abstract chain to Standard-Model numbers: $\alpha$ band, $\alpha_s(M_Z)$, and $\theta_W$.

Within the RS landmarks, this is where the fine-structure band $(137.030,137.039)$, the strong-force planar hypothesis, and the $\varphi$-Weinberg link are collected under one certificate (C-014). The honest gap matters: exact infrared $\alpha$ is not forced, so the forcing chain must not silently treat measured $\alpha$ as a theorem. The module’s value is precisely that separation—what is proved (positivity, $\alpha_s$ packaging, $\varphi$-mixing bounds) versus what remains boundary data—before unification rhetoric is attached.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (11)