pith. sign in
module module moderate

IndisputableMonolith.Unification.YangMillsMassGap

show as:
view Lean formalization →

The YangMillsMassGap module derives the Yang-Mills mass gap from the Recognition Science J-cost evaluated at the golden ratio. Gauge theorists and mass-gap researchers would cite the algebraic link to the phi-ladder. The module assembles a chain of identities beginning from the phi-inverse relation and J-cost monotonicity.

claimThe Yang-Mills mass gap satisfies $\Delta = J(\phi)$ where $J(x) = (x + x^{-1})/2 - 1$ and $\phi$ obeys $\phi^2 = \phi + 1$, with the equality obtained after substituting the inverse identity $\phi^{-1} = \phi - 1$.

background

The module sits inside the unification layer and imports the RS time quantum $\tau_0 = 1$ tick, the J-cost ledger, spatial dimension forcing to $D=3$, the cube-derived gauge group $SU(3)\times SU(2)\times U(1)$, the three fermion generations, and the self-similar forcing of $\phi$. Upstream DimensionForcing states that $D=3$ is forced by the RS framework; PhiForcing states that $\phi$ is forced by self-similarity in a discrete ledger with J-cost.

The central algebraic tool is the phi-inverse identity $\phi^{-1} = \phi - 1$, which follows directly from the quadratic minimal polynomial. Sibling lemmas then equate the J-cost at $\phi$ to the mass-gap expression and establish positivity and monotonicity on the phi-ladder.

proof idea

The module is a collection of algebraic lemmas. The core step applies the phi-inverse identity to simplify $J(\phi)$ and then invokes J-cost monotonicity and positivity to obtain the mass-gap equality. One-line wrappers handle the final substitutions; no external tactics beyond ring normalization and field simplification are required.

why it matters in Recognition Science

The module supplies the concrete mass-gap realization that is imported by SpacetimeEmergence, which forces the full Lorentzian geometry from J-cost. It realizes the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain inside the gauge sector and closes one link in the mass formula on the phi-ladder.

scope and limits

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (48)