two_div_17_lower
plain-language theorem explainer
The theorem establishes the strict inequality 0.117 < 2/17 for the geometric strong coupling in the reals. Physicists verifying symmetry-derived constants in Recognition Science cite this to anchor the lower edge of the T15 prediction. The proof is a one-line term wrapper that reduces via the alpha_s_geom definition then applies numerical normalization.
Claim. $0.117 < 2/17$ where $2/17$ is the geometric strong coupling constant derived from the symmetry count $W=17$.
background
The StrongForce module derives the strong coupling from planar symmetries of the ledger, setting alpha_s = 2/W with W=17. The definition alpha_s_geom fixes this value as the rational 2/17, labeled the Wallpaper Fraction and Predicted Strong Coupling. The module states the hypothesis that the strong force couples to pairs of symmetries, yielding the approximation 0.11765 that lies within 0.2 sigma of the PDG 2022 measurement 0.1179 plus or minus 0.0009.
proof idea
The term proof first simplifies the target using the definition of alpha_s_geom, then invokes norm_num to discharge the concrete numerical comparison between the decimal 0.117 and the rational 2/17.
why it matters
This lower bound supports the T15 verification of the strong force by confirming the geometric prediction exceeds 0.117. It feeds the module's claim that the 2/17 value matches observation to within 0.0003 and sits inside the Recognition Science program that extracts constants from the forcing chain and the eight-tick octave. The module records the result as part of the now-proven T15 theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.