alpha_s_positive
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.