Unification Gauge Couplings Complete

Gauge couplings and their geometry

In particle physics, a coupling constant measures the strength of a fundamental force. The fine-structure constant α governs electromagnetism, α_s governs the strong force, and the weak mixing angle sin²θ_w governs the weak force. Each is a measured number, not something the Standard Model predicts from first principles.

Recognition Science (RS) proposes that these numbers are forced by the geometry of a discrete ledger, a record of recognition events. The framework's machine-checked library of formal theorems contains a module, unification gauge couplings complete, that derives each coupling from a distinct geometric structure. The electromagnetic seed is 4π·11, a factor tied to cube edges. The strong coupling is α_s = 2/17, where 17 counts the wallpaper groups, the 17 distinct repeating patterns in two dimensions. The weak mixing angle is predicted as sin²θ_w = (3 - φ)/6, where φ is the golden ratio. These are derivations, not fits.

The module proves the formulas as theorems. It shows α_s_pred = 2/17 and that this value, 0.1176, lies within the experimental error of the measured PDG 2022 value 0.1179 ± 0.0009. It proves the weak mixing prediction falls between 0.22 and 0.24, matching the observed 0.2229 within about three percent. For the fine-structure constant, the theorem is weaker: it proves only that the construction for α is positive, not that it equals the measured value. The exact value of α remains an open problem.

What the module does not establish is gauge unification itself. Grand unified theories predict the three couplings meet at a high energy scale around 10¹⁶ GeV. The module states this meeting is open, and nothing in it bears on the question. Stating it requires the renormalization-group running of the couplings, which the development lacks. The claim that the three couplings converge at high energy is not a theorem in this library.

The consequence of the module is a structural claim: the three couplings differ at low energy because each measures a different geometric structure. α comes from charge coupling with the seed 4π·11, α_s from color with the seventeen wallpaper groups, and the weak mixing from the 3/8 ratio of the gauge group. The theorems establish these origins. The unification that would tie them together remains a target.

/-- **C-014.2**: Strong coupling α_s (at M_Z).

    Derived from wallpaper groups: α_s = 2/17 ≈ 0.1176
    Matches PDG 2022: 0.1179 ± 0.0009

    **Formula**: α_s = 2/W where W = 17 -/
theorem alpha_s_coupling_derived : alpha_s_pred = 2 / 17 := by
  simp only [alpha_s_pred, alpha_s_geom]
  norm_num

/-- **C-014.3**: Weak mixing angle sin²θ_w (from φ-structure).

    Best φ-based prediction: sin²θ_w = (3 - φ) / 6 ≈ 0.230
    Observed value: 0.2229 ± 0.0003
    Match: Within ~3%

    **Formula**: sin²θ_w = (3 - φ) / 6 -/
theorem weak_mixing_phi_based : bestPrediction = (3 - phi) / 6 := by
  unfold bestPrediction prediction3
  rfl

/-- **BOUNDS**: α_s is within experimental error of PDG value. -/
theorem alpha_s_within_pdg_bounds : abs (alpha_s_pred - 0.1179) < 0.0009 :=
  alpha_s_match

/-- **C-014.1**: Electromagnetic coupling α (fine-structure constant).

    HONEST STATUS (2026-07-06): the theorem proved here is ONLY positivity
    of the α CONSTRUCTION (band (137.030, 137.039)). The exact measured
    value of α is NOT derived: within RS it is a free boundary datum
    (`Constants.AlphaGenesis.KappaGammaIrreducibility`), and the
    construction's first-order value is excluded by measurement at
    >30,000σ (`Constants.AlphaGenesis.MeasurementVerdict`).

    **Proved**: α > 0 (positivity of the construction; formerly misnamed
    `alpha_coupling_derived`). -/
theorem alpha_construction_pos : alpha > 0 := by
  unfold alpha alphaInv alpha_seed
  positivity

@[deprecated alpha_construction_pos (since := "2026-07-06")]
alias alpha_coupling_derived := alpha_construction_pos

What this page does not claim

The exact value of the fine-structure constant is not derived in this module. The module does not prove that the three couplings converge at high energy. The weak mixing prediction of (3 - φ)/6 is not the tree-level 3/8 value.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Unification/GaugeCouplingsComplete.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: