Cycle witnesses at every order, incompatibility and distance

AUDIT-NOTES A5 / Theorem thm:cycle: the parity witness cycle_witness (from CycleWitness.lean), the incompatibility of the cycle target (cycle_not_compatible) and the distance bound q/10 ≤ d_TV (cycle_distance), the last two through the quantitative parity rigidity CycleModelAux.quant_rigidity (Lemma lem:quantrigidity). Everything here is proved.

theorem TriangleInflation.Graph.cycle_witness (m t : ℕ) (hm : 3 ≤ m) (ht : 1 ≤ t) (q : ℝ) (hq : q = 1 / (4 * ↑m ^ 2 * ↑t ^ 2)) : GAIFeasible (cycle m hm) t (cycleTarget m q)

AUDIT-NOTES A5, the cycle witness. With N = mt auxiliary signs s_{v,i} carrying the positive density H_{N,q}(s) = 2^{−N} ∑_{|S| even} (−q)^{|S|/2} ∏_S s, and copied observations O_v^{ij} = s_{v−1,i} s_{v,j}, the target P_{m,q} with moments (−q)^{|∂F|/2} passes every AI prescription at order t, for q = 1/(4m²t²): the boundaries of ancestrally disjoint injectable blocks are disjoint, so their moments multiply.

theorem TriangleInflation.Graph.cycle_exp_witness (m t : ℕ) (hm : 3 ≤ m) (ht : 1 ≤ t) (q : ℝ) (hq : q = 1 / (4 * ↑m ^ 2 * ↑t ^ 2)) : GExpFeasible (cycle m hm) t (cycleTarget m q)

The same witness passes the recursively expressible test, by AUDIT-NOTES A2.

Auxiliary material for the cycle arcs

Nothing in this namespace changes the two statements below, which appear in their original form.

def TriangleInflation.Graph.CycleModelAux.av {X : Type u_2} [Fintype X] (μ f : X → ℝ) : ℝ

Weighted average of a function over a finite latent alphabet.

Equations

• TriangleInflation.Graph.CycleModelAux.av μ f = ∑ x : X, μ x * f x

theorem TriangleInflation.Graph.CycleModelAux.av_mono {X : Type u_1} [Fintype X] {μ f g : X → ℝ} (hμ : ∀ (x : X), 0 ≤ μ x) (h : ∀ (x : X), f x ≤ g x) : av μ f ≤ av μ g

theorem TriangleInflation.Graph.CycleModelAux.av_const {X : Type u_1} [Fintype X] {μ : X → ℝ} (hμ : IsLaw μ) (k : ℝ) : (av μ fun (x : X) => k) = k

theorem TriangleInflation.Graph.CycleModelAux.av_sub {X : Type u_1} [Fintype X] (μ f g : X → ℝ) : (av μ fun (x : X) => f x - g x) = av μ f - av μ g

theorem TriangleInflation.Graph.CycleModelAux.av_add {X : Type u_1} [Fintype X] (μ f g : X → ℝ) : (av μ fun (x : X) => f x + g x) = av μ f + av μ g

theorem TriangleInflation.Graph.CycleModelAux.av_abs_le {X : Type u_1} [Fintype X] {μ : X → ℝ} (hμ : ∀ (x : X), 0 ≤ μ x) (f : X → ℝ) : |av μ f| ≤ av μ fun (x : X) => |f x|

theorem TriangleInflation.Graph.CycleModelAux.abs_av_le {X : Type u_1} [Fintype X] {μ : X → ℝ} (hμ : IsLaw μ) {f : X → ℝ} {k : ℝ} (h : ∀ (x : X), |f x| ≤ k) : |av μ f| ≤ k

theorem TriangleInflation.Graph.CycleModelAux.av_mul_left {X : Type u_1} [Fintype X] (μ f : X → ℝ) (k : ℝ) : (av μ fun (x : X) => k * f x) = k * av μ f

