The square witness at q = Θ(1/t)

Theorem thm:squarelinear of papers/inflation-nontermination/paper/sections/15-cycles.tex.

The corrected Fourier density with m = 4 families and c = 5, W = Re ∏_g f_g + 5 ∑_g (1 − Re f_g), is pushed forward along the parity read of CycleWitness.lean. Its moments agree with those of the auxiliary density auxH on every set of signs that is empty or meets at least two families, and every character that an injectable, ancestral-product or diagonal prescription looks at has a latent boundary of that kind. So each prescribed pushforward of the new witness equals the corresponding pushforward of parWit, and the obligations are inherited from parWit_diag, parWit_injectable and parWit_ai, which hold for every real q.

Four-factor telescoping

theorem TriangleInflation.Graph.SqWitnessAux.re_prod_lower4 (R : ℝ) (hR0 : 0 < R) (u₀ u₁ u₂ u₃ : ℂ) (h₀ : ‖u₀‖ = R) (h₁ : ‖u₁‖ = R) (h₂ : ‖u₂‖ = R) (h₃ : ‖u₃‖ = R) : R ^ 4 - (u₀ * u₁ * u₂ * u₃).re ≤ 4 * R ^ 3 * (R - u₀.re + (R - u₁.re) + (R - u₂.re) + (R - u₃.re))

The m = 4 case of re_prod_lower: for four complex numbers of modulus R, R⁴ − Re(u₀u₁u₂u₃) ≤ 4R³ ∑_g (R − Re u_g).

theorem TriangleInflation.Graph.SqWitnessAux.sqW_core (R : ℝ) (hR1 : 1 ≤ R) (hRsq : R ^ 2 ≤ 16 / 15) (u₀ u₁ u₂ u₃ : ℂ) (h₀ : ‖u₀‖ = R) (h₁ : ‖u₁‖ = R) (h₂ : ‖u₂‖ = R) (h₃ : ‖u₃‖ = R) : 1 / 3 ≤ (u₀ * u₁ * u₂ * u₃).re + 5 * (1 - u₀.re + (1 - u₁.re) + (1 - u₂.re) + (1 - u₃.re))

The m = 4, c = 5 density Re(u₀u₁u₂u₃) + 5 ∑_g (1 − Re u_g) is at least 1/3 whenever the common modulus R satisfies 1 ≤ R and R² ≤ 16/15.

The corrected density with a general family type

noncomputable def TriangleInflation.Graph.SqWitnessAux.fam {κ : Type u_1} (t : ℕ) (q : ℝ) (s : κ × Fin t → Bool) (g : κ) : ℂ

f_g(s) = ∏_i (1 + i√q s_{g,i}), the factor of the family g.

Equations

• TriangleInflation.Graph.SqWitnessAux.fam t q s g = ∏ i : Fin t, TriangleInflation.Graph.triAtom q (s (g, i))

noncomputable def TriangleInflation.Graph.SqWitnessAux.sqW {κ : Type u_1} [Fintype κ] (t : ℕ) (q : ℝ) (s : κ × Fin t → Bool) : ℝ

W(s) = Re ∏_g f_g + 5 ∑_g (1 − Re f_g).

Equations

• TriangleInflation.Graph.SqWitnessAux.sqW t q s = (∏ g : κ, TriangleInflation.Graph.SqWitnessAux.fam t q s g).re + 5 * ∑ g : κ, (1 - (TriangleInflation.Graph.SqWitnessAux.fam t q s g).re)

theorem TriangleInflation.Graph.SqWitnessAux.fam_norm {κ : Type u_1} {t : ℕ} (q : ℝ) (hq : 0 ≤ q) (s : κ × Fin t → Bool) (g : κ) : ‖fam t q s g‖ = √(1 + q) ^ t

theorem TriangleInflation.Graph.SqWitnessAux.prod_fam {κ : Type u_1} [Fintype κ] {t : ℕ} (q : ℝ) (s : κ × Fin t → Bool) : ∏ g : κ, fam t q s g = ∏ v : κ × Fin t, triAtom q (s v)

theorem TriangleInflation.Graph.SqWitnessAux.prod_two_zeta' {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q : ℝ) (S : Finset ι) : (∏ v : ι, if v ∈ S then 2 * triZeta q else 2) = 2 ^ Fintype.card ι * triZeta q ^ S.card

theorem TriangleInflation.Graph.SqWitnessAux.sum_walsh_prodFam {κ : Type u_1} [Fintype κ] [DecidableEq κ] {t : ℕ} (q : ℝ) (S : Finset (κ × Fin t)) : ∑ s : κ × Fin t → Bool, ↑(walsh S s) * ∏ g : κ, fam t q s g = 2 ^ Fintype.card (κ × Fin t) * triZeta q ^ S.card

