CubeScalar

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

Scalarity of the annealed diagonal blocks on cubes

ABK26: the hypercube symmetry assumption also implies, in the case that U = cu is a cube, that each of the diagonal blocks of bfAhom_m(cu) is a scalar matrix.

The mechanism is CoarseGraining's Chapter 4 scalarization route (Ch04.Internal.annealedPrimitiveScalarizationData_of_isotropic_adjoint), which needs only a law carrier, signed-permutation isotropy in law, and adjoint invariance in law. All three are already proved for the genuine cutoff law, so no structural-law (in particular no unit-range) hypothesis is used here.

Main results

• coefficientCutoffLaw_isScalarMatrix_annealedBAtScale
• coefficientCutoffLaw_isScalarMatrix_annealedSigmaStarInvAtScale
• coefficientCutoffLaw_isScalarMatrix_annealedSigmaAtScale
• coefficientCutoffLaw_exists_annealedBlockMatrixAtScale_eq_blockDiag_smul_one

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_isScalarMatrix_annealedBAtScale {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) : HCPolySupport.IsScalarMatrix (HCPolySupport.Book.Ch04.annealedBAtScale (Cutoff.coefficientCutoffLaw M m) n)

ABK26. The annealed upper-left block of the genuine cutoff on an origin cube is a scalar matrix.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_isScalarMatrix_annealedSigmaStarInvAtScale {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) : HCPolySupport.IsScalarMatrix (HCPolySupport.Book.Ch04.annealedSigmaStarInvAtScale (Cutoff.coefficientCutoffLaw M m) n)

ABK26. The annealed inverse-star block of the genuine cutoff on an origin cube is a scalar matrix.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_isScalarMatrix_annealedSigmaAtScale {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) : HCPolySupport.IsScalarMatrix (HCPolySupport.Book.Ch04.annealedSigmaAtScale (Cutoff.coefficientCutoffLaw M m) n)

The annealed conductivity of the genuine cutoff on an origin cube is a scalar matrix.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_exists_annealedBlockMatrixAtScale_eq_blockDiag_smul_one {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) : ∃ (s : ℝ) (t : ℝ), HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) n = HCPolySupport.Book.Ch02.blockDiag (s • 1) (t • 1)

ABK26 combined. On an origin cube the annealed cutoff block matrix is block diagonal with scalar diagonal blocks.