R324PermCross: a uniform positive floor for the Green's function

Off the single junk point z = 0, the heat-integral Green's function of 1 - Δ on 𝕋⁴ is bounded below by the explicit positive constant g₀ = e⁻² (8π)⁻² e^{-π²}: the defining time integral is genuinely convergent there, and already the t ∈ (1,2] window of the k = 0 Gaussian summand carries this much mass.

This floor is the geometric input of the R324PermCross nonexistence theorem: every physical pure-cross pairing integral is bounded below by a fixed exponential c^m, so the m!-member bijection fibre defeats any K^m |log ε|^{m-1} budget at a fixed admissible scale.

Main results:

• r324PermCross_integrableOn_greenIntegrand — for z ≠ 0 the integrand t ↦ e^{-t} Θ(t,z) is integrable on (0,∞);
• r324PermCross_greenFn_floor — g₀ ≤ greenFn z for every z ≠ 0.

Geometry of the canonical lift

theorem Anderson4D.r324PermCross_torusDistSq_le (z : T4) : torusDistSq z ≤ 4 * Real.pi ^ 2

The canonical lift has squared length at most 4π².

theorem Anderson4D.r324PermCross_eq_zero_of_torusDistSq {z : T4} (h : torusDistSq z = 0) : z = 0

Vanishing lifted distance forces the origin: torusDistSq only vanishes at z = 0.

theorem Anderson4D.r324PermCross_torusDistSq_pos {z : T4} (hz : z ≠ 0) : 0 < torusDistSq z

Positive lifted distance off the origin.

theorem Anderson4D.r324PermCross_coord_sq {a : ℝ} (ha : |a| ≤ Real.pi) (m : ℤ) : a ^ 2 / 2 + Real.pi ^ 2 / 2 * ↑m ^ 2 ≤ (a + 2 * Real.pi * ↑m) ^ 2

Componentwise lattice bound: for |a| ≤ π and m ∈ ℤ, (a + 2πm)² ≥ a²/2 + (π²/2) m².

theorem Anderson4D.r324PermCross_latticeDistSq_ge (z : T4) (k : Z4) : torusDistSq z / 2 + Real.pi ^ 2 / 2 * ∑ i : Fin dim, ↑(k i) ^ 2 ≤ latticeDistSq z k

The lattice-point distance dominates half the lifted distance plus a Gaussian lattice weight.

Gaussian lattice sums

theorem Anderson4D.r324PermCross_summable_exp_int {c : ℝ} (hc : 0 < c) : Summable fun (m : ℤ) => Real.exp (-c * ↑m ^ 2)

Summability of the one-dimensional Gaussian lattice sum.

theorem Anderson4D.r324PermCross_tsum_exp_int_le {c : ℝ} (hc : 0 < c) : ∑' (m : ℤ), Real.exp (-c * ↑m ^ 2) ≤ 2 * (1 - Real.exp (-c))⁻¹

One-dimensional Gaussian tail: ∑_{m ∈ ℤ} e^{-c m²} ≤ 2 (1 - e^{-c})⁻¹.

theorem Anderson4D.r324PermCross_summable_tsum_pi_prod {g : ℤ → ℝ} (h0 : ∀ (m : ℤ), 0 ≤ g m) (hg : Summable g) (n : ℕ) : (Summable fun (k : Fin n → ℤ) => ∏ i : Fin n, g (k i)) ∧ ∑' (k : Fin n → ℤ), ∏ i : Fin n, g (k i) = (∑' (m : ℤ), g m) ^ n

Nonnegative product-form lattice sums over Fin n → ℤ factor into powers of the one-dimensional sum.

theorem Anderson4D.r324PermCross_tsum_gaussZ4 {c : ℝ} (hc : 0 < c) : (Summable fun (k : Z4) => Real.exp (-c * ∑ i : Fin dim, ↑(k i) ^ 2)) ∧ ∑' (k : Z4), Real.exp (-c * ∑ i : Fin dim, ↑(k i) ^ 2) = (∑' (m : ℤ), Real.exp (-c * ↑m ^ 2)) ^ dim

The ℤ⁴ Gaussian lattice sum is the fourth power of the one-dimensional one.

The two heat-kernel majorants

theorem Anderson4D.r324PermCross_heat_coeff (t : ℝ) : (4 * Real.pi * t) ^ (-2) = (16 * Real.pi ^ 2)⁻¹ * (t ^ 2)⁻¹

The heat normalization as an honest inverse square.

theorem Anderson4D.r324PermCross_heat_coeff_nonneg (t : ℝ) : 0 ≤ (4 * Real.pi * t) ^ (-2)

Nonnegativity of the heat normalization.

noncomputable def Anderson4D.r324PermCrossGaussConst : ℝ

The ℤ⁴ Gaussian constant of the small-time majorant.

Equations

• Anderson4D.r324PermCrossGaussConst = ∑' (k : Anderson4D.Z4), Real.exp (-(Real.pi ^ 2 / 8) * ∑ i : Fin Anderson4D.dim, ↑(k i) ^ 2)

theorem Anderson4D.r324PermCrossGaussConst_nonneg : 0 ≤ r324PermCrossGaussConst

theorem Anderson4D.r324PermCross_heat_small {z : T4} {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) : Real.exp (-t) * heatKernelT4 t z ≤ (16 * Real.pi ^ 2)⁻¹ * r324PermCrossGaussConst * ((t ^ 2)⁻¹ * Real.exp (-(torusDistSq z / 8 / t)))

Small-time bound: for 0 < t ≤ 1, e^{-t} Θ(t,z) ≤ (16π²)⁻¹ C_Z · t⁻² e^{-(d/8)/t}.

noncomputable def Anderson4D.r324PermCrossLargeConst : ℝ

The constant of the large-time majorant.

Equations

• Anderson4D.r324PermCrossLargeConst = (16 * Real.pi ^ 2)⁻¹ * (16 * Real.exp (Real.pi ^ 2 / 8) / Real.pi ^ 2) ^ Anderson4D.dim * 16

theorem Anderson4D.r324PermCross_heat_large (z : T4) {t : ℝ} (ht : 1 ≤ t) : Real.exp (-t) * heatKernelT4 t z ≤ r324PermCrossLargeConst * Real.exp (-(t / 2))

Large-time bound: for 1 ≤ t, e^{-t} Θ(t,z) ≤ C_L e^{-t/2}.

Integrability and the floor

theorem Anderson4D.r324PermCross_integrableOn_greenIntegrand {z : T4} (hz : z ≠ 0) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-t) * heatKernelT4 t z) (Set.Ioi 0) MeasureTheory.volume

Off the origin, the Green time integrand is integrable on (0,∞).

noncomputable def Anderson4D.r324PermCrossGreenFloorConst : ℝ

The explicit uniform floor constant e⁻² (64π²)⁻¹ e^{-π²}.

Equations

• Anderson4D.r324PermCrossGreenFloorConst = Real.exp (-2) * ((64 * Real.pi ^ 2)⁻¹ * Real.exp (-Real.pi ^ 2))

theorem Anderson4D.r324PermCrossGreenFloorConst_pos : 0 < r324PermCrossGreenFloorConst

theorem Anderson4D.r324PermCross_greenFn_floor {z : T4} (hz : z ≠ 0) : r324PermCrossGreenFloorConst ≤ greenFn z

The Green's function floor: off the origin, greenFn z ≥ e⁻² (64π²)⁻¹ e^{-π²} > 0.