theorem TriangleInflation.Graph.SqWitnessAux.fam_as_prod {κ : Type u_1} [Fintype κ] [DecidableEq κ] {t : ℕ} (q : ℝ) (s : κ × Fin t → Bool) (g : κ) : fam t q s g = ∏ v : κ × Fin t, if v.1 = g then triAtom q (s v) else 1

theorem TriangleInflation.Graph.SqWitnessAux.sum_walsh_fam {κ : Type u_1} [Fintype κ] [DecidableEq κ] {t : ℕ} (q : ℝ) (S : Finset (κ × Fin t)) (g : κ) : ∑ s : κ × Fin t → Bool, ↑(walsh S s) * fam t q s g = if ∀ v ∈ S, v.1 = g then 2 ^ Fintype.card (κ × Fin t) * triZeta q ^ S.card else 0

def TriangleInflation.Graph.SqWitnessAux.Spread {κ : Type u_1} {t : ℕ} (S : Finset (κ × Fin t)) : Prop

A set of signs is spread when it is empty or meets at least two families.

Equations

• TriangleInflation.Graph.SqWitnessAux.Spread S = ∀ l ∈ S, ∃ l' ∈ S, l'.1 ≠ l.1

theorem TriangleInflation.Graph.SqWitnessAux.fam_term_zero {κ : Type u_1} [Fintype κ] [DecidableEq κ] {t : ℕ} (q : ℝ) (S : Finset (κ × Fin t)) (hS : Spread S) (g : κ) : ∑ s : κ × Fin t → Bool, (walsh S s - (↑(walsh S s) * fam t q s g).re) = 0

On a spread set the family corrections cancel: the g-term of the moment vanishes.

theorem TriangleInflation.Graph.SqWitnessAux.sqW_moment {κ : Type u_1} [Fintype κ] [DecidableEq κ] {t : ℕ} (q : ℝ) (hq : 0 ≤ q) (S : Finset (κ × Fin t)) (hS : Spread S) : ∑ s : κ × Fin t → Bool, walsh S s * sqW t q s = 2 ^ Fintype.card (κ × Fin t) * triMom q S.card

noncomputable def TriangleInflation.Graph.SqWitnessAux.sqDensity {κ : Type u_1} [Fintype κ] (t : ℕ) (q : ℝ) (s : κ × Fin t → Bool) : ℝ

ρ = 2^{−N} W, the witness density on the auxiliary signs.

Equations

• TriangleInflation.Graph.SqWitnessAux.sqDensity t q s = 1 / 2 ^ Fintype.card (κ × Fin t) * TriangleInflation.Graph.SqWitnessAux.sqW t q s

theorem TriangleInflation.Graph.SqWitnessAux.sqDensity_moment {κ : Type u_1} [Fintype κ] [DecidableEq κ] {t : ℕ} (q : ℝ) (hq : 0 ≤ q) (S : Finset (κ × Fin t)) (hS : Spread S) : ∑ s : κ × Fin t → Bool, sqDensity t q s * ∏ l ∈ S, sgn (s l) = if Even S.card then (-q) ^ (S.card / 2) else 0

theorem TriangleInflation.Graph.SqWitnessAux.sqDensity_sum {κ : Type u_1} [Fintype κ] [DecidableEq κ] {t : ℕ} (q : ℝ) (hq : 0 ≤ q) : ∑ s : κ × Fin t → Bool, sqDensity t q s = 1

theorem TriangleInflation.Graph.SqWitnessAux.sqW_ge {κ : Type u_1} [Fintype κ] {t : ℕ} (e : κ ≃ Fin 4) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑t * q ≤ 1 / 16) (s : κ × Fin t → Bool) : 1 / 3 ≤ sqW t q s

theorem TriangleInflation.Graph.SqWitnessAux.sqDensity_nonneg {κ : Type u_1} [Fintype κ] {t : ℕ} (e : κ ≃ Fin 4) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑t * q ≤ 1 / 16) (s : κ × Fin t → Bool) : 0 ≤ sqDensity t q s

theorem TriangleInflation.Graph.SqWitnessAux.sqDensity_perm {κ : Type u_1} [Fintype κ] {t : ℕ} (q : ℝ) (π : κ → Equiv.Perm (Fin t)) (s : κ × Fin t → Bool) : (sqDensity t q fun (l : κ × Fin t) => s (l.1, (π l.1) l.2)) = sqDensity t q s

The witness on a cycle

noncomputable def TriangleInflation.Graph.SqWitnessAux.sqWit {m : ℕ} (hm : 3 ≤ m) (t : ℕ) (q : ℝ) : GAssign (cycle m hm) t → ℝ

The square-type witness: the corrected density pushed forward along the parity read.

Equations

• TriangleInflation.Graph.SqWitnessAux.sqWit hm t q = TriangleInflation.pushforward (TriangleInflation.Graph.SqWitnessAux.sqDensity t q) TriangleInflation.Graph.CycleWitnessAux.parityRead

