Forbidden configurations

Proof of Proposition 4.1, Step 2 (periodic-mesh-calculations.tex): "A vertex of degree at least four would contain a four-leaf star, and the vector z with entries two at the centre and one at the leaves satisfies zᵀMz = 0 on it. Two trivalent vertices would contain their connecting path and two extra edges at each end; weights two on the path and one on its four leaves again give a nonzero vector z with zᵀMz = 0. Both contradict positive definiteness of principal submatrices."

With the configuration bound (qform_le_config), the extra edges of the whole graph only lower zᵀMz, so each configuration gives zᵀMz ≤ 0.

theorem MultiplicativeBasisDeformations.config_false {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) {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {h : ι → D} (hh : Function.Injective h) (w : ι → ℚ) (hw : ∀ (i : ι), 0 ≤ w i) (i₀ : ι) (hi₀ : w i₀ ≠ 0) (e : κ → ι × ι) (he : Function.Injective e) (hadj : ∀ (c : κ), G.Adj (h (e c).1) (h (e c).2)) (hle : ∑ i : ι, 2 * w i ^ 2 ≤ ∑ c : κ, w (e c).1 * w (e c).2) : False

A configuration with nonnegative, not all zero, weights and ∑ 2 w² ≤ ∑ w w over distinct adjacent pairs cannot occur.

theorem MultiplicativeBasisDeformations.degree_le_three {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) (v : D) : G.degree v ≤ 3

No vertex of degree four.

theorem MultiplicativeBasisDeformations.no_two_trivalent {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) {m : ℕ} (p : Fin (m + 1) → D) (l : Fin 4 → D) (hinj : Function.Injective (Sum.elim p l)) (hpath : ∀ (k : Fin m), G.Adj (p k.castSucc) (p k.succ)) (hl : ∀ (j : Fin 4), G.Adj (if ↑j < 2 then p 0 else p (Fin.last m)) (l j)) : False

No two trivalent vertices: the configuration of a path p₀ … p_m with two extra leaves at each end cannot occur.

theorem MultiplicativeBasisDeformations.arm_sum_aux (L : ℕ) : 2 * ∑ j ∈ Finset.range (L + 1), (↑j + 1) ^ 2 - 2 * ∑ j ∈ Finset.range L, (↑j + 1) * (↑j + 2) = (↑L + 1) * (↑L + 2)

The sum identity behind the arm computation.

theorem MultiplicativeBasisDeformations.arm_contribution (L : ℕ) : ∑ k ∈ Finset.range (L + 1), 2 * ((↑L + 1 - ↑k) / (↑L + 2)) ^ 2 - 2 * ((↑L + 1) / (↑L + 2)) - ∑ k ∈ Finset.range L, 2 * ((↑L + 1 - ↑k) / (↑L + 2) * ((↑L - ↑k) / (↑L + 2))) = -((↑L + 1) / (↑L + 2))

The arm computation (the Schur complement at the centre): for one arm of length L + 1 with weights (L + 1 - k)/(L + 2), its contribution is -(L+1)/(L+2).

theorem MultiplicativeBasisDeformations.sigma_fin_eq_iff {t : ℕ} {L : Fin t → ℕ} {a b : Fin t} {k : Fin (L a + 1)} {k' : Fin (L b + 1)} : ⟨a, k⟩ = ⟨b, k'⟩ ↔ a = b ∧ ↑k = ↑k'

theorem MultiplicativeBasisDeformations.arm_inequality {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) {t : ℕ} (L : Fin t → ℕ) (c : D) (a : (i : Fin t) → Fin (L i + 1) → D) (hinj : Function.Injective (Sum.elim (fun (x : Unit) => c) fun (x : (i : Fin t) × Fin (L i + 1)) => a x.fst x.snd)) (hc : ∀ (i : Fin t), G.Adj c (a i 0)) (ha : ∀ (i : Fin t) (k : Fin (L i)), G.Adj (a i k.castSucc) (a i k.succ)) : ∑ i : Fin t, (↑(L i) + 1) / (↑(L i) + 2) < 2

The arm inequality (Schur complement at the centre, periodic-mesh-calculations.tex): a centre with t arms of lengths L_i + 1 satisfies ∑_i (L_i + 1)/(L_i + 2) < 2, i.e. 2 - ∑ p_i/(p_i + 1) > 0 for arm lengths p_i.