log_divergence
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of any cutoff momentum or energy scale.
- Does not address convergence after a cutoff is imposed.
- Does not incorporate the phi-ladder, J-uniqueness, or eight-tick octave from the forcing chain.
- Does not depend on specific constants such as l0 or E0 beyond the module context.
formal statement (Lean)
50theorem log_divergence (Λ : ℝ) (hΛ : Λ > 1) :
51 Real.log Λ > 0 := Real.log_pos hΛ
proof body
Term-mode proof.
52
53/-! ## The τ₀ Discreteness Scale -/
54
55/-- The fundamental length scale l0 = c * tau0.
56 tau0 ~ 1.288e-27 s gives l0 ~ 3.86e-19 m.
57 This also determines:
58 - Energy scale: E0 = hbar / tau0 ~ 5.1e-8 J ~ 3.2e11 GeV
59 - Momentum scale: p0 = hbar / l0 ~ 1.7e-10 kg*m/s -/