KappaZero

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Vanishing of the annealed coupling matrix of the cutoff law

ABK26, e.annealed.khom.zero: by the adjoint redundancy of the coarse-grained block matrix and the hypercube-symmetry assumption that a_m has the same law as a_m^t, the annealed coupling matrix vanishes on every cube, khom_m(U) = 0.

The two mixed blocks of the deterministic coarse block matrix flip sign under a -> a^t (CoarseGraining's coarseBlockMatrix_lowerLeft_adjointCoeffField_of_exists and coarseBlockMatrix_upperRight_adjointCoeffField_of_exists), and the actual cutoff law is adjoint invariant (Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw_adjoint_invariant), so each mixed annealed entry equals its own negative.

Main results

• coefficientCutoffLaw_annealedBlockMatrix_lowerLeft_eq_zero
• coefficientCutoffLaw_annealedBlockMatrix_upperRight_eq_zero
• coefficientCutoffLaw_annealedSigmaStarInvKappaMean_eq_zero
• coefficientCutoffLaw_annealedKappa_eq_zero

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_annealedBlockMatrix_lowerLeft_eq_zero {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : (HCPolySupport.Book.Ch04.annealedBlockMatrix (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q)).lowerLeft = 0

The lower-left annealed block of the genuine cutoff law vanishes on every triadic cube.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_annealedBlockMatrix_upperRight_eq_zero {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : (HCPolySupport.Book.Ch04.annealedBlockMatrix (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q)).upperRight = 0

The upper-right annealed block of the genuine cutoff law vanishes on every triadic cube.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_annealedSigmaStarInvKappaMean_eq_zero {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.annealedSigmaStarInvKappaMean (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q) = 0

The annealed mixed observable E[sigma_*^{-1}(U; a) kappa(U; a)] of the genuine cutoff law vanishes on every triadic cube.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_annealedKappa_eq_zero {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.annealedKappa (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q) = 0

ABK26, e.annealed.khom.zero. The annealed coupling matrix of the genuine coefficient cutoff vanishes on every triadic cube.