module module high

`IndisputableMonolith.Physics.RunningCouplings`

The RunningCouplings module derives beta functions and running alpha_s from the phi-ladder using J-cost identities. Physicists modeling RG flows or SM parameters cite these results to connect continuous evolution to discrete locking. The structure consists of targeted algebraic lemmas on asymptotic freedom criteria and perturbative anchors.

claim$\phi > 1$, $\beta(\alpha_s)$ from ladder derivative, $b_0^{\rm QCD}$, asymptotic freedom criterion, and $\alpha_s(\mu)$ running with RS anchors at $\phi^{-5}$ scales.

background

This module imports JcostCore, whose core object is the J-cost $J(x) = (x + x^{-1})/2 - 1$ obeying the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. It works in the Recognition Science setting where mass and coupling scales sit on the phi-ladder with eight-tick octave periodicity. The upstream JcostCore module supplies the functional equation that forces phi as the self-similar fixed point and D=3 dimensions.

proof idea

The module opens with the elementary inequality phi_gt_one, then derives beta_function_from_ladder_derivative by differentiating the ladder, computes b0_qcd and b0_sm_positive coefficients, and closes with alpha_s_running together with positivity and perturbative bounds. Each sibling is an independent algebraic reduction; no overarching tactic script.

why it matters in Recognition Science

This module supplies the continuous RG flow that feeds CouplingLockIn, which formalizes the transition from RG flow to discrete geometric locking at the eight-beat plateau. It also supplies the running couplings required by ParticleSummary for Standard Model Parameters derived from Recognition Science. It occupies the RG segment of the T0-T8 forcing chain before discrete locking occurs.

scope and limits

Does not compute explicit numerical running trajectories beyond the RS anchor scale.
Does not treat non-perturbative strong-coupling regimes.
Does not derive beta functions for electroweak or Yukawa couplings.
Does not prove global convergence of the flow to fixed points.

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