Orientation identities for single-scale kernels

The anchored elimination order traverses one side of the original word in reverse. This file isolates the purely analytic facts which make that change of orientation harmless. The stronger two-class cutoff is symmetric, and it can always be relaxed to the one-class cutoff at either endpoint.

theorem Anderson4D.XYCluster.lambda_comm (c : XYCluster) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : c.lambda R skipped x y = c.lambda R skipped y x

A one-class kernel is symmetric in its two lattice points.

theorem Anderson4D.XYCluster.strongLambda_comm (a b : XYCluster) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : a.strongLambda b R skipped x y = b.strongLambda a R skipped y x

The two-class kernel is unchanged when both endpoint data are swapped.

theorem Anderson4D.XYCluster.strongLambda_le_leftLambda (a b : XYCluster) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : a.strongLambda b R skipped x y ≤ a.lambda R skipped x y

Forgetting the right endpoint scale weakens the strong cutoff.

theorem Anderson4D.XYCluster.strongLambda_le_rightLambda (a b : XYCluster) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : a.strongLambda b R skipped x y ≤ b.lambda R skipped x y

Forgetting the left endpoint scale weakens the strong cutoff.

theorem Anderson4D.XYCluster.strongLambda_le_rightLambda_rev (a b : XYCluster) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : a.strongLambda b R skipped x y ≤ b.lambda R skipped y x

Right-endpoint relaxation in the reversed point orientation.

Active (N,X) class specializations

theorem Anderson4D.XYCluster.nxClassStrongLambda_comm {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) (a b : ActiveNXClass Nm mu) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : (nxClassCluster ht hroot Nm mu z hz ↑a ⋯).strongLambda (nxClassCluster ht hroot Nm mu z hz ↑b ⋯) R skipped x y = (nxClassCluster ht hroot Nm mu z hz ↑b ⋯).strongLambda (nxClassCluster ht hroot Nm mu z hz ↑a ⋯) R skipped y x

strongLambda_comm specialized to the clusters of two active classes.

theorem Anderson4D.XYCluster.nxClassStrongLambda_le_leftLambda {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) (a b : ActiveNXClass Nm mu) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : (nxClassCluster ht hroot Nm mu z hz ↑a ⋯).strongLambda (nxClassCluster ht hroot Nm mu z hz ↑b ⋯) R skipped x y ≤ (nxClassCluster ht hroot Nm mu z hz ↑a ⋯).lambda R skipped x y

Left-class relaxation for two active (N,X) classes.

theorem Anderson4D.XYCluster.nxClassStrongLambda_le_rightLambda {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) (a b : ActiveNXClass Nm mu) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : (nxClassCluster ht hroot Nm mu z hz ↑a ⋯).strongLambda (nxClassCluster ht hroot Nm mu z hz ↑b ⋯) R skipped x y ≤ (nxClassCluster ht hroot Nm mu z hz ↑b ⋯).lambda R skipped x y

Right-class relaxation for two active (N,X) classes.

theorem Anderson4D.XYCluster.nxClassStrongLambda_le_rightLambda_rev {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) (a b : ActiveNXClass Nm mu) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : (nxClassCluster ht hroot Nm mu z hz ↑a ⋯).strongLambda (nxClassCluster ht hroot Nm mu z hz ↑b ⋯) R skipped x y ≤ (nxClassCluster ht hroot Nm mu z hz ↑b ⋯).lambda R skipped y x

Reversed-point right-class relaxation for active (N,X) classes.