rsAlphaFactor_pos
plain-language theorem explainer
The theorem establishes that the RS alpha factor, defined as 44 times pi, is strictly positive. Physicists assembling Recognition Science predictions for the fine structure constant cite this to certify the leading gauge-loop term before constructing the full alpha certificate. The proof is a one-line wrapper that unfolds the definition and invokes the positivity tactic.
Claim. The RS alpha factor satisfies $0 < 44 pi$, where the factor is the gauge-loop area contribution on the recognition lattice with rung 44 equal to gap(3) minus one.
background
The module derives the fine structure constant from the recognition lattice, with the leading term 44 pi arising as the gauge-loop area. The definition rsAlphaFactor sets this term to 44 times pi in real numbers. The module states that the rung equals gap(3) minus one and that 44 pi is positive, forming one of the structural facts needed for the alpha prediction near 137.036.
proof idea
The proof is a one-line wrapper. It unfolds rsAlphaFactor to expose the expression 44 times Real.pi and then applies the positivity tactic to obtain the strict inequality.
why it matters
This theorem supplies the factor_pos field required by the fineStructureCert definition, which packages the full RS alpha certification. It closes the trivial positivity check listed in the module for the 44 pi term. In the framework it supports the alpha band claim that the inverse lies inside (137.030, 137.039) by confirming the base factor is positive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.