Physics Coupling Running3 From Jcost

The coupling template

In particle physics, a coupling constant (a number fixing the strength of a force) is not truly constant. Its value changes with the energy scale at which you measure it, an effect called running. The standard model's strong force coupling, alpha_s, runs from about 0.3 at low energies down to a measured value of 0.1179 at the mass of the Z boson, the heavy carrier of the weak force. A framework called Recognition Science proposes that this running follows a specific mathematical rule.

The rule starts with a cost function, J(x) = (x + 1/x)/2 - 1, which the framework derives from five plain conditions on how recognition events (a discrete record of what the universe has distinguished) are priced. The module named CouplingRunning3_FromJcost defines a domain cost as J applied to the ratio of two masses, m and e. It then proves three general facts: the cost is zero when the two masses are equal, the cost is never negative for positive masses, and a threshold value phi - 3/2 (about 0.118) is positive. These are all true for any positive inputs, because they follow from the cost function's own properties.

In Recognition Science, the framework's library (a machine-checked collection of formal theorems) shows that this threshold value matches the measured alpha_s at the Z boson mass. The framework's prediction, alpha_s = J(phi) = 0.118, lands within about 0.1 percent of the measured 0.1179. That agreement is a research note, not a proved theorem. The module itself proves nothing specific to coupling constants, because its definition of domainCost never says what m and e are. The physics enters only through a research note attached to the code, which records where the idea was meant to go.

What the module does establish is a clean template: any physical theory that names its own m and e can reuse these three proved facts. The cost vanishes at equality, stays nonnegative, and has a positive threshold. The coupling prediction, by contrast, depends on identifying m and e with specific particles, an identification the module does not make. The formal result is the template; the physics is the unfinished sentence.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module proves the alpha_s prediction. The module identifies which particles m and e represent. The framework's cost function is derived from recognition events in this module.

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/CouplingRunning3_FromJCost.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: