beta_function_from_ladder_derivative
plain-language theorem explainer
The declaration confirms that differentiability of the coupling g at ladder point r follows directly from the given hypothesis. Researchers deriving RS renormalization group flows cite it to license the ladder derivative in the beta function expression. The proof is a one-line term that returns the input hypothesis without further reduction.
Claim. If the coupling function $g:ℝ→ℝ$ is differentiable at the ladder scale point $r$, then $g$ remains differentiable at $r$. This licenses the RS beta function form $β(g)=(1/ℒnφ) dg/dr$ at that point.
background
The module treats renormalization group evolution of couplings via the φ-ladder derivative in Recognition Science. The anchor scale μ*=182.201 GeV is a stationary point of the flow, and asymptotic freedom in QCD follows from the sign of the derivative fixed by the SU(3) structure. Upstream, PhiForcingDerived.of supplies the J-cost structure whose fixed point yields the ladder, while SpectralEmergence.of forces the gauge content SU(3)×SU(2)×U(1) together with three generations.
proof idea
The proof is a one-line term that directly returns the hypothesis hg, confirming the differentiability assumption needed for the ladder derivative.
why it matters
This step underwrites the beta_function_structure result in the module, which writes β(g)=(1/ln φ) dg/dr from the φ-ladder. It supports the asymptotic freedom criterion for n_f≤16 and connects to the phi-forcing chain (T5 J-uniqueness and T6 fixed point) that determines the derivative sign. The declaration closes the differentiability interface required for the running coupling formulas in the RS renormalization paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.