Off-diagonal representatives for the R-322 primitive input

Proposition 4.1 freezes its input hypothesis as the literal pointwise bound |G z| ≤ invSqKer z. Since invSqKer 0 = 0, the free Green function and the kernels produced by proper-block collapse do not satisfy that normalized statement at the identity. This is only a representative issue: all uses of those inputs inside a nontrivial primitive integral are insensitive to their value on the singleton {0}.

This file records the bridge explicitly. We zero a kernel at the identity, prove that this preserves the paper's class E, normalize its off-diagonal constant, and establish the null-diagonal facts needed to compare primitive integrals. No estimate or output predicate is assumed here.

Zeroed and normalized representatives

noncomputable def Anderson4D.offDiagonalRepresentative (f : T4 → ℝ) (z : T4) : ℝ

Replace the value of a kernel at the torus identity by zero.

Equations

• Anderson4D.offDiagonalRepresentative f z = if z = 0 then 0 else f z

@[simp]

theorem Anderson4D.offDiagonalRepresentative_zero (f : T4 → ℝ) : offDiagonalRepresentative f 0 = 0

theorem Anderson4D.offDiagonalRepresentative_eq (f : T4 → ℝ) {z : T4} (hz : z ≠ 0) : offDiagonalRepresentative f z = f z

noncomputable def Anderson4D.normalizedOffDiagonalRepresentative (C : ℝ) (f : T4 → ℝ) (z : T4) : ℝ

Scaling which turns an off-diagonal bound |f z| ≤ C * invSqKer z into the normalized Proposition 4.1 bound.

Equations

• Anderson4D.normalizedOffDiagonalRepresentative C f z = C⁻¹ * Anderson4D.offDiagonalRepresentative f z

@[simp]

theorem Anderson4D.normalizedOffDiagonalRepresentative_zero (C : ℝ) (f : T4 → ℝ) : normalizedOffDiagonalRepresentative C f 0 = 0

theorem Anderson4D.offDiagonalRepresentative_memE {f : T4 → ℝ} (hf : MemEClassT4 f) : MemEClassT4 (offDiagonalRepresentative f)

Zeroing at the identity preserves the hyperoctahedral class E.

theorem Anderson4D.normalizedOffDiagonalRepresentative_memE (C : ℝ) {f : T4 → ℝ} (hf : MemEClassT4 f) : MemEClassT4 (normalizedOffDiagonalRepresentative C f)

Constant scaling preserves the hyperoctahedral class E.

theorem Anderson4D.offDiagonalRepresentative_ae_eq (f : T4 → ℝ) : offDiagonalRepresentative f =ᵐ[paperMeasure] f

Zeroing at one point does not change a kernel almost everywhere.

theorem Anderson4D.normalizedOffDiagonalRepresentative_le {C : ℝ} (hC : 0 < C) {f : T4 → ℝ} (hbound : ∀ (z : T4), z ≠ 0 → |f z| ≤ C * invSqKer z) (z : T4) : |normalizedOffDiagonalRepresentative C f z| ≤ invSqKer z

The normalized representative satisfies the literal input bound required by Proposition 4.1.

