Pith. sign in
module module moderate

IndisputableMonolith.Constants.StrongCoupling

show as:
view Lean formalization →

The StrongCoupling module supplies RS-native predictions and certificates for the strong coupling constant alpha_s together with gauge sum bounds. Researchers deriving particle-physics constants from first principles would cite it to obtain the strong-sector complement to the electromagnetic alpha. The module consists of sibling definitions and existence statements built on the imported alpha derivation.

claimThe module establishes the prediction for the strong fine-structure constant $\alpha_s$ and the gauge-sum value with explicit bounds, all derived from the cubic-ledger geometry.

background

The module sits inside the Recognition Science constants domain. It imports the base Constants module, whose sole documented content is the definition of the fundamental RS time quantum $\tau_0 = 1$ tick, and the AlphaDerivation module, whose main result is the structural derivation of $4\pi$ from the Gauss-Bonnet theorem applied to vertex deficits of the cubic lattice $Q_3$.

No additional notation or J-cost definitions are introduced locally; the module simply extends the ledger geometry already used for $\alpha^{-1}$ into the strong-coupling sector via the listed sibling objects.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module completes the gauge-sector constants by supplying the strong-coupling piece that sits beside the electromagnetic alpha already obtained in AlphaDerivation. It thereby supports any later derivation that requires the full set of gauge couplings inside the Recognition framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)