asymptotic_freedom_direction
plain-language theorem explainer
For positive beta coefficient b the running coupling at positive phi-ladder rung n is strictly smaller than the reference value alpha0. QCD modelers embedding asymptotic freedom into Recognition Science phi-scaling would cite this when deriving the decrease of strong coupling with energy. The proof reduces directly to positivity of log phi and a division inequality after unfolding the explicit runningCoupling formula.
Claim. Let $alpha_0 > 0$, $b > 0$, and positive integer $n > 0$. Then the running coupling at rung $n$ satisfies $alpha_0 / (1 + b n ln phi) < alpha_0$.
background
The module derives running couplings from phi-ladder scaling in Recognition Science. The function runningCoupling is defined by alpha(n) = alpha0 / (1 + b n log phi), where phi is the golden ratio. The lemma phi_gt_onePointFive supplies the bound phi > 1.5 that guarantees log phi > 0. Upstream, the scale definition gives energy levels as powers of phi, and the Coupling abbrev encodes sparse relations in the FEP bridge.
proof idea
The tactic proof first unfolds the runningCoupling definition. It then applies Real.log_pos to phi_gt_onePointFive to obtain log phi >0. Positivity of b n log phi follows by mul_pos on hb, Int.cast_pos.mpr hn, and hlog. The denominator is shown greater than 1 by linarith. Finally div_lt_div_of_pos_left with ha yields the strict inequality, which simp reduces to the goal.
why it matters
This theorem supplies the direction of asymptotic freedom for positive b in the QFT running couplings module. It supports the subsequent gauge coupling unification discussion at GUT scale where couplings meet near 1/24. In the Recognition framework it realizes the phi-forcing chain step T6 for self-similar scaling in the strong sector, consistent with the eight-tick octave and D=3. No downstream uses are recorded yet, leaving open how it composes with the alpha band bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.