rsAlphaFactor_gt_100
plain-language theorem explainer
The theorem establishes that the RS-derived factor 44π exceeds 100, a basic positivity check used in certifying the fine structure constant prediction. Physicists working on Recognition Science derivations of α⁻¹ would reference this bound when assembling the FineStructureCert structure. The proof is a one-line wrapper that unfolds the definition of rsAlphaFactor and applies linear arithmetic with the known inequality π > 3.
Claim. The recognition science alpha factor, defined as $44$ times $pi$, satisfies $44pi > 100$.
background
In the Recognition Science framework the fine structure constant inverse is predicted as α⁻¹ = 44π × correction ≈ 137.036, where the 44π factor arises from the gauge loop area in the recognition lattice. The rung equals 44 = gap(3) - 1, consistent with three spatial dimensions from the forcing chain. The rsAlphaFactor is the explicit noncomputable definition 44 * Real.pi that supplies this gauge-loop denominator.
proof idea
The proof unfolds rsAlphaFactor to expose 44 * Real.pi, then applies linarith using the library fact Real.pi_gt_three to conclude the inequality.
why it matters
This bound feeds directly into the fineStructureCert definition, which assembles alpha_rung, factor_pos, and factor_gt_100 to certify the RS prediction α⁻¹ ≈ 137.036. It closes the basic positivity requirement for the 44π gauge loop area inside the alpha band (137.030, 137.039) and supports the T8 forcing of D = 3 through the rung calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.