module module high

`IndisputableMonolith.Physics.RunningCouplings`

RunningCouplings module derives the beta function for the strong coupling directly from the phi-ladder derivative inside the J-cost framework and proves the positivity conditions required for asymptotic freedom. Physicists modeling renormalization-group evolution inside Recognition Science cite these lemmas when linking continuous flow to the eight-tick geometric locking. The proofs are short algebraic reductions that apply the Recognition Composition Law and the explicit form of J to the ladder derivative.

claim$J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ implies the beta function for the strong coupling via differentiation along the phi-ladder; the leading coefficient $b_0$ is positive precisely when the number of flavors lies below the critical value, guaranteeing asymptotic freedom.

background

The module imports the J-cost core, whose central object is the function $J(x)=(x+x^{-1})/2-1$ obeying the Recognition Composition Law. From this identity the module extracts the phi-ladder whose rungs label mass scales in units of the recognition yardstick. The local theoretical setting is the continuous renormalization-group flow that must later lock onto the discrete eight-tick octave of Recognition Science.

proof idea

phi_gt_one is immediate from the fixed-point equation for the self-similar solution. beta_function_from_ladder_derivative differentiates the ladder expression with respect to the logarithmic scale variable. b0_qcd and b0_sm_positive evaluate the resulting coefficient at the physical flavor numbers. asymptotic_freedom_criterion and no_asymptotic_freedom_17 compare the sign of b0 against the critical flavor number obtained from the same derivative.

why it matters in Recognition Science

The lemmas supply the running-coupling input required by CouplingLockIn, whose doc-comment states that the module formalizes the transition from continuous RG flow to discrete geometric locking at the eight-beat plateau. They also feed ParticleSummary, which assembles Standard Model parameters from Recognition Science. The results therefore close the step that converts the J-cost identity into perturbative QCD-like behavior inside the RS framework.

scope and limits

Does not compute numerical running trajectories for alpha_s at specific scales.
Does not derive beta functions for the electroweak couplings.
Does not include higher-loop or non-perturbative corrections.
Does not address flavor thresholds or decoupling effects.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.CouplingLockIn module_import
IndisputableMonolith.Physics.ParticleSummary module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (33)

theorem phi_gt_one L32
theorem beta_function_from_ladder_derivative L44
def b0_qcd L53
theorem b0_sm_positive L56
theorem asymptotic_freedom_criterion L61
theorem no_asymptotic_freedom_17 L68
theorem critical_flavor_number L73
def alpha_s_running L82
theorem alpha_s_positive L86
def rs_anchor_scale L94
def rs_alpha_s_anchor L97
theorem rs_alpha_s_perturbative L100
def rs_alpha_s_MZ L105
theorem rs_alpha_s_MZ_range L109
def rs_weinberg_angle_sq L194
theorem weinberg_angle_in_range L197
structure GUTUnification L215
theorem gut_above_ew L221
def mass_anomalous_dim L241
def mass_evolution_exp L244
theorem mass_anomalous_dim_pos L247
theorem mass_evolution_exp_pos L250
theorem mass_evo_exp_nf3 L257
theorem mass_evo_exp_nf4 L259
theorem mass_evo_exp_nf5 L261
theorem mass_evo_exp_nf6 L263
def running_mass L268
theorem mass_ratio_rg_invariant L273
structure FlavorThreshold L281
def charm_threshold L288
def bottom_threshold L295
def top_threshold L302
def transport_mass_through L311