log_divergence
plain-language theorem explainer
Establishes that the natural logarithm of any real number exceeding unity is strictly positive. A physicist deriving UV regularization from spacetime discreteness would cite it to confirm that momentum integrals of the form ∫ dk/k diverge as the cutoff Λ grows without bound. The proof is a direct one-line application of the standard positivity lemma for the logarithm.
Claim. For any real number $Λ > 1$, $log Λ > 0$.
background
The QFT.UVCutoff module derives a natural ultraviolet cutoff for quantum field theory from Recognition Science discreteness at the fundamental tick duration τ₀. Upstream definitions supply tau0 as the duration of one tick (with value sqrt(hbar_codata * G_codata / (π c_codata³)) / c_codata in derivation form) and hbar as the reduced Planck constant in RS-native units (φ^{-5} · 1). The module states that spacetime discreteness implies momenta cannot exceed p_max = ℏ/τ₀, which regularizes all UV divergences.
proof idea
The proof is a one-line term wrapper that applies the lemma Real.log_pos directly to the hypothesis hΛ.
why it matters
It supplies the elementary divergence fact needed to motivate the module's claim that a discrete τ₀ scale provides first-principles UV regularization, as outlined in the module's target for the paper on natural UV regularization from information-theoretic discreteness. No downstream theorems are recorded, leaving the result as a foundational step before cutoff insertion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.