log_le_linear
plain-language theorem explainer
For any slope δ > 0 and any x ≥ 1, log x is bounded above by the affine function δx − 1 − log δ. Shell-entropy estimates in the Gaussian-UV path-sum argument cite it to turn n log n = o(n²) into an explicit threshold. The proof is a short rearrangement of the classical inequality log y ≤ y − 1 at y = δx.
Claim. For every $\delta > 0$ and every real $x \geq 1$, $\log x \leq \delta\, x + (-1 - \log \delta)$.
background
The ambient module builds exact (cap-free) complexity shells for the quotient-class path-sum configuration space and inserts a hand-chosen Gaussian UV factor $\exp(-\rho n^2)$ so the shell series converges for every $\rho > 0$. Shell cardinality is bounded by $(n+1)^{12(n+1)}$, so the entropy exponent is of order $n\log n$. Comparing that to the quadratic Gaussian exponent needs a quantitative linear upper bound on the logarithm.
The classical comparison $\log y \leq y - 1$ for $y > 0$ is the only analytic input. Scaling the argument to $y = \delta x$ produces an arbitrary positive slope $\delta$ at the price of an additive constant $-1 - \log\delta$. No Recognition-Science cost functional or ledger identity is used here; the lemma is pure real analysis serving the Stage-2 summability argument.
proof idea
From $x \geq 1$ deduce $x > 0$. Positivity of $\delta$ and $x$ gives $\delta x > 0$, so Real.log_le_sub_one_of_pos yields $\log(\delta x) \leq \delta x - 1$. Multiplicativity expands the left side as $\log\delta + \log x$. A single linarith rearranges to the claimed affine bound.
why it matters
Immediate consumer is exists_gaussian_domination: for every $\rho > 0$ there is a threshold $N$ past which the entropy exponent $12(n+1)\log(n+1)$ is at most half the Gaussian exponent $\rho n^2$. That domination closes the modulus bound on regulated shell terms and feeds summability of the UV-regularized shell series and convergence of cutoff partial sums to $Z_{\mathrm{RS,uv}}$.
In the Seven Gaps honesty protocol this is Stage-2 mathematics only. The Gaussian factor is an inserted regulator, not derived physics; regulator removal ($\rho\to 0^+$) remains a named open (HasZRSRegulatorRemoval). The lemma does not touch continuum-limit flags or the FullTheoryLedger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.