theorem TriangleInflation.Graph.SqWitnessAux.sqWit_moment {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 ≤ q) (A : Finset (GObs (cycle m hm) t)) (hA : Spread (CycleWitnessAux.latBd A)) : ∑ ω : GAssign (cycle m hm) t, sqWit hm t q ω * ∏ o ∈ A, sgn (ω o) = ∑ ω : GAssign (cycle m hm) t, CycleWitnessAux.parWit (cycle m hm) t q ω * ∏ o ∈ A, sgn (ω o)

theorem TriangleInflation.Graph.SqWitnessAux.push_eq {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 ≤ q) {β : Type} [Finite β] [DecidableEq β] {ι : Type} [Finite ι] (f : GAssign (cycle m hm) t → β) (E : β ≃ (ι → Bool)) (h : ∀ (F : Finset ι), ∃ (A : Finset (GObs (cycle m hm) t)), Spread (CycleWitnessAux.latBd A) ∧ ∀ (ω : GAssign (cycle m hm) t), ∏ v ∈ F, sgn (E (f ω) v) = ∏ o ∈ A, sgn (ω o)) : pushforward (sqWit hm t q) f = pushforward (CycleWitnessAux.parWit (cycle m hm) t q) f

A pushforward whose characters all pull back to characters with spread latent boundary is the same for the new witness and for parWit.

theorem TriangleInflation.Graph.SqWitnessAux.spread_copy {m t : ℕ} (hm : 3 ≤ m) (ι : (cycle m hm).Edge → Fin t) {A : Finset (GObs (cycle m hm) t)} (hA : A ⊆ copySet ι) : Spread (CycleWitnessAux.latBd A)

theorem TriangleInflation.Graph.SqWitnessAux.spread_family {m t : ℕ} (hm : 3 ≤ m) {n : Type u_1} [Fintype n] (A : n → Finset (GObs (cycle m hm) t)) (ιf : n → (cycle m hm).Edge → Fin t) (hA : ∀ (k : n), A k ⊆ copySet (ιf k)) (hd : ∀ (k k' : n), k ≠ k' → Disjoint (gAncestorsOf (A k)) (gAncestorsOf (A k'))) : Spread (CycleWitnessAux.latBd (Finset.univ.biUnion A))

theorem TriangleInflation.Graph.SqWitnessAux.sqWit_isLaw {m t : ℕ} (hm : 3 ≤ m) (e : (cycle m hm).Edge ≃ Fin 4) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑t * q ≤ 1 / 16) : IsLaw (sqWit hm t q)

theorem TriangleInflation.Graph.SqWitnessAux.sqWit_symmetric {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) : GSymmetric t (sqWit hm t q)

theorem TriangleInflation.Graph.SqWitnessAux.sqWit_diag_eq {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 ≤ q) : pushforward (sqWit hm t q) readDiag = pushforward (CycleWitnessAux.parWit (cycle m hm) t q) readDiag

theorem TriangleInflation.Graph.SqWitnessAux.sqWit_inj_eq {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 ≤ q) (S : Finset (GObs (cycle m hm) t)) (hS : GInjectable S) : pushforward (sqWit hm t q) (gRestrict S) = pushforward (CycleWitnessAux.parWit (cycle m hm) t q) (gRestrict S)

theorem TriangleInflation.Graph.SqWitnessAux.sqWit_ai_eq {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 ≤ q) {n : ℕ} (S : Fin n → Finset (GObs (cycle m hm) t)) (hinj : ∀ (k : Fin n), GInjectable (S k)) (hai : ∀ (k k' : Fin n), k ≠ k' → GAncestrallyIndependent (S k) (S k')) : (pushforward (sqWit hm t q) fun (ω : GAssign (cycle m hm) t) (k : Fin n) => gRestrict (S k) ω) = pushforward (CycleWitnessAux.parWit (cycle m hm) t q) fun (ω : GAssign (cycle m hm) t) (k : Fin n) => gRestrict (S k) ω

B2: the linear-in-t witnesses

theorem TriangleInflation.Graph.square_linear_witness (t : ℕ) (ht : 1 ≤ t) (q : ℝ) (hq : q = 1 / (16 * ↑t)) : GAIFeasible squareGraph t (squareTarget q)

AUDIT-NOTES B2(i). With the corrected Fourier density (m families of t signs, f_g = ∏_i (1 + i√q s_{g,i}), W = Re ∏_g f_g + c ∑_g (1 − Re f_g), m = 4, c = 5, positive for tq ≤ 1/16), the square parity target with q = 1/(16t) passes every AI prescription at order t. This is the source of the Ω(1/t) square lower bound, an order of magnitude better in t than the q = 1/(4m²t²) of cycle_witness.