-- QLF_LambShift.lean -- The hydrogen Lamb shift from QLF substrate primitives, scaling as -- α⁵ × m_e c² × log(α⁻²) (Lamb_Shift.md). -- -- The structural argument: -- -- 1. Vacuum hosts ZFA closures at every Markov-blanket depth R from -- R = 1 (one Planck event) to R = R_cosmic. Each closure is a -- vacuum mode at frequency ω = f_vac / R (Frequency_Synchronization.md, -- VacuumEnergy.md §6). -- -- 2. The bound electron at shell-depth R_n = R_1 · n² couples to -- vacuum modes between its own Compton depth R_e (IR cutoff) and -- the shell binding depth R_n (UV cutoff). Both are substrate -- Markov-blanket depths — no external regularization needed. -- -- 3. The substrate Bethe-log range is the depth ratio: -- -- log(R_n / R_e) = log(m_e c² / |E_n|) = log(2 n² / α²) -- -- For n = 1: log(2/α²) ≈ 10.53. -- -- 4. The α⁵ scaling decomposes as: -- α² from Bohr binding (Ry = α²/2 m_e c²) -- α from gauge-twist vertex (emit virtual photon) -- α from gauge-twist vertex (reabsorb) -- α from |ψ(0)|² Bohr-density factor -- Total: α⁵ m_e c². -- -- 5. The 4/(3π n³) prefactor: 1/n³ from |ψ_n(0)|² shell density, -- 4π/π = 4 from solid angle / vertex phase, 1/(3π) = (2/3) × 1/(2π) -- from transverse-polarization × loop phase. -- -- 6. Combined Lamb formula: -- ΔE_Lamb(nS) = (4 α⁵ m_e c²) / (3π n³) × L_eff(n) -- where L_eff(n) = 2 log(1/α) - k(n,0) + small is the effective -- Bethe log, with k(n,0) the QED Bethe constant capturing the -- oscillator-strength weighting on the naive depth-ratio range. -- -- Honest scope. This module Lean-anchors: -- • the substrate Bethe-log range log(R_n/R_e) = log(2 n²/α²) -- • the α⁵ scaling claim (named factor decomposition) -- • the combined Sommerfeld-Bethe formula with L_eff as parameter -- • the ground-state and 2S special-case evaluations using -- substrate α from QLF_FineStructureSubstrate.alpha_QLF -- -- It does NOT Lean-anchor: -- • the substrate derivation of k(n,0) from shell-closure overlap -- counts (Tier-3 open — Lamb_Shift.md §6) -- • the AMM and vacuum-polarization contributions for the 2S₁/₂ -- splitting (separate Tier-3 targets) -- • each of the four α-factors as separate derivation chains -- (current Dirac module similarly records mechanism factors as -- named definitions tied to source docs) -- -- This is the **fifth Lean-anchored fundamental-physics theorem** in -- the QLF tree, after α (QLF_FineStructureSubstrate), m_p/m_e -- (QLF_LenzMassRatio), γ (QLF_EulerMascheroni), and the Dirac -- correction (QLF_DiracCorrection). -- -- Companion to: -- • Lamb_Shift.md — structural argument -- • lamb_shift_demo.py — numerical demo -- • Hydrogen.md §§2-4, §4.1 — Bohr derivation, shell depths -- • Dirac_Correction.md — preceding Bohr-to-Dirac residual -- • Cross_Frequency_Lorentz.md — depth-scaling redshift -- • VacuumEnergy.md §6 — vacuum-alignment principle -- • Magnetism_Spatial_Dynamics.md §6.1 — substrate α single-vertex -- • Per_Qubit_Mass_Quantum.md — per-Compton clock -- • lean/QLF_FineStructureSubstrate.lean — substrate α -- • lean/QLF_LenzMassRatio.lean — substrate m_p/m_e -- • lean/QLF_DiracCorrection.lean — sibling module import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecialFunctions.Pow.Real import QLF_FineStructureSubstrate namespace QLF /-- **Substrate Bethe-log range** for shell `n`: `log(R_n / R_e) = log(2 n² / α²)`. The depth ratio between the bound shell at depth `R_n = R_1 · n²` (with `R_1 = E_Planck / Ry`) and the electron's Compton depth `R_e = E_Planck / (m_e c²)`. Using `Ry = (α²/2) m_e c²`: R_n / R_e = R_1 n² / R_e = n² · m_e c² / Ry = n² · (2 / α²) so `log(R_n/R_e) = log(2 n²) - 2 log α = log(2 n²) + 2 log(1/α)`. For `n = 1`: `log(2/α²) ≈ 10.53`. Both cutoffs are substrate Markov-blanket depths; no external regularization. -/ noncomputable def substrate_bethe_log_range (n : ℕ) : ℝ := Real.log (2 * (n : ℝ)^2 / alpha_QLF^2) /-- **Twice-log-inverse-α factor** appearing in `L_eff`: `2 log(1/α)`. For substrate α = 1/137: `2 log 137 ≈ 9.84`. -/ noncomputable def twice_log_inv_alpha : ℝ := 2 * Real.log (1 / alpha_QLF) /-- **Effective Bethe logarithm** at shell `n`: `L_eff(n) = 2 log(1/α) - k(n,0) + small`. The naive substrate depth-ratio log `2 log(1/α)` is the unweighted range; the Bethe constant `k(n,0)` subtracts off the oscillator- strength-weighting correction. For 2S: `k(2,0) ≈ 2.812`, giving `L_eff(2) ≈ 9.84 - 2.81 ≈ 7.03` (Bethe's published value 7.6859 includes higher-order corrections beyond the leading subtraction). This module takes `k_n_0` as a parameter; substrate derivation of `k(n,0)` from shell-closure overlap weighted sums is Tier-3 open. -/ noncomputable def L_eff (n : ℕ) (k_n_0 : ℝ) : ℝ := twice_log_inv_alpha - k_n_0 /-- **α² factor** from Bohr binding: `Ry = (α²/2) m_e c²`. -/ noncomputable def bohr_alpha_squared : ℝ := alpha_QLF^2 /-- **α factor** from a single gauge-twist vertex (emit or reabsorb a virtual photon — the substrate primitive for Coulomb-via-gauge- twist-exchange mediation, [`Magnetism_Spatial_Dynamics.md`](Magnetism_Spatial_Dynamics.md) §6.1). -/ noncomputable def vertex_alpha : ℝ := alpha_QLF /-- **α factor** from `|ψ(0)|²` Bohr-density at the proton. The Bohr wavefunction at origin scales as `|ψ_n(0)|² = (αm_e)³/(π n³)`, yielding one α after dimensional bookkeeping against `1/m_e²` in the self-energy integral. -/ noncomputable def bohr_density_alpha : ℝ := alpha_QLF /-- **Total α⁵ scaling** from the four named factors: `bohr_alpha_squared × vertex_alpha² × bohr_density_alpha = α⁵`. -/ noncomputable def lamb_alpha_scaling : ℝ := bohr_alpha_squared * vertex_alpha^2 * bohr_density_alpha /-- **The α⁵ identity**: the named factor product equals `α^5`. -/ theorem lamb_alpha_scaling_eq : lamb_alpha_scaling = alpha_QLF^5 := by unfold lamb_alpha_scaling bohr_alpha_squared vertex_alpha bohr_density_alpha ring /-- **Lamb prefactor** at shell `n`: `4 / (3π n³)`. Substrate decomposition (Lamb_Shift.md §5): 1/n³ — shell density |ψ_n(0)|² ∝ 1/n³ 4 — 4π solid angle / π vertex phase-coherence norm 1/(3π) — (2/3) transverse-polarization × 1/(2π) loop phase. -/ noncomputable def lamb_prefactor (n : ℕ) : ℝ := 4 / (3 * Real.pi * (n : ℝ)^3) /-- **The Lamb shift** at shell `n` in units of `m_e c²`, parameterised by the Bethe constant `k(n, 0)`: ΔE_Lamb(nS) / (m_e c²) = (4 / (3π n³)) × α⁵ × (2 log(1/α) - k(n,0)) Combining the prefactor, the α⁵ scaling, and the effective Bethe log. Substrate α from `QLF_FineStructureSubstrate.alpha_QLF`. -/ noncomputable def lamb_shift_over_m_e_c2 (n : ℕ) (k_n_0 : ℝ) : ℝ := lamb_prefactor n * lamb_alpha_scaling * L_eff n k_n_0 /-- **Lamb shift expansion**: explicit form of `lamb_shift_over_m_e_c2`. -/ theorem lamb_shift_expansion (n : ℕ) (k_n_0 : ℝ) : lamb_shift_over_m_e_c2 n k_n_0 = (4 * alpha_QLF^5 / (3 * Real.pi * (n : ℝ)^3)) * (twice_log_inv_alpha - k_n_0) := by unfold lamb_shift_over_m_e_c2 lamb_prefactor L_eff rw [lamb_alpha_scaling_eq] ring /-- **Two-vertex topology + Bohr-density α⁵ scaling**: the structural accounting of the five α factors in `α⁵ m_e c²` Lamb scaling. -/ theorem alpha_five_decomposition : bohr_alpha_squared = alpha_QLF^2 ∧ vertex_alpha = alpha_QLF ∧ bohr_density_alpha = alpha_QLF ∧ bohr_alpha_squared * vertex_alpha * vertex_alpha * bohr_density_alpha = alpha_QLF^5 := by refine ⟨rfl, rfl, rfl, ?_⟩ unfold bohr_alpha_squared vertex_alpha bohr_density_alpha ring /-- **Substrate-α evaluation** of the depth-ratio Bethe log at `n = 1`: `log(R_1/R_e) = log(2 · 137²) = log(37538)`. Numerically `log(37538) ≈ 10.53`. This is the *unweighted* substrate range; the actual Bethe constant `k(1,0) ≈ 2.984` subtracts down to `L_eff(1) ≈ 7.55`. -/ theorem substrate_bethe_log_ground_state : substrate_bethe_log_range 1 = Real.log (2 * (137 : ℝ)^2) := by unfold substrate_bethe_log_range rw [alpha_QLF_eq] congr 1 push_cast ring /-- **Substrate Bethe log at n=2**: `log(R_2/R_e) = log(8 · 137²)`. For 2S₁/₂: naive substrate range ≈ 11.92; actual `L_eff(2) ≈ 7.69` (Bethe 1947) after subtracting `k(2,0) ≈ 2.812`. -/ theorem substrate_bethe_log_n2 : substrate_bethe_log_range 2 = Real.log (8 * (137 : ℝ)^2) := by unfold substrate_bethe_log_range rw [alpha_QLF_eq] congr 1 push_cast ring /-- **Headline conjunction**: the substrate Bethe-log range is Lean-anchored; α⁵ scaling is Lean-anchored; the combined Lamb formula is Lean-anchored. -/ theorem lamb_shift_substrate_summary : substrate_bethe_log_range 1 = Real.log (2 * (137 : ℝ)^2) ∧ substrate_bethe_log_range 2 = Real.log (8 * (137 : ℝ)^2) ∧ lamb_alpha_scaling = alpha_QLF^5 := by exact ⟨substrate_bethe_log_ground_state, substrate_bethe_log_n2, lamb_alpha_scaling_eq⟩ /-- **What this module does NOT prove**. - It does NOT derive the Bethe constant `k(n,0)` from substrate principles. `k(n,0)` enters as a parameter; substrate derivation from shell-closure overlap counts (Lamb_Shift.md §6) is Tier-3 open. - It does NOT derive the AMM correction `+68 MHz` or the vacuum- polarization correction `−27 MHz` that contribute to the 2S₁/₂ − 2P₁/₂ Lamb shift measurement. Those are separate Tier-3 targets (Schwinger g-2 substrate, Uehling pair-production substrate). - It does NOT derive the explicit `1/(2π)` loop-phase factor in the prefactor `1/(3π)`; the substrate-angular-counting in `Magnetism_Spatial_Dynamics.md` §6.1.3 must be extended to two- vertex topologies to close this. - It does NOT close the substrate-α 0.026% gap. The Lamb shift inherits `5 × 0.026% ≈ 0.13%` from α⁵ scaling. -/ theorem lamb_shift_not_proved_here : True := trivial end QLF