Encyclopedia Physics Physics Gauge Coupling Hierarchy Score Card

ARTICLE 5 claims 3 theorems 1 measured

Physics Gauge Coupling Hierarchy Score Card

A machine-checked module that certifies a proposed hierarchy of the three Standard Model gauge couplings, and honestly reports how far it falls short of measurement.

The scorecard's verdict

In particle physics, the three fundamental forces of the Standard Model, electromagnetism, the weak force, and the strong force, each have a coupling constant, a number that sets how strongly particles interact through that force. The inverse of these couplings, written α⁻¹, are about 137 for electromagnetism, roughly 30 for the weak force, and near 0.12 for the strong force. A gauge coupling hierarchy is any proposed mathematical pattern that relates these three numbers to each other and to more basic constants.

The Recognition Science framework proposes such a hierarchy. Its module, the gauge coupling hierarchy score card, defines three specific formulas. The inverse electromagnetic coupling is claimed to lie in the band (137.030, 137.039). The weak mixing angle, which connects the electromagnetic and weak sectors, is defined as sin²θ_W = (3 − φ)/6, where φ is the golden ratio. The strong coupling is set as α_s = φ⁻³/π. The module also asserts a gauge sum: the three inverse couplings add to 12π. All of these are presented with zero free parameters, meaning no numbers are fitted to experiment.

The scorecard's own theorems verify internal consistency. It proves the electromagnetic inverse coupling is greater than the weak one, that sin²θ_W is positive and less than one, and that the strong coupling is positive. These are all ledger facts, meaning they follow from the framework's discrete record of recognition events, not from any measurement. The module bundles these into a certificate structure, a formal object that packages all the claims together, and proves the certificate exists.

The module is also honest about what its band is not. The band (137.030, 137.039) is about 429,000 times wider than the CODATA 2022 measured value 137.035999177(21). The framework's own library proves the construction value is excluded by that measurement at more than 30,000 sigma. The band is a certified window of the construction, not a claim about the measured fine-structure constant. The module does not derive the measured value; it only certifies that its own formula lands somewhere in a wide interval that also happens to contain the measurement.

In plain language, the scorecard does three things. It writes down a proposed pattern for the three gauge couplings. It machine-checks that the pattern is internally consistent and has no free parameters. And it states plainly that the pattern's electromagnetic prediction is wildly imprecise compared to experiment, so the pattern is not a successful derivation of the measured constants.

THEOREM alpha_inv_em_band · IndisputableMonolith/Physics/GaugeCouplingHierarchyScoreCard.lean
/-- α⁻¹_EM is in (137.030, 137.039). -/
theorem alpha_inv_em_band :
    (137.030 : ℝ) < alphaInv ∧ alphaInv < 137.039 :=
  ⟨Numerics.alphaInv_gt, Numerics.alphaInv_lt⟩
MODEL sin2_W_rs · IndisputableMonolith/Physics/GaugeCouplingHierarchyScoreCard.lean
/-- sin²θ_W from RS. -/
def sin2_W_rs : ℝ := (3 - phi) / 6
THEOREM em_exceeds_weak · IndisputableMonolith/Physics/GaugeCouplingHierarchyScoreCard.lean
/-- The hierarchy: α⁻¹_EM > α⁻¹_weak (since sin²θ_W < 1). -/
theorem em_exceeds_weak : alphaInv > alpha_weak_inv := by
  unfold alpha_weak_inv
  have hα : 0 < alphaInv := by linarith [Numerics.alphaInv_gt]
  have hsin : sin2_W_rs < 1 := sin2_W_lt_one
  nlinarith [mul_lt_mul_of_pos_left hsin hα]
MEASURED alpha_inv_em_band · IndisputableMonolith/Physics/GaugeCouplingHierarchyScoreCard.lean
/-- α⁻¹_EM is in (137.030, 137.039). -/
theorem alpha_inv_em_band :
    (137.030 : ℝ) < alphaInv ∧ alphaInv < 137.039 :=
  ⟨Numerics.alphaInv_gt, Numerics.alphaInv_lt⟩
THEOREM alpha_inv_em_band · IndisputableMonolith/Physics/GaugeCouplingHierarchyScoreCard.lean
/-- α⁻¹_EM is in (137.030, 137.039). -/
theorem alpha_inv_em_band :
    (137.030 : ℝ) < alphaInv ∧ alphaInv < 137.039 :=
  ⟨Numerics.alphaInv_gt, Numerics.alphaInv_lt⟩

What this page does not claim

The scorecard derives the measured fine-structure constant. The band (137.030, 137.039) is a prediction that agrees with experiment. The formulas for the weak and strong couplings are verified against measurement.

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/Physics/GaugeCouplingHierarchyScoreCard.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND