Positive definiteness of 2I - Adj(Δ)

Proof of Proposition 4.1, Step 2 (periodic-mesh-calculations.tex): "For M = 2I - Adj(Δ), direct expansion gives, for any real vector z, zᵀMz = ∑_{{i,j}} n_i n_j (z_i/n_i - z_j/n_j)² + ∑_i ((Mn)_i/n_i) z_i². Thus M is positive definite."

qform G z = ∑_i 2 z_i² - ∑_i ∑_{j ∼ i} z_i z_j is zᵀ M z. If n > 0 and Mn > 0 componentwise, then qform G z > 0 for z ≠ 0 (qform_pos). For a vector z ≥ 0 supported on a configuration of edges, qform is bounded above by the same expression over the configuration (qform_le_of_pattern); this is how the forbidden subtrees are excluded.

def MultiplicativeBasisDeformations.qform {D : Type v} [Fintype D] (G : SimpleGraph D) [DecidableRel G.Adj] (z : D → ℚ) : ℚ

The quadratic form zᵀ (2I - A) z.

theorem MultiplicativeBasisDeformations.sum_neighbors_swap {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (f : D → D → ℚ) : ∑ i : D, ∑ j ∈ G.neighborFinset i, f i j = ∑ i : D, ∑ j ∈ G.neighborFinset i, f j i

theorem MultiplicativeBasisDeformations.qform_pos {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] (n : D → ℚ) (hn : ∀ (i : D), 0 < n i) (hMn : ∀ (i : D), 0 < 2 * n i - ∑ j ∈ G.neighborFinset i, n j) {z : D → ℚ} (hz : z ≠ 0) : 0 < qform G z

The quadratic identity: positivity from a positive vector with Mn > 0.

noncomputable def MultiplicativeBasisDeformations.zOf {D : Type v} {ι : Type u_1} (h : ι → D) (w : ι → ℚ) : D → ℚ

Extension by zero of weights on an embedded configuration.

theorem MultiplicativeBasisDeformations.zOf_apply {D : Type v} [Fintype D] [DecidableEq D] {ι : Type u_1} {h : ι → D} (hh : Function.Injective h) (w : ι → ℚ) (i : ι) : zOf h w (h i) = w i

theorem MultiplicativeBasisDeformations.zOf_apply_of_not {D : Type v} [Fintype D] [DecidableEq D] {ι : Type u_1} {h : ι → D} (w : ι → ℚ) {d : D} (hd : ¬∃ (i : ι), h i = d) : zOf h w d = 0

theorem MultiplicativeBasisDeformations.qform_le_config {D : Type v} [Fintype D] [DecidableEq D] (G : SimpleGraph D) [DecidableRel G.Adj] {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {h : ι → D} (hh : Function.Injective h) (w : ι → ℚ) (hw : ∀ (i : ι), 0 ≤ w i) (e : κ → ι × ι) (he : Function.Injective e) (hadj : ∀ (c : κ), G.Adj (h (e c).1) (h (e c).2)) : qform G (zOf h w) ≤ ∑ i : ι, 2 * w i ^ 2 - ∑ c : κ, w (e c).1 * w (e c).2

The configuration bound: for nonnegative weights on embedded vertices and a family of distinct ordered pairs of adjacent vertices among them, zᵀMz ≤ ∑ 2 w² - ∑_{pairs} w w.