mass_gap_bounds
plain-language theorem explainer
The theorem pins the mass gap parameter Δ to the interval (0.118, 0.119) in RS-native units. Lattice QCD researchers comparing the Yang-Mills gap to Recognition Science predictions would cite this bound when testing the unification. The proof is a one-line wrapper that invokes the prior numerical lemma massGap_numerical_bound.
Claim. $0.118 < Δ < 0.119$, where Δ denotes the mass gap in RS-native units.
background
The module derives 4D Lorentzian spacetime from the J-cost functional and the T0–T8 forcing chain, with spatial metric coefficients fixed by J''(1) = 1 and temporal direction fixed by the 8-tick octave. The mass gap enters via the imported Yang-MillsMassGap structure, where the gap is the lowest excitation energy above the vacuum in the multiplicative recognizer cost. Upstream results supply the J-cost definition (derivedCost on positive ratios) and the ledger factorization that calibrates J on (ℝ₊, ×).
proof idea
One-line wrapper that applies massGap_numerical_bound.
why it matters
The bound supplies a concrete, testable number inside the spacetime emergence certificate (SE-001 to SE-010), linking the J-cost minimization to the Yang-Mills sector. It closes a numerical prediction step in the unification chain that begins from RCL and T5–T8, feeding the claim that the mass gap is forced rather than postulated. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.