large_ratio_suppression
plain-language theorem explainer
For any real x exceeding 100 the factor exp(-x) is strictly less than 1. Cosmologists bounding non-Abelian gauge corrections to the cosmological constant in Recognition Science cite this to show that SU(2) and SU(3) contributions vanish. The proof is a one-line wrapper that invokes the standard exponential inequality for negative arguments and checks the sign via linear arithmetic.
Claim. Let $x$ be a real number satisfying $x > 100$. Then $e^{-x} < 1$.
background
The module shows that non-Abelian gauge corrections to Ω_Λ = 11/16 are exponentially suppressed while the U(1) term α/π survives. In RS-native units the coherence energy is fixed by phi^{-5} with phi the self-similar fixed point; the upstream correction factor for quantum channel capacity at positive integer N is 1/(phi N). The RS units structure U sets tau0 = 1 tick, ell0 = 1 voxel and c = 1. The theorem supplies the elementary bound needed once a mass-to-coherence ratio exceeds 100, as occurs for the SU(2) sector where the ratio reaches order 9×10^{11}.
proof idea
The proof is a one-line wrapper that applies the lemma Real.exp_lt_one_of_neg (exp(y) < 1 for y < 0) and uses linarith to confirm that -x is negative from the hypothesis x > 100.
why it matters
The result closes the argument of Dark_Energy_Mode_Counting.tex §8 Theorem 8.1 that only the massless U(1) correction remains at leading order. It directly supports the framework claim that SU(2) and SU(3) sectors are negligible because their mass gaps produce ratios far above 100, consistent with the eight-tick octave and phi-ladder structure. No open scaffolding is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.