Physics Rgtransport

The transport bridge

In particle physics, the mass of a fermion such as an electron or quark is not a fixed number. It changes with the energy scale at which you measure it, a behavior called running. The renormalization group equation describes this: d(ln m)/d(ln μ) = -γ_m(μ), where γ_m is the mass anomalous dimension, a function of the coupling constants at that scale. The physics-rgtransport module formalizes the mathematical bridge between this running and the mass formula used in Recognition Science.

The module defines the integrated residue, the accumulated effect of the anomalous dimension as the scale runs from a reference point μ₀ to a final scale μ₁. The formula is f(μ₀, μ₁) = (1/λ) ∫ γ_m(μ') d(ln μ'), where λ = ln φ, the natural logarithm of the golden ratio. This residue is the exponent that connects the structural mass, defined at an anchor scale μ⋆ = 182.201 GeV, to the physical mass: m(μ⋆) = m_phys · φ^{f(μ⋆, m_phys)}.

In Recognition Science, the framework models the physical mass as a phi-power ladder. The transport module proves the connection theorems that make this ladder precise. The theorem mass_ratio_phi_power shows that the exponential of the negative transport integral equals phi raised to the residue power. The theorem stationarity_iff_gamma_zero proves that the residue is stationary at the anchor scale exactly when the anomalous dimension vanishes there, a fixed-point condition.

The module is deliberately a framework, not a full calculation. It defines the structures AnomalousDimension and RunningCoupling with the properties they must satisfy, such as smoothness and perturbative bounds. It provides the one-loop QCD and QED beta functions and anomalous dimensions as concrete examples. But it does not contain the four-loop QCD or two-loop QED kernels; those require extensive Standard Model machinery. The module provides the mathematical skeleton that such kernels would plug into.

What this establishes in plain language: the framework's mass formula is not a disconnected numerology. It is tied to the standard running of masses through a well-defined integral. The bridge is proved in a machine-checked library of formal theorems, meaning the mathematics is verified step by step. The physical content, the actual kernels, remains an open target for future work.

/-- The integrated residue from ln-scale `lnμ₀` to `lnμ₁`.

    `f(μ₀, μ₁) = (1/λ) ∫_{lnμ₀}^{lnμ₁} γ(exp(t)) dt`

    This is the abstract definition; the actual computation requires the SM kernels.
    We parameterize by an `AnomalousDimension` structure. -/
def integratedResidue (γ : AnomalousDimension) (f : Fermion) (lnμ₀ lnμ₁ : ℝ) : ℝ :=
  (1 / lambda) * ∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t)

/-- The mass ratio in φ-power form.

    If `m(μ₁)/m(μ₀) = exp(-λ · f)`, then `m(μ₁)/m(μ₀) = φ^{-f}`.

    Note: `-lambda * f_residue` parses as `(-lambda) * f_residue` by precedence. -/
theorem mass_ratio_phi_power (f_residue : ℝ) :
    Real.exp (-lambda * f_residue) = phi ^ (-f_residue) := by
  have hphi_pos : 0 < phi := lt_trans (by norm_num : (0 : ℝ) < 1) one_lt_phi
  simp only [lambda]
  -- `-Real.log phi * f_residue` equals `Real.log phi * (-f_residue)`
  have h1 : -Real.log phi * f_residue = Real.log phi * (-f_residue) := by ring
  rw [h1]
  -- Now goal is: Real.exp (Real.log phi * -f_residue) = phi ^ (-f_residue)
  have h2 : Real.log phi * -f_residue = -f_residue * Real.log phi := by ring
  rw [h2, ← Real.log_rpow hphi_pos, Real.exp_log (Real.rpow_pos_of_pos hphi_pos _)]

theorem stationarity_iff_gamma_zero (γ : AnomalousDimension) (f : Fermion) :
    residueDerivative γ f lnMuStar = 0 ↔ γ.gamma f muStar = 0 := by
  simp only [residueDerivative, lnMuStar]
  rw [Real.exp_log muStar_pos]
  have hlambda : lambda ≠ 0 := ne_of_gt lambda_pos
  constructor
  · intro h
    have hmul : (1 / lambda) * γ.gamma f muStar = 0 := h
    have h1 : (1 / lambda) ≠ 0 := one_div_ne_zero hlambda
    exact (mul_eq_zero.mp hmul).resolve_left h1
  · intro h
    simp [h]

What this page does not claim

The module does not provide the actual QCD or QED kernels. The module does not prove that the transport integral equals the empirical residue for any specific particle. The module does not derive the value of the anchor scale μ⋆.

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