Pointwise chain-weight bridge for the single-scale proof

The local estimates use the kernels lambda and strongLambda, while the frozen Proposition 5.10 statement uses latticeEdgeWeight x y = (1 + ‖x-y‖²)⁻¹. This file records the pointwise comparisons needed by the final finite-Fubini assembly.

For an unskipped edge, separation at the LCA scale activates the local cutoff and the statement weight is bounded by the inverse-square kernel. For a skipped edge, multiplying the local value R⁻² by R² recovers the omitted statement factor exactly.

theorem Anderson4D.XYCluster.latticeEdgeWeight_le_norm_inv_sq (x y : Fin 4 → ℤ) (hxy : 0 < znorm (x - y)) : latticeEdgeWeight x y ≤ (znorm (x - y))⁻¹ ^ 2

The bracketed lattice weight is no larger than the homogeneous inverse-square weight away from the diagonal.

theorem Anderson4D.XYCluster.latticeEdgeWeight_le_nxClassLambda_unskipped {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {l r : HeppLeaf t} (hlr : l ≠ r) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (hra : singleScaleSigma1 Nm mu r = a) : latticeEdgeWeight (z l) (z r) ≤ (nxClassCluster ht hroot Nm mu z hz a ha).lambda R false (z l) (z r)

An unskipped edge entering a leaf in the active (N,X) class a is bounded by that class's lambda kernel.

theorem Anderson4D.XYCluster.latticeEdgeWeight_le_nxClassStrongLambda_unskipped {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {l r : HeppLeaf t} (hlr : l ≠ r) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (hla : singleScaleSigma1 Nm mu l = a) (hrb : singleScaleSigma1 Nm mu r = b) : latticeEdgeWeight (z l) (z r) ≤ (nxClassCluster ht hroot Nm mu z hz a ha).strongLambda (nxClassCluster ht hroot Nm mu z hz b hb) R false (z l) (z r)

The stronger cutoff on the second edge is also activated by LCA separation when its two endpoint classes are fixed.

theorem Anderson4D.XYCluster.sq_mul_lambda_skipped (c : XYCluster) (R : ℝ) (hR : R ≠ 0) (u x : Fin 4 → ℤ) : R ^ 2 * c.lambda R true u x = 1

A skipped local edge contributes exactly R⁻², hence its omitted statement factor is recovered by the global R² budget.

theorem Anderson4D.XYCluster.sq_mul_strongLambda_skipped (a b : XYCluster) (R : ℝ) (hR : R ≠ 0) (x y : Fin 4 → ℤ) : R ^ 2 * a.strongLambda b R true x y = 1

Strong-kernel version of sq_mul_lambda_skipped.

Uniform pointwise and product interfaces

noncomputable def Anderson4D.XYCluster.edgeStatementFactor (skipped : Bool) (x y : Fin 4 → ℤ) : ℝ

The factor printed in the skipped-chain product at one edge.

Equations

• Anderson4D.XYCluster.edgeStatementFactor skipped x y = if skipped = true then 1 else Anderson4D.latticeEdgeWeight x y

theorem Anderson4D.XYCluster.edgeStatementFactor_nonneg (skipped : Bool) (x y : Fin 4 → ℤ) : 0 ≤ edgeStatementFactor skipped x y

theorem Anderson4D.XYCluster.edgeStatementFactor_le_scaled_nxClassLambda {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (hR : R ≠ 0) {l r : HeppLeaf t} (skipped : Bool) (hlr : skipped = false → l ≠ r) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (hra : singleScaleSigma1 Nm mu r = a) : edgeStatementFactor skipped (z l) (z r) ≤ (if skipped = true then R ^ 2 else 1) * (nxClassCluster ht hroot Nm mu z hz a ha).lambda R skipped (z l) (z r)

Pointwise statement-to-lambda comparison, including the exact R² charge on a skipped edge.

theorem Anderson4D.XYCluster.edgeStatementFactor_le_scaled_nxClassStrongLambda {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (hR : R ≠ 0) {l r : HeppLeaf t} (skipped : Bool) (hlr : skipped = false → l ≠ r) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (hla : singleScaleSigma1 Nm mu l = a) (hrb : singleScaleSigma1 Nm mu r = b) : edgeStatementFactor skipped (z l) (z r) ≤ (if skipped = true then R ^ 2 else 1) * (nxClassCluster ht hroot Nm mu z hz a ha).strongLambda (nxClassCluster ht hroot Nm mu z hz b hb) R skipped (z l) (z r)

Pointwise statement-to-strongLambda comparison for the second edge of a paired elimination block.

theorem Anderson4D.XYCluster.heppChainWeightExcept_le_R_pow_mul_kernelProduct {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (O : Finset (AdjacentIndex m)) (w : Fin m → HeppLeaf t) (R : ℝ) (K : AdjacentIndex m → ℝ) (hlocal : ∀ (j : AdjacentIndex m), edgeStatementFactor (decide (j ∈ O)) (z (w ↑j)) (z (w (adjacentSucc j))) ≤ (if j ∈ O then R ^ 2 else 1) * K j) : heppChainWeightExcept z O w ≤ R ^ (2 * O.card) * ∏ j : AdjacentIndex m, K j

Generic finite-product reinsertion of the skipped-edge budget. This is the algebraic statement behind the factor R^(2s) in (5.87), independent of the later choice of one- and two-variable elimination blocks.

A concrete kernel product attached to an (N,X) word

noncomputable def Anderson4D.XYCluster.nxClassEdgeKernel {t : PlaneTree} {m : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (O strongEdges : Finset (AdjacentIndex m)) (cls : Fin m → ActiveNXClass Nm mu) (w : Fin m → HeppLeaf t) (j : AdjacentIndex m) : ℝ

At every adjacency, use the target class's one-variable kernel, except on the selected set strongEdges, where the two-class cutoff of (5.91) is used. This definition is pointwise in a leaf word; the later Fubini step turns its product into nested conditioned copy sums.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.XYCluster.nxClassEdgeKernel_nonneg {t : PlaneTree} {m : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (O strongEdges : Finset (AdjacentIndex m)) (cls : Fin m → ActiveNXClass Nm mu) (w : Fin m → HeppLeaf t) (j : AdjacentIndex m) : 0 ≤ nxClassEdgeKernel ht hroot Nm mu z hz R O strongEdges cls w j

theorem Anderson4D.XYCluster.heppChainWeightExcept_le_nxClassEdgeKernelProduct {t : PlaneTree} {m : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (hR : R ≠ 0) (O strongEdges : Finset (AdjacentIndex m)) (cls : Fin m → ActiveNXClass Nm mu) (w : Fin m → HeppLeaf t) (hcls : ∀ (i : Fin m), singleScaleSigma1 Nm mu (w i) = ↑(cls i)) (hno : NoAdjacentOutside O w) : heppChainWeightExcept z O w ≤ R ^ (2 * O.card) * ∏ j : AdjacentIndex m, nxClassEdgeKernel ht hroot Nm mu z hz R O strongEdges cls w j

Concrete statement-boundary comparison for a fixed leaf word and its induced active (N,X) word. Equal adjacent leaves are needed only off O, exactly as in the frozen proposition.