two_div_17_upper
plain-language theorem explainer
The theorem establishes that the geometric prediction for the strong coupling constant lies strictly below 0.118. Researchers deriving Standard Model parameters from symmetry counts in Recognition Science would cite this bound to close the T15 verification. The proof reduces the claim to a direct numerical comparison via unfolding and constant evaluation.
Claim. The geometric strong coupling constant satisfies $2/17 < 0.118$.
background
In Recognition Science the strong coupling is obtained as the reciprocal of half the symmetry group count, giving α_s = 2/17 ≈ 0.11765. The module T15 formalizes this as the coupling to planar ledger symmetries, distinct from the fine-structure derivation that uses the full edge geometry 4π·11. Upstream structures supply the discrete φ-tiers for nuclear densities and the J-cost calibration on the ledger factorization.
proof idea
The proof is a one-line wrapper that unfolds the geometric definition of the strong coupling and applies numerical normalization to confirm the constant inequality.
why it matters
This bound completes the upper side of the T15 verification that the 2/17 prediction lies inside the PDG interval 0.1179 ± 0.0009. It anchors the framework claim that gauge couplings emerge from symmetry density without adjustable parameters and supports the eight-tick octave and D = 3 landmarks by fixing the strong sector count W = 17.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.