Pith. sign in
theorem

massGap_pos

proved
show as:
module
IndisputableMonolith.Unification.YangMillsMassGap
domain
Unification
line
120 · github
papers citing
1 paper (below)

plain-language theorem explainer

Recognition Science derives a strictly positive mass gap Δ = J(φ) = (√5 - 2)/2 from the J-cost functional on the phi-ladder. Researchers addressing the Yang-Mills mass gap Millennium problem in this framework would cite the result for the exact spectral gap value. The proof is a one-line term wrapper that unfolds the massGap definition and applies linear arithmetic to the auxiliary bound √5 > 2.

Claim. $0 < (√5 - 2)/2$

background

The J-cost functional is J(x) = ½(x + x⁻¹) - 1. On the phi-ladder lattice forced by T5 and T6, its value at the golden ratio φ yields the mass gap constant massGap := (√5 - 2)/2, which equals J(φ). The module derives this as the minimum cost of any non-vacuum excitation for the SU(2), SU(3), and U(1) sectors on Q₃, with no free parameters. Upstream results supply the massGap definition itself and the lemma sqrt5_gt_two establishing 2 < √5 by direct comparison to √4 = 2.

proof idea

The proof is a term-mode one-liner. It unfolds massGap to the explicit expression (√5 - 2)/2, then invokes linarith on the inequality supplied by the upstream lemma sqrt5_gt_two.

why it matters

This theorem supplies the positivity step that feeds minimum_rest_mass_is_gap and spacetime_emergence_cert in the unification layer. It completes the terminal segment of the forcing chain (RCL → T5 J-uniqueness → T6 phi → T8 D = 3 → GaugeFromCube) by showing the gap Δ = J(φ) is strictly positive and exact. The module documentation positions the result as the RS resolution of the Yang-Mills mass gap problem, with the gap being universal across gauge sectors and falsifiable by any sub-gap phi-ladder excitation.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 1 of 1)