massive_suppression
plain-language theorem explainer
In the Recognition Science cosmology model, any gauge sector with positive boson mass M and coherence energy E > 0 yields a vacuum correction strictly smaller than its coupling divided by π. Researchers modeling the leading dark-energy correction from the U(1) sector alone cite this to establish that non-Abelian contributions are negligible. The proof is a short tactic sequence that unfolds the exponential definition, establishes the strict exponential inequality via Real.exp_lt_one_of_neg, and reduces the comparison by multiplication with a 0-
Claim. Let $s$ be a gauge sector with coupling constant $a > 0$ and boson mass $M > 0$, and let $E > 0$ be an energy scale. Then the vacuum correction $a/π · exp(-M/E)$ satisfies $a/π · exp(-M/E) < a/π$.
background
The GaugeSector structure encodes a gauge factor of Aut(Q₃) together with its coupling constant α, boson mass M, and the positivity hypotheses 0 < α and 0 ≤ M. The vacuumCorrection function is defined by the expression α/π · exp(-M/E) for a given energy scale E. In the module setting, non-Abelian gauge corrections to Ω_Λ = 11/16 are exponentially suppressed relative to the massless U(1) photon contribution at zero momentum. This lemma supplies the strict inequality required for the SU(2) and SU(3) sectors whose bosons carry positive mass or are confined.
proof idea
The proof unfolds the definition of vacuumCorrection. It first establishes exp(-M/E) < 1 by applying Real.exp_lt_one_of_neg to the negative argument -M/E. Positivity of α/π follows directly from the coupling positivity hypothesis via div_pos. The comparison is then obtained by multiplying the exponential inequality on the left by the positive quantity α/π and invoking the arithmetic identity x · 1 = x.
why it matters
This theorem is invoked by u1_dominates to establish that the SU(2) correction is smaller than the U(1) correction and by the certificate nonAbelianSuppressionCert. It fills the exponential-suppression step in the paper's Theorem 8.1 on non-Abelian gauge corrections. Within the Recognition framework it supports the claim that only the massless U(1) sector contributes at leading order to Ω_Λ, consistent with the eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.