pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.StrongForce

show as:
view Lean formalization →

The module derives the strong coupling α_s = 2/17 as the wallpaper fraction from cubic lattice geometry in Recognition Science. QCD and nuclear physicists cite it to anchor the strong force at the Z scale without free parameters. The module organizes geometric definitions, predictions, and certification theorems that assemble the result from upstream ledger structure.

claimThe strong coupling constant satisfies $α_s = 2/17$ at the Z-boson mass scale, obtained as the wallpaper fraction from the geometry of the cubic lattice in Recognition Science.

background

The module sits in the physics domain and imports the RS time quantum τ₀ = 1 tick together with the alpha derivation from the cubic ledger. That upstream derivation obtains 4π from Gauss-Bonnet vertex deficits on Q₃ and supplies the geometric foundation for all gauge couplings. The central object introduced here is the wallpaper fraction 2/17 that fixes α_s.

proof idea

This is a definition module, no proofs. It collects expressions for experimental, geometric, and predicted values of α_s, defines the equality between the geometric prediction and 2/17, and certifies the match via T15Cert and t15_verified.

why it matters in Recognition Science

The module supplies the fixed α_s = 2/17 imported by the QCD-to-Nuclear Bridge to obtain SEMF coefficients from string tension and by the AlphaRunning module to compute one-loop running from M_Z. It directly addresses the C-014 registry item on determining the strong coupling from RS structure. Downstream documentation states that all theorems are machine-verified with zero sorry and zero axiom.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)