theorem Anderson4D.normalizedOffDiagonalRepresentative_admissible {n : ℕ} {C : Fin (2 * n - 1) → ℝ} (hC : ∀ (j : Fin (2 * n - 1)), 0 < C j) {G : Fin (2 * n - 1) → T4 → ℝ} (hmem : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (hbound : ∀ (j : Fin (2 * n - 1)) (z : T4), z ≠ 0 → |G j z| ≤ C j * invSqKer z) : IsAdmissiblePrimitiveInput n fun (j : Fin (2 * n - 1)) => normalizedOffDiagonalRepresentative (C j) (G j)

Family form of the preceding construction, matching the exact input type of Proposition 4.1.

Null diagonals in finite paper products

theorem Anderson4D.ae_pi_eval_ne_eval {n : ℕ} (i j : Fin (n + 1)) (hij : i ≠ j) : ∀ᵐ (v : Fin (n + 1) → T4) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure, v i ≠ v j

Distinct coordinates of a finite tuple sampled from the paper product measure are unequal almost surely. This is the precise measure-theoretic fact that permits off-diagonal representatives in primitive chains.

theorem Anderson4D.ae_pi_eval_ne_eval_of_pos {m : ℕ} (hm : 0 < m) (i j : Fin m) (hij : i ≠ j) : ∀ᵐ (v : Fin m → T4) ∂MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure, v i ≠ v j

Cardinality-generic form of ae_pi_eval_ne_eval.

theorem Anderson4D.ae_pi_eval_ne_const {m : ℕ} (i : Fin m) (x : T4) : ∀ᵐ (v : Fin m → T4) ∂MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure, v i ≠ x

A fixed coordinate of a nonempty paper-product tuple avoids any fixed torus point almost surely.

Primitive-chain edge diagonals

theorem Anderson4D.ae_primitiveEdge_sub_ne_zero (n : ℕ) (hn : 2 ≤ n) (z w : T4) (j : Fin (2 * n - 1)) : ∀ᵐ (v : Fin (2 * n - 2) → T4) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure, primitiveAssemble n ⋯ z w v (primitiveEdgeLeft n ⋯ j) - primitiveAssemble n ⋯ z w v (primitiveEdgeRight n ⋯ j) ≠ 0

At order at least two, every edge in an assembled primitive chain is off the diagonal almost surely. Endpoint edges use the nullity of a coordinate hyperplane; internal edges use ae_pi_eval_ne_eval_of_pos.

Congruence of primitive kernels under singleton changes

theorem Anderson4D.primitiveChainProduct_congr_ae_offDiagonal (n : ℕ) (hn : 2 ≤ n) (G G' : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), z ≠ 0 → G j z = G' j z) (z w : T4) : (fun (v : Fin (2 * n - 2) → T4) => primitiveChainProduct n ⋯ G (primitiveAssemble n ⋯ z w v)) =ᵐ[MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure] fun (v : Fin (2 * n - 2) → T4) => primitiveChainProduct n ⋯ G' (primitiveAssemble n ⋯ z w v)

At order at least two, changing every chain input only at the identity does not change the chain product almost everywhere.

theorem Anderson4D.primitiveIntegrand_congr_ae_offDiagonal (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 2 ≤ n) (G G' : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), z ≠ 0 → G j z = G' j z) (κ : PartialPairing (Fin (2 * n))) (z w : T4) : (fun (v : Fin (2 * n - 2) → T4) => primitiveIntegrand ρ ε n ⋯ G κ (primitiveAssemble n ⋯ z w v)) =ᵐ[MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure] fun (v : Fin (2 * n - 2) → T4) => primitiveIntegrand ρ ε n ⋯ G' κ (primitiveAssemble n ⋯ z w v)

The primitive integrand is insensitive almost everywhere to off-diagonal-equivalent chain inputs.

theorem Anderson4D.primitiveKernel_congr_offDiagonal (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 2 ≤ n) (G G' : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), z ≠ 0 → G j z = G' j z) (z w : T4) : primitiveKernel ρ lam ε n ⋯ G z w = primitiveKernel ρ lam ε n ⋯ G' z w

For primitive order at least two, the kernel depends only on the off-diagonal representatives of its input functions.

theorem Anderson4D.primitiveKernel_offDiagonalRepresentative (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : primitiveKernel ρ lam ε n ⋯ G z w = primitiveKernel ρ lam ε n ⋯ (fun (j : Fin (2 * n - 1)) => offDiagonalRepresentative (G j)) z w

In particular, zeroing all chain inputs at the identity leaves every primitive kernel of order at least two unchanged.

Constant scaling of primitive inputs

theorem Anderson4D.primitiveChainProduct_const_mul (n : ℕ) (hn : 1 ≤ n) (C : ℝ) (G : Fin (2 * n - 1) → T4 → ℝ) (x : Fin (2 * n) → T4) : primitiveChainProduct n hn (fun (j : Fin (2 * n - 1)) (z : T4) => C * G j z) x = C ^ (2 * n - 1) * primitiveChainProduct n hn G x

Multiplying every chain input by one constant contributes one copy of that constant for each of the 2n-1 chain edges.

theorem Anderson4D.primitiveIntegrand_const_mul (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (C : ℝ) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : primitiveIntegrand ρ ε n hn (fun (j : Fin (2 * n - 1)) (z : T4) => C * G j z) κ x = C ^ (2 * n - 1) * primitiveIntegrand ρ ε n hn G κ x

Constant scaling at the integrand level.

theorem Anderson4D.primitiveKernel_const_mul (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (C : ℝ) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : primitiveKernel ρ lam ε n hn (fun (j : Fin (2 * n - 1)) (u : T4) => C * G j u) z w = C ^ (2 * n - 1) * primitiveKernel ρ lam ε n hn G z w

Constant scaling at the primitive-kernel level.

theorem Anderson4D.primitiveKernel_eq_pow_mul_normalized (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 2 ≤ n) {C : ℝ} (hC : 0 < C) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : primitiveKernel ρ lam ε n ⋯ G z w = C ^ (2 * n - 1) * primitiveKernel ρ lam ε n ⋯ (fun (j : Fin (2 * n - 1)) => normalizedOffDiagonalRepresentative C (G j)) z w

Exact comparison between an unnormalized input family and its normalized off-diagonal representative. The restriction n ≥ 2 is essential only for the singleton-congruence step.

The free Green input

theorem Anderson4D.greenFn_abs_le_mul_invSqKer {C : ℝ} (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ C / torusDistSq z) (z : T4) (hz : z ≠ 0) : |greenFn z| ≤ C * invSqKer z

The constant from the paper's free Green estimate supplies the exact off-diagonal input bound used by normalization.

theorem Anderson4D.normalizedGreenFn_admissible (n : ℕ) {C : ℝ} (hC : 0 < C) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ C / torusDistSq z) : IsAdmissiblePrimitiveInput n fun (x : Fin (2 * n - 1)) => normalizedOffDiagonalRepresentative C greenFn

A positive constant in the off-diagonal Green estimate produces an admissible family for Proposition 4.1 at every order.

theorem Anderson4D.primitiveKernelDiff_greenFn_le_scaledMajorant (ρ : SmoothCutoff) {orderConstant supportConstant Cprop Cgreen lam ε : ℝ} {n : ℕ} (hn : 2 ≤ n) (hCgreen : 0 < Cgreen) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ Cgreen / torusDistSq z) (hprop41 : Prop41BoundPredicate ρ lam ε n ⋯ (fun (x : Fin (2 * n - 1)) => normalizedOffDiagonalRepresentative Cgreen greenFn) orderConstant supportConstant Cprop) (hreg : PrimitiveEstimateRegime n lam ε orderConstant supportConstant Cprop) (z : T4) : |primitiveKernelDiff ρ lam ε n ⋯ (fun (x : Fin (2 * n - 1)) => greenFn) z| ≤ Cgreen ^ (2 * n - 1) * primitiveKernelMajorant Cprop lam ε supportConstant n z

Proposition 4.1 applied to the normalized Green representative gives a fully explicit bound for the actual free-Green primitive kernel. The factor Cgreen^(2n-1) is the exact cost of undoing the input normalization.

theorem Anderson4D.sum_detJ_primitive_le_scaledMajorant (ρ : SmoothCutoff) {orderConstant supportConstant Cprop Cgreen lam ε : ℝ} {n : ℕ} (hn : 2 ≤ n) (hCgreen : 0 < Cgreen) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ Cgreen / torusDistSq z) (hprop41 : Prop41BoundPredicate ρ lam ε n ⋯ (fun (x : Fin (2 * n - 1)) => normalizedOffDiagonalRepresentative Cgreen greenFn) orderConstant supportConstant Cprop) (hreg : PrimitiveEstimateRegime n lam ε orderConstant supportConstant Cprop) (z : T4) : |∑ σ ∈ primitiveFullPairings n, detJ ρ lam ε n σ z 0| ≤ Cgreen ^ (2 * n - 1) * primitiveKernelMajorant Cprop lam ε supportConstant n z

R-322 terminal-sum form of primitiveKernelDiff_greenFn_le_scaledMajorant.