alpha_s_positive
The theorem shows that the Recognition Science prediction for the strong coupling constant is strictly positive. Gauge theorists checking unification or running couplings would cite it to confirm consistency with the observed positive value of α_s(M_Z). The proof is a one-line term wrapper that unfolds the definition and applies div_pos to the positivity of a negative power of phi together with the positivity of pi.
claim$0 < phi^{-3} / pi$
background
In the StrongCoupling module the strong coupling is obtained from the complement of the gauge sum at the recognition scale: 1/α_EM + 1/α_weak + 1/α_s equals cube_edges(D) times pi, with D = 3. The definition alpha_s_prediction is phi to the power -3 divided by pi, using the phi-ladder fixed point from the forcing chain. Upstream results include cube_edges(d) defined as d times 2 to the d-1 and the positivity properties of phi and pi that appear in the LedgerFactorization and PhiForcingDerived structures.
proof idea
The term proof first unfolds alpha_s_prediction to expose phi^{-3} / pi, then applies the lemma div_pos whose two arguments are zpow_pos applied to phi_pos and Real.pi_pos.
why it matters in Recognition Science
The result is used directly by strong_coupling_cert_exists to populate the StrongCouplingCert record and by the running-couplings theorem in Physics.RunningCouplings. It closes the Q9 derivation of α_s from φ-geometry in the module documentation and supplies the positivity needed for the eight-tick gauge structure at D = 3. No open scaffolding remains for this particular positivity claim.
scope and limits
- Does not derive the beta-function or running equation for alpha_s.
- Does not compute numerical values at scales other than the recognition scale.
- Does not incorporate experimental error bars from PDG measurements.
- Does not address higher-order corrections beyond the leading phi-ladder term.
formal statement (Lean)
40theorem alpha_s_positive : 0 < alpha_s_prediction := by
proof body
Term-mode proof.
41 unfold alpha_s_prediction
42 exact div_pos (zpow_pos phi_pos _) Real.pi_pos
43
44/-! ## Structural Constraints
45
46The three gauge couplings at the recognition scale satisfy:
47 1/α_EM + 1/α_weak + 1/α_s = cube_edges(D) × π
48
49This is the RS analog of gauge coupling unification. -/
50