theorem TriangleInflation.Graph.CycleModelAux.av_mul_av {X : Type u_1} [Fintype X] {Y : Type u_2} [Fintype Y] (μ : X → ℝ) (ν : Y → ℝ) (F : X → ℝ) (G : Y → ℝ) : av μ F * av ν G = av μ fun (x : X) => av ν fun (y : Y) => F x * G y

theorem TriangleInflation.Graph.CycleModelAux.av_nonneg {X : Type u_1} [Fintype X] {μ f : X → ℝ} (hμ : ∀ (x : X), 0 ≤ μ x) (h : ∀ (x : X), 0 ≤ f x) : 0 ≤ av μ f

theorem TriangleInflation.Graph.CycleModelAux.av_one_sub {X : Type u_1} [Fintype X] {μ : X → ℝ} (hμ : IsLaw μ) (f : X → ℝ) : (av μ fun (x : X) => 1 - f x) = 1 - av μ f

theorem TriangleInflation.Graph.CycleModelAux.exists_le_of_av {X : Type u_1} [Fintype X] {μ f : X → ℝ} (hμ : IsLaw μ) {c : ℝ} (hf : av μ f = c) : ∃ (x : X), 0 < μ x ∧ f x ≤ c

theorem TriangleInflation.Graph.CycleModelAux.av2_sub {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (μ : A → ℝ) (ν : B → ℝ) (f g : A → B → ℝ) : ((av μ fun (p : A) => av ν fun (q : B) => f p q) - av μ fun (p : A) => av ν fun (q : B) => g p q) = av μ fun (p : A) => av ν fun (q : B) => f p q - g p q

theorem TriangleInflation.Graph.CycleModelAux.abs_av2_le_av2 {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {μ : A → ℝ} {ν : B → ℝ} (hμ : ∀ (p : A), 0 ≤ μ p) (hν : ∀ (q : B), 0 ≤ ν q) (f : A → B → ℝ) : |av μ fun (p : A) => av ν fun (q : B) => f p q| ≤ av μ fun (p : A) => av ν fun (q : B) => |f p q|

theorem TriangleInflation.Graph.CycleModelAux.abs_av3_le_av3 {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] {μ : A → ℝ} {ν : B → ℝ} {ρ : C → ℝ} (hμ : ∀ (p : A), 0 ≤ μ p) (hν : ∀ (q : B), 0 ≤ ν q) (hρ : ∀ (s : C), 0 ≤ ρ s) (f : A → B → C → ℝ) : |av μ fun (p : A) => av ν fun (q : B) => av ρ fun (s : C) => f p q s| ≤ av μ fun (p : A) => av ν fun (q : B) => av ρ fun (s : C) => |f p q s|

theorem TriangleInflation.Graph.CycleModelAux.av3_sub {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (μ : A → ℝ) (ν : B → ℝ) (ρ : C → ℝ) (f g : A → B → C → ℝ) : ((av μ fun (p : A) => av ν fun (q : B) => av ρ fun (s : C) => f p q s) - av μ fun (p : A) => av ν fun (q : B) => av ρ fun (s : C) => g p q s) = av μ fun (p : A) => av ν fun (q : B) => av ρ fun (s : C) => f p q s - g p q s

theorem TriangleInflation.Graph.CycleModelAux.av3_const_inner {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (μ : A → ℝ) (ν : B → ℝ) {ρ : C → ℝ} (hρ : IsLaw ρ) (f : A → B → ℝ) : (av μ fun (p : A) => av ν fun (q : B) => av ρ fun (x : C) => f p q) = av μ fun (p : A) => av ν fun (q : B) => f p q

theorem TriangleInflation.Graph.CycleModelAux.abs_sub_le_one_sub_mul {p r : ℝ} (hp : |p| ≤ 1) (hr : |r| ≤ 1) : |p - r| ≤ 1 - p * r

theorem TriangleInflation.Graph.CycleModelAux.two_mul_le_abs_add {u w : ℝ} (hu : |u| ≤ 1) (hw : |w| ≤ 1) : 2 * (u * w) ≤ |u + w|

theorem TriangleInflation.Graph.CycleModelAux.abs_mul2_le_one {p q : ℝ} (hp : |p| ≤ 1) (hq : |q| ≤ 1) : |p * q| ≤ 1

theorem TriangleInflation.Graph.CycleModelAux.abs_mul3_le_one {p q s : ℝ} (hp : |p| ≤ 1) (hq : |q| ≤ 1) (hs : |s| ≤ 1) : |p * q * s| ≤ 1

theorem TriangleInflation.Graph.CycleModelAux.av2_one_sub {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {μ : A → ℝ} {ν : B → ℝ} (hμ : IsLaw μ) (hν : IsLaw ν) (f : A → B → ℝ) : (av μ fun (p : A) => av ν fun (q : B) => 1 - f p q) = 1 - av μ fun (p : A) => av ν fun (q : B) => f p q

theorem TriangleInflation.Graph.CycleModelAux.av3_one_sub {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] {μ : A → ℝ} {ν : B → ℝ} {ρ : C → ℝ} (hμ : IsLaw μ) (hν : IsLaw ν) (hρ : IsLaw ρ) (f : A → B → C → ℝ) : (av μ fun (p : A) => av ν fun (q : B) => av ρ fun (s : C) => 1 - f p q s) = 1 - av μ fun (p : A) => av ν fun (q : B) => av ρ fun (s : C) => f p q s

theorem TriangleInflation.Graph.CycleModelAux.quant_rigidity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (μX : X → ℝ) (μY : Y → ℝ) (μZ : Z → ℝ) (hX : IsLaw μX) (hY : IsLaw μY) (hZ : IsLaw μZ) (a : X → Z → ℝ) (b : X → Y → ℝ) (c : Z → Y → ℝ) (ha : ∀ (x : X) (z : Z), |a x z| ≤ 1) (hb : ∀ (x : X) (y : Y), |b x y| ≤ 1) (hc : ∀ (z : Z) (y : Y), |c z y| ≤ 1) (r : ℝ) (hAr : (av μX fun (x : X) => av μZ fun (z : Z) => a x z) ≤ r) (hBr : (av μY fun (y : Y) => av μX fun (x : X) => b x y) ≤ r) (hCr : (av μY fun (y : Y) => av μZ fun (z : Z) => c z y) ≤ r) : -4 * (1 - av μY fun (y : Y) => av μX fun (x : X) => av μZ fun (z : Z) => a x z * b x y * c z y) ≤ r

Quantitative parity rigidity for the triangle pattern.

theorem TriangleInflation.Graph.CycleModelAux.sum_pi_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] (g : (i : ι) → β i → ℝ) : ∑ x : (i : ι) → β i, ∏ i : ι, g i (x i) = ∏ i : ι, ∑ s : β i, g i s

def TriangleInflation.Graph.CycleModelAux.sResp {Γ : PairGraph} (M : GModel Γ) (v : Γ.V) (x : (e : Γ.Edge) → M.L e) : ℝ

The sign response of a model at a vertex: E[sgn O_v | sources].

Equations

• TriangleInflation.Graph.CycleModelAux.sResp M v x = (2 * M.resp v fun (e : ↥(Γ.inc v)) => x ↑e) - 1

theorem TriangleInflation.Graph.CycleModelAux.sResp_congr {Γ : PairGraph} (M : GModel Γ) (v : Γ.V) {x x' : (e : Γ.Edge) → M.L e} (h : ∀ e ∈ Γ.inc v, x e = x' e) : sResp M v x = sResp M v x'

theorem TriangleInflation.Graph.CycleModelAux.sResp_bound {Γ : PairGraph} (M : GModel Γ) (hM : M.Valid) (v : Γ.V) (x : (e : Γ.Edge) → M.L e) : -1 ≤ sResp M v x ∧ sResp M v x ≤ 1

def TriangleInflation.Graph.CycleModelAux.lat {Γ : PairGraph} (M : GModel Γ) (x : (e : Γ.Edge) → M.L e) : ℝ

The latent measure of a model.

Equations

• TriangleInflation.Graph.CycleModelAux.lat M x = ∏ e : Γ.Edge, M.μ e (x e)

theorem TriangleInflation.Graph.CycleModelAux.lat_nonneg {Γ : PairGraph} (M : GModel Γ) (hM : M.Valid) (x : (e : Γ.Edge) → M.L e) : 0 ≤ lat M x

theorem TriangleInflation.Graph.CycleModelAux.lat_sum {Γ : PairGraph} (M : GModel Γ) (hM : M.Valid) : ∑ x : (e : Γ.Edge) → M.L e, lat M x = 1

theorem TriangleInflation.Graph.CycleModelAux.lat_isLaw {Γ : PairGraph} (M : GModel Γ) (hM : M.Valid) : IsLaw (lat M)

theorem TriangleInflation.Graph.CycleModelAux.moment_eq {Γ : PairGraph} (M : GModel Γ) (F : Finset Γ.V) : ∑ w : Γ.V → Bool, M.law w * ∏ v ∈ F, sgn (w v) = ∑ x : (e : Γ.Edge) → M.L e, lat M x * ∏ v ∈ F, sResp M v x

The Walsh moments of the observed law of a model.

theorem TriangleInflation.Graph.CycleModelAux.lat_update {Γ : PairGraph} (M : GModel Γ) (e₀ : Γ.Edge) (x : (e : Γ.Edge) → M.L e) (s : M.L e₀) : lat M (Function.update x e₀ s) * M.μ e₀ (x e₀) = lat M x * M.μ e₀ s

theorem TriangleInflation.Graph.CycleModelAux.rerand {Γ : PairGraph} (M : GModel Γ) (hM : M.Valid) (e₀ : Γ.Edge) (f : ((e : Γ.Edge) → M.L e) → ℝ) : ∑ s : M.L e₀, ∑ x : (e : Γ.Edge) → M.L e, M.μ e₀ s * (lat M x * f (Function.update x e₀ s)) = ∑ x : (e : Γ.Edge) → M.L e, lat M x * f x

Re-randomizing one source coordinate does not change a latent average.

theorem TriangleInflation.Graph.CycleModelAux.cycleNext_val' {m : ℕ} (v : Fin m) : ↑(cycleNext v) = if ↑v + 1 = m then 0 else ↑v + 1

theorem TriangleInflation.Graph.CycleModelAux.cycleNext_ne {m : ℕ} (hm : 2 ≤ m) (v : Fin m) : v ≠ cycleNext v

theorem TriangleInflation.Graph.CycleModelAux.cycle_adj_next {m : ℕ} (hm : 3 ≤ m) (i : Fin m) : (cycleAdj m).Adj i (cycleNext i)

theorem TriangleInflation.Graph.CycleModelAux.mem_edgeFinset_cycle {m : ℕ} (hm : 3 ≤ m) {a b : Fin m} (h : (cycleAdj m).Adj a b) : s(a, b) ∈ (cycle m hm).G.edgeFinset

theorem TriangleInflation.Graph.CycleModelAux.adj_of_mem_edgeFinset {m : ℕ} (hm : 3 ≤ m) {a b : Fin m} (h : s(a, b) ∈ (cycle m hm).G.edgeFinset) : (cycleAdj m).Adj a b

def TriangleInflation.Graph.CycleModelAux.cEdge (m : ℕ) (hm : 3 ≤ m) (i : Fin m) : (cycle m hm).Edge

The edge of the cycle recorded by its lower endpoint.

Equations

• TriangleInflation.Graph.CycleModelAux.cEdge m hm i = TriangleInflation.Graph.CycleWitnessAux.ce hm i

theorem TriangleInflation.Graph.CycleModelAux.cEdge_val {m : ℕ} (hm : 3 ≤ m) (i : Fin m) : ↑(cEdge m hm i) = s(i, cycleNext i)

theorem TriangleInflation.Graph.CycleModelAux.mem_inc {m : ℕ} {hm : 3 ≤ m} (v : (cycle m hm).V) (e : (cycle m hm).Edge) : e ∈ (cycle m hm).inc v ↔ v ∈ ↑e

theorem TriangleInflation.Graph.CycleModelAux.inc_cases {m : ℕ} (hm : 3 ≤ m) (v : Fin m) (e : (cycle m hm).Edge) (h : e ∈ (cycle m hm).inc v) : e = cEdge m hm v ∨ ∃ (p : Fin m), cycleNext p = v ∧ e = cEdge m hm p

Every source incident to v is recorded either by v or by a predecessor of v.

The three arcs {0}, {1} and {2,…,m-1}

def TriangleInflation.Graph.CycleModelAux.cv0 (m : ℕ) (hm : 3 ≤ m) : Fin m

The vertex 0 of the cycle.

Equations

• TriangleInflation.Graph.CycleModelAux.cv0 m hm = ⟨0, ⋯⟩

def TriangleInflation.Graph.CycleModelAux.cv1 (m : ℕ) (hm : 3 ≤ m) : Fin m

The vertex 1 of the cycle.

Equations

• TriangleInflation.Graph.CycleModelAux.cv1 m hm = ⟨1, ⋯⟩

def TriangleInflation.Graph.CycleModelAux.cvl (m : ℕ) (hm : 3 ≤ m) : Fin m

The vertex m-1 of the cycle.

Equations

• TriangleInflation.Graph.CycleModelAux.cvl m hm = ⟨m - 1, ⋯⟩

theorem TriangleInflation.Graph.CycleModelAux.cycleNext_cv0 {m : ℕ} (hm : 3 ≤ m) : cycleNext (cv0 m hm) = cv1 m hm

theorem TriangleInflation.Graph.CycleModelAux.cycleNext_cv1 {m : ℕ} (hm : 3 ≤ m) : ↑(cycleNext (cv1 m hm)) = 2

theorem TriangleInflation.Graph.CycleModelAux.cycleNext_cvl {m : ℕ} (hm : 3 ≤ m) : cycleNext (cvl m hm) = cv0 m hm

theorem TriangleInflation.Graph.CycleModelAux.mem_cEdge_iff {m : ℕ} (hm : 3 ≤ m) (v i : Fin m) : cEdge m hm i ∈ (cycle m hm).inc v ↔ v = i ∨ v = cycleNext i

Membership in the incidence set of the source recorded by i.

theorem TriangleInflation.Graph.CycleModelAux.inc_cv0 {m : ℕ} (hm : 3 ≤ m) (e : (cycle m hm).Edge) (h : e ∈ (cycle m hm).inc (cv0 m hm)) : e = cEdge m hm (cv0 m hm) ∨ e = cEdge m hm (cvl m hm)

The sources incident to vertex 0 are those recorded by m-1 and by 0.

theorem TriangleInflation.Graph.CycleModelAux.inc_cv1 {m : ℕ} (hm : 3 ≤ m) (e : (cycle m hm).Edge) (h : e ∈ (cycle m hm).inc (cv1 m hm)) : e = cEdge m hm (cv1 m hm) ∨ e = cEdge m hm (cv0 m hm)

The sources incident to vertex 1 are those recorded by 0 and by 1.

theorem TriangleInflation.Graph.CycleModelAux.cEdge_cv0_not_mem_inc {m : ℕ} (hm : 3 ≤ m) (v : Fin m) (hv : 2 ≤ ↑v) : cEdge m hm (cv0 m hm) ∉ (cycle m hm).inc v

The source {0,1} meets no vertex of the long arc.

theorem TriangleInflation.Graph.CycleModelAux.cEdge_cv1_not_mem_inc_cv0 {m : ℕ} (hm : 3 ≤ m) : cEdge m hm (cv1 m hm) ∉ (cycle m hm).inc (cv0 m hm)

The source {1,2} does not meet the vertex 0.

theorem TriangleInflation.Graph.CycleModelAux.cEdge_cv0_ne_cv1 {m : ℕ} (hm : 3 ≤ m) : cEdge m hm (cv0 m hm) ≠ cEdge m hm (cv1 m hm)

The boundaries of the three arcs

theorem TriangleInflation.Graph.CycleModelAux.boundary_card_two {m : ℕ} (_hm : 3 ≤ m) (F : Finset (Fin m)) (p q : Fin m) (hpq : ↑p ≠ ↑q) (h : ∀ (v : Fin m), ¬(v ∈ F ↔ cycleNext v ∈ F) ↔ ↑v = ↑p ∨ ↑v = ↑q) : (cycleBoundary m F).card = 2

theorem TriangleInflation.Graph.CycleModelAux.mem_arcA {m : ℕ} (hm : 3 ≤ m) (u : Fin m) : u ∈ {cv0 m hm} ↔ ↑u = 0

theorem TriangleInflation.Graph.CycleModelAux.mem_arcB {m : ℕ} (hm : 3 ≤ m) (u : Fin m) : u ∈ {cv1 m hm} ↔ ↑u = 1

theorem TriangleInflation.Graph.CycleModelAux.mem_pair01 {m : ℕ} (hm : 3 ≤ m) (u : Fin m) : u ∈ {cv0 m hm, cv1 m hm} ↔ ↑u = 0 ∨ ↑u = 1

theorem TriangleInflation.Graph.CycleModelAux.boundary_arcA {m : ℕ} (hm : 3 ≤ m) : (cycleBoundary m {cv0 m hm}).card = 2

theorem TriangleInflation.Graph.CycleModelAux.boundary_arcB {m : ℕ} (hm : 3 ≤ m) : (cycleBoundary m {cv1 m hm}).card = 2

theorem TriangleInflation.Graph.CycleModelAux.boundary_arcC {m : ℕ} (hm : 3 ≤ m) : (cycleBoundary m {cv0 m hm, cv1 m hm}ᶜ).card = 2

Re-randomization in the average form

theorem TriangleInflation.Graph.CycleModelAux.av_def {X : Type u_1} [Fintype X] (μ f : X → ℝ) : av μ f = ∑ x : X, μ x * f x

theorem TriangleInflation.Graph.CycleModelAux.av_rerand {Γ : PairGraph} (M : GModel Γ) (hM : M.Valid) (e₀ : Γ.Edge) (f : ((e : Γ.Edge) → M.L e) → ℝ) : (av (M.μ e₀) fun (s : M.L e₀) => av (lat M) fun (x : (e : Γ.Edge) → M.L e) => f (Function.update x e₀ s)) = av (lat M) f

The Walsh moments of a model of the cycle

theorem TriangleInflation.Graph.CycleModelAux.cycle_moment {m : ℕ} (hm : 3 ≤ m) (q : ℝ) (M : GModel (cycle m hm)) (hlaw : M.law = cycleTarget m q) (F : Finset (Fin m)) : (av (lat M) fun (x : (e : (cycle m hm).Edge) → M.L e) => ∏ v ∈ F, sResp M v x) = (-q) ^ ((cycleBoundary m F).card / 2)

Reduction of a model to the triangle pattern

Two sources eX, eY and three groups of vertices: v0, which does not see eY; v1, which sees only eX and eY; and a block S, no vertex of which sees eX.

theorem TriangleInflation.Graph.CycleModelAux.tri_reduction {Γ : PairGraph} (M : GModel Γ) (hM : M.Valid) (eX eY : Γ.Edge) (hXY : eX ≠ eY) (v0 v1 : Γ.V) (S : Finset Γ.V) (hprodsplit : ∀ (y : (e : Γ.Edge) → M.L e), sResp M v0 y * sResp M v1 y * ∏ v ∈ S, sResp M v y = ∏ v : Γ.V, sResp M v y) (hv0 : eY ∉ Γ.inc v0) (hv1 : ∀ e ∈ Γ.inc v1, e = eX ∨ e = eY) (hS : ∀ v ∈ S, eX ∉ Γ.inc v) (r : ℝ) (hA : (av (lat M) fun (x : (e : Γ.Edge) → M.L e) => sResp M v0 x) ≤ r) (hB : (av (lat M) fun (x : (e : Γ.Edge) → M.L e) => sResp M v1 x) ≤ r) (hC : (av (lat M) fun (x : (e : Γ.Edge) → M.L e) => ∏ v ∈ S, sResp M v x) ≤ r) : -4 * (1 - av (lat M) fun (x : (e : Γ.Edge) → M.L e) => ∏ v : Γ.V, sResp M v x) ≤ r

The cycle case of the reduction

theorem TriangleInflation.Graph.CycleModelAux.cycle_arc_bound {m : ℕ} (hm : 3 ≤ m) (M : GModel (cycle m hm)) (hM : M.Valid) (r : ℝ) (hA : (av (lat M) fun (x : (e : (cycle m hm).Edge) → M.L e) => sResp M (cv0 m hm) x) ≤ r) (hB : (av (lat M) fun (x : (e : (cycle m hm).Edge) → M.L e) => sResp M (cv1 m hm) x) ≤ r) (hC : (av (lat M) fun (x : (e : (cycle m hm).Edge) → M.L e) => ∏ v ∈ {cv0 m hm, cv1 m hm}ᶜ, sResp M v x) ≤ r) : -4 * (1 - av (lat M) fun (x : (e : (cycle m hm).Edge) → M.L e) => ∏ v : Fin m, sResp M v x) ≤ r

Transfer of moments along total variation

theorem TriangleInflation.Graph.CycleModelAux.moment_transfer {α : Type u_1} [Fintype α] (P Q f : α → ℝ) (hf : ∀ (a : α), |f a| ≤ 1) : |∑ a : α, P a * f a - ∑ a : α, Q a * f a| ≤ 2 * dTV P Q

theorem TriangleInflation.Graph.CycleModelAux.abs_prod_sgn {α : Type u_1} (F : Finset α) (w : α → Bool) : |∏ v ∈ F, sgn (w v)| ≤ 1

The compatible set is nonempty

theorem TriangleInflation.Graph.CycleModelAux.exists_gCompatible (Γ : PairGraph) : ∃ (Q : GTarget Γ), GCompatible Γ Q

theorem TriangleInflation.Graph.cycle_not_compatible (m : ℕ) (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 < q) : ¬GCompatible (cycle m hm) (cycleTarget m q)

AUDIT-NOTES A5, incompatibility of the cycle target. Partition the cycle into three nonempty contiguous arcs and output the product of the signs in each arc: a compatible cycle law induces a compatible triangle law, parity-perfect, whose three means are all -q, and (-q)^3 < 0 contradicts parity_rigidity. (The proof below uses the quantitative form CycleModelAux.quant_rigidity of rigidity, which subsumes the exact one.)

theorem TriangleInflation.Graph.cycle_distance (m : ℕ) (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 < q) : q / 12 ≤ distToCompatible (cycle m hm) (cycleTarget m q)

AUDIT-NOTES A5, the quantitative form: parity repair (a compatible law with parity error η is within 5η of a parity-perfect compatible law) turns the rigidity contradiction into d_TV(P_{m,q}, C_{C_m}) ≥ q/12. The proof below replaces the repair construction by the moment form CycleModelAux.quant_rigidity, which gives the sharper constant q/10; the hypothesis m² q ≤ 1/4 (which makes cycleTarget a law) is not needed for the bound.