Constants Strong Coupling Strong Coupling Cert

The strong coupling certificate

The strong coupling constant, written α_s, measures how powerfully quarks and gluons bind inside protons and neutrons. At the mass of the Z boson, the particle that carries the weak force, the Particle Data Group's 2024 review gives α_s(M_Z) = 0.1180 ± 0.0009. This is one of the most precisely measured numbers in particle physics, and it is not predicted by the Standard Model; it must be measured and then plugged into calculations.

Recognition Science (RS) attempts to derive such constants from a single starting point: reality keeps a discrete record of recognition events, and the cost of recognition is forced by a proved theorem. In this framework, the three gauge couplings at a unification scale come from a cube's geometry. The strong sector uses the remaining degrees of freedom after the electromagnetic and weak sectors take theirs. The structural claim is that α_s(M_Z) equals φ^−k for some integer k, where φ is the golden ratio, with the integer determined by how the coupling runs from the recognition scale down to M_Z.

The declaration StrongCouplingCert, a machine-checked certificate in the framework's library of formal theorems, establishes three precise facts. First, the predicted value α_s_prediction = φ⁻³/π is positive. Second, the sum of inverse couplings at the recognition scale satisfies 1/α_EM + 1/α_weak + 1/α_s = 12π, the framework's analog of gauge coupling unification. Third, this sum lies strictly between 36 and 48. These are theorems, proved in the machine-checked library with no unproved assumptions. The certificate bundles them into a single object and proves that this object exists.

What the certificate does not claim matters as much as what it proves. It does not assert that α_s(M_Z) numerically matches the measured 0.1180. The predicted expression φ⁻³/π ≈ 0.0477 is far from the measured value at the Z mass; the framework's claim is about the structure at the recognition scale, not a direct prediction at M_Z. The certificate also does not prove that the integer k in φ^−k is 3, nor that the running from the recognition scale to M_Z follows any particular renormalization group equation. The certificate's gauge_sum_value theorem establishes the sum equals 12π by definition of the prediction, not by derivation from deeper principles. The physical bridge from the recognition scale to the Z mass remains open.

In plain terms, the certificate is a rigorous record of what the framework's geometry implies about the gauge couplings' structure, and an explicit acknowledgment of where the derivation stops. It proves the algebraic skeleton: positivity, a specific sum rule, and bounds on that sum. It leaves open the dynamical content: the running, the integer k, and the numerical match to experiment. A reader can trust the three proved facts completely, and know exactly which questions remain targets for future work.

noncomputable def alpha_s_prediction : ℝ := phi ^ (-(3 : ℤ)) / Real.pi

structure StrongCouplingCert where
  positive : 0 < alpha_s_prediction
  gauge_structure : gauge_sum_prediction = 12 * Real.pi
  gauge_bounded : (36 : ℝ) < gauge_sum_prediction ∧ gauge_sum_prediction < 48

theorem strong_coupling_cert_exists : Nonempty StrongCouplingCert :=
  ⟨{ positive := alpha_s_positive
     gauge_structure := gauge_sum_value
     gauge_bounded := gauge_sum_bounds }⟩

theorem alpha_s_positive : 0 < alpha_s_prediction := by
  unfold alpha_s_prediction
  exact div_pos (zpow_pos phi_pos _) Real.pi_pos

theorem gauge_sum_value : gauge_sum_prediction = 12 * Real.pi := by
  unfold gauge_sum_prediction cube_edges
  simp [D]

theorem gauge_sum_bounds :
    (36 : ℝ) < gauge_sum_prediction ∧ gauge_sum_prediction < (48 : ℝ) := by
  rw [gauge_sum_value]
  constructor <;> nlinarith [Real.pi_gt_three, Real.pi_lt_four]

What this page does not claim

The certificate does not prove that α_s(M_Z) numerically matches the measured 0.1180. The certificate does not establish that the integer k in φ^−k equals 3. The certificate does not derive the running of the coupling from the recognition scale to M_Z.

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/Constants/StrongCoupling.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: