Physics Rgtransport Certificate

The certified transport exponents

In particle physics, the values of coupling constants are not fixed once and for all. They depend on the energy scale at which you measure them, a behavior called running. The renormalization group describes this running, and its equations tell you how to transport a coupling from one scale to another. The Recognition Science framework needs such transport for its own particle ladder, and it records the result in a module called the RG transport certificate.

The certificate is a definition, not a theorem. It fixes nine rational numbers, one for each fermion in the framework's list: electron, muon, tau, up, down, strange, charm, bottom, top. Each number is the certified transport exponent, written f^RG, that the framework's canonical policy produces. The electron gets 494/10000, the muon 288/10000, the tau 179/10000, and so on through the list. A tenth entry, for any other fermion, is simply zero.

These values come from an external certificate, a snapshot of a declared transport policy that specifies loop order, thresholds, scheme, and integrator. They are not fit parameters of the model layer, and they are not derived from the forcing chain. The policy snapshot lives in a JSON file, and the certificate records the floating-point results. Any comparison against measured particle data must declare this policy seam, because the numbers are conventions, not consequences.

The module also proves a small set of formal facts about the certificate. It shows the tolerance is nonnegative, that the lower and upper endpoints of the certified interval are ordered, and that the center value lies inside its own interval. One theorem states an equivalent form: a value is certified exactly when its absolute error from the center is at most the tolerance. These proofs are machine-checked, but they establish only the arithmetic of the enclosure, not the physics of the transport.

In Recognition Science, the certificate is a bridge between the framework's discrete ladder and the continuous running of couplings. It supplies the numbers that a comparison against measured data would use, with a declared tolerance of one part in ten thousand. What it does not do is derive those numbers from first principles. The transport policy is a choice, and the certificate records it faithfully.

/-- Certified SM RG transport exponent f^RG_i(μ*, μ_end) from canonical policy. -/
def f_RG_certified : Fermion → ℚ
  | .e   => 494/10000
  | .mu  => 288/10000
  | .tau => 179/10000
  | .u   => 4822/10000
  | .d   => 4764/10000
  | .s   => 4764/10000
  | .c   => 5470/10000
  | .b   => 3807/10000
  | .t   => 98/10000
  | _    => 0

/-- Certified SM RG transport exponent f^RG_i(μ*, μ_end) from canonical policy. -/
def f_RG_certified : Fermion → ℚ
  | .e   => 494/10000
  | .mu  => 288/10000
  | .tau => 179/10000
  | .u   => 4822/10000
  | .d   => 4764/10000
  | .s   => 4764/10000
  | .c   => 5470/10000
  | .b   => 3807/10000
  | .t   => 98/10000
  | _    => 0

/-- Equivalent absolute-error enclosure form for certified transport values. -/
theorem is_certified_iff_abs_error_le (f : Fermion) (val : ℝ) :
    is_certified f val ↔
      |val - (f_RG_certified f : ℝ)| ≤ (f_RG_tolerance : ℝ) := by
  constructor
  · intro h
    rcases h with ⟨hlo, hhi⟩
    have h1 : -((f_RG_tolerance : ℚ) : ℝ) ≤ val - (f_RG_certified f : ℚ) := by
      linarith
    have h2 : val - (f_RG_certified f : ℚ) ≤ ((f_RG_tolerance : ℚ) : ℝ) := by
      linarith
    exact abs_le.mpr ⟨h1, h2⟩
  · intro h
    have h' := abs_le.mp h
    constructor <;> linarith [h'.1, h'.2]

/-- The certified center value is enclosed for every fermion. -/
theorem certified_center_enclosed (f : Fermion) :
    is_certified f (f_RG_certified f) := by
  unfold is_certified
  have htol_nonneg : (0 : ℝ) ≤ (f_RG_tolerance : ℝ) := by
    exact_mod_cast f_RG_tolerance_nonneg
  constructor
  · exact sub_le_self _ htol_nonneg
  · exact le_add_of_nonneg_right htol_nonneg

What this page does not claim

The certified transport exponents are not derived from the framework's forcing chain. The module does not prove that the certified values match any measured particle data. The transport policy is not a fit parameter of the model layer; it is an external convention that must be declared.

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