Pith. sign in
module module moderate

IndisputableMonolith.Physics.StrongNuclearForceFromRS

show as:
view Lean formalization →

Module defining the Recognition Science prediction for the strong coupling: α_s = 2/17 ≈ 0.1176, with comparison to the PDG value and a certificate packing the match. Physicists citing RS hadronic predictions use the coupling definition and near-PDG lemma. Structure is definitional plus elementary arithmetic identities and a cert record.

claimThe RS strong coupling is $\alpha_s^{\mathrm{RS}} = 2/17 \approx 0.1176$. The module records its equality to that fraction, an approximate decimal, the PDG reference value, a nearness statement $\alpha_s^{\mathrm{RS}} \approx \alpha_s^{\mathrm{PDG}}$, a QCD free-parameter count, and a certificate bundling these facts.

background

Recognition Science fixes dimensionless couplings from the same forcing chain that yields $J$, $\varphi$, the eight-tick period, and $D=3$. The fine-structure constant sits in a narrow band around $1/137$; the strong coupling is treated analogously as a pure rational fixed by ledger structure rather than a free QCD input.

This module lives in the Physics layer and imports only Mathlib and Constants (the RS time quantum $\tau_0 = 1$ tick and related units). It introduces strongCouplingRS as the RS value $2/17$, the PDG reference alphaSPDG, and a small certificate type that packages the numerical agreement for downstream audits.

No dynamical QCD Lagrangian is derived here; the claim is the numerical identification of the coupling at the RS scale with the simple fraction $2/17$.

proof idea

Definition module with thin equational lemmas. strongCouplingRS is introduced as the constant $2/17$; strongCouplingRS_eq and strongCoupling_approx are immediate arithmetic rewrites to the fraction and its decimal. alphaSRS_near_PDG compares that value to the stored PDG figure. qcdParameterCount and StrongForceCert / strongForceCert assemble a record that the RS coupling matches observation within the stated tolerance. No deep tactic proofs; the content is definitions plus rfl-style or norm_num identities.

why it matters in Recognition Science

Closes the strong-force entry in the RS constants table: once $\varphi$ and the rung structure are fixed (T5–T7), $\alpha_s = 2/17$ is the predicted hadronic coupling, parallel to the $\alpha^{-1}\in(137.030,137.039)$ band for QED. Downstream consumers (none linked in the current graph) would cite strongForceCert when auditing that RS has no free QCD coupling parameter. The module does not yet feed a larger forcing-chain theorem; it stands as the Physics-layer anchor for the strong interaction number.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)