Linear-in-t witnesses (B2)

Statements split from the original Statements.lean skeleton (one file per proving task); see AUDIT-NOTES B2 and the packet source B6-square-linear-lower-bound.md §1–2 for the mathematics.

Proved here: Walsh orthogonality and the Fourier uniqueness of a law on ι → Bool (funext_of_walsh_moments); the positivity W ≥ 3/5 of the corrected m = 3, c = 4 density for tq ≤ 1/16 (triW_ge), through the division-free form triW_core of the packet's 1 − cos ∑θ_g ≤ 3 ∑ (1 − cos θ_g); the complete moment table triW_moment; the normalization triW_sum and hence triDensity_isLaw; and triParity_isLaw.

Graph/TriangleWitness.lean and Graph/SquareWitness.lean complete triangle_linear_witness and square_linear_witness using the pushforward of this density along the copied-observation map together with symmetry, the diagonal law and the injectable/ancestral prescriptions.

Walsh characters and Fourier uniqueness

A law on ι → Bool is determined by its sign moments. The inversion formula is the orthogonality of the Walsh characters χ_S(w) = ∏_{i ∈ S} sgn (w i).

def TriangleInflation.Graph.walsh {ι : Type u_1} (S : Finset ι) (w : ι → Bool) : ℝ

The Walsh character of a set of coordinates, in the sign convention of sgn.

Equations

• TriangleInflation.Graph.walsh S w = ∏ i ∈ S, TriangleInflation.Graph.sgn (w i)

theorem TriangleInflation.Graph.sgn_ne_zero (b : Bool) : sgn b ≠ 0

theorem TriangleInflation.Graph.sgn_mul_sgn (a b : Bool) : sgn a * sgn b = if a = b then 1 else -1

Two bits have sign product 1 when equal and -1 when different.

theorem TriangleInflation.Graph.sum_prod_subsets {ι : Type u_1} [Fintype ι] (f : ι → ℝ) : ∑ S : Finset ι, ∏ i ∈ S, f i = ∏ i : ι, (f i + 1)

The sum of a product over all subsets is the product of 1 + f i.

theorem TriangleInflation.Graph.walsh_orthogonality {ι : Type u_1} [Fintype ι] (w v : ι → Bool) : ∑ S : Finset ι, walsh S w * walsh S v = if w = v then 2 ^ Fintype.card ι else 0

Orthogonality of the Walsh characters.

theorem TriangleInflation.Graph.funext_of_walsh_moments {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P Q : (ι → Bool) → ℝ) (h : ∀ (S : Finset ι), ∑ w : ι → Bool, walsh S w * P w = ∑ w : ι → Bool, walsh S w * Q w) : P = Q

A weight function on ι → Bool is determined by its Walsh moments.

theorem TriangleInflation.Graph.sum_walsh_mul_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (k : ι → Bool → ℂ) : ∑ s : ι → Bool, ↑(walsh S s) * ∏ v : ι, k v (s v) = ∏ v : ι, if v ∈ S then -k v true + k v false else k v true + k v false

The generating identity behind the moment table: pairing the Walsh character χ_S against a product weight replaces the coordinate sum k v true + k v false by the difference -k v true + k v false exactly at the coordinates of S.

Positivity of the corrected Fourier density (AUDIT-NOTES B2)

The density is ρ(s) = 2^{-3t} W(s) with W = Re (f_x f_y f_z) + 4 ∑_g (1 − Re f_g) and f_g = ∏_i (1 + i√q s_{g,i}). Each f_g has modulus R = (1+q)^{t/2}, and the whole positivity argument is the following inequality about three complex numbers of equal modulus, which replaces the packet's argument through arg by a division-free telescoping of R³ − u₀u₁u₂.

theorem TriangleInflation.Graph.norm_sub_sq_of_norm_eq (A : ℝ) (u : ℂ) (h : ‖u‖ = A) : ‖↑A - u‖ ^ 2 = 2 * A * (A - u.re)

‖A − u‖² = 2A(A − Re u) for a complex number of modulus A.

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

The telescoped triangle inequality plus Cauchy–Schwarz: for three complex numbers of modulus R, R³ − Re(u₀u₁u₂) ≤ 3R² ∑_g (R − Re u_g). This is the m = 3 case of 1 − cos(∑θ_g) ≤ m ∑_g (1 − cos θ_g) in AUDIT-NOTES B2, stated without arg.

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

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

The corrected Fourier density of AUDIT-NOTES B2, m = 3, c = 4

@[reducible, inline]

abbrev TriangleInflation.Graph.TriSign (t : ℕ) : Type

The auxiliary signs of the triangle witness: three families (x, z, y) of t copy indices each.

Equations

• TriangleInflation.Graph.TriSign t = (Fin 3 × Fin t)

noncomputable def TriangleInflation.Graph.triAtom (q : ℝ) (b : Bool) : ℂ

The complex atom 1 + i√q ε of the Fourier density, with ε = sgn b.

Equations

• TriangleInflation.Graph.triAtom q b = 1 + Complex.I * ↑(√q * TriangleInflation.Graph.sgn b)

@[simp]

theorem TriangleInflation.Graph.triAtom_re (q : ℝ) (b : Bool) : (triAtom q b).re = 1

@[simp]

theorem TriangleInflation.Graph.triAtom_im (q : ℝ) (b : Bool) : (triAtom q b).im = √q * sgn b

noncomputable def TriangleInflation.Graph.triFactor (t : ℕ) (q : ℝ) (s : TriSign t → Bool) (g : Fin 3) : ℂ

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

Equations

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

noncomputable def TriangleInflation.Graph.triW (t : ℕ) (q : ℝ) (s : TriSign t → Bool) : ℝ

W(s) = Re(f_x f_z f_y) + 4 ∑_g (1 − Re f_g), the m = 3, c = 4 density of AUDIT-NOTES B2 relative to the uniform sign cube.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.triAtom_norm (q : ℝ) (hq : 0 ≤ q) (b : Bool) : ‖triAtom q b‖ = √(1 + q)

theorem TriangleInflation.Graph.triFactor_norm (t : ℕ) (q : ℝ) (hq : 0 ≤ q) (s : TriSign t → Bool) (g : Fin 3) : ‖triFactor t q s g‖ = √(1 + q) ^ t

theorem TriangleInflation.Graph.one_add_pow_le (t : ℕ) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑t * q ≤ 1 / 16) : (1 + q) ^ t ≤ 16 / 15

(1+q)^t ≤ 1/(1 − tq) ≤ 16/15 when tq ≤ 1/16: Bernoulli on (1−q)^t together with (1−q²)^t ≤ 1.

theorem TriangleInflation.Graph.triW_ge (t : ℕ) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑t * q ≤ 1 / 16) (s : TriSign t → Bool) : 3 / 5 ≤ triW t q s

AUDIT-NOTES B2, the positivity of the corrected density at every sign assignment: W ≥ 3/5 whenever tq ≤ 1/16.

theorem TriangleInflation.Graph.triW_nonneg (t : ℕ) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑t * q ≤ 1 / 16) (s : TriSign t → Bool) : 0 ≤ triW t q s

The moment table (AUDIT-NOTES B2)

E_ρ ∏_{v ∈ S} s_v is 1 for S = ∅, 0 for odd |S|, −3(−q)^{|S|/2} for a nonempty even S inside one family, and (−q)^{|S|/2} for an even S meeting at least two families.

noncomputable def TriangleInflation.Graph.triZeta (q : ℝ) : ℂ

ζ = i√q, the per-coordinate Fourier weight.

Equations

• TriangleInflation.Graph.triZeta q = Complex.I * ↑√q

theorem TriangleInflation.Graph.triZeta_sq (q : ℝ) (hq : 0 ≤ q) : triZeta q ^ 2 = ↑(-q)

def TriangleInflation.Graph.triMom (q : ℝ) (n : ℕ) : ℝ

The target moment of a character with n coordinates: (−q)^{n/2} for even n and 0 for odd n.

Equations

• TriangleInflation.Graph.triMom q n = if n % 2 = 0 then (-q) ^ (n / 2) else 0

theorem TriangleInflation.Graph.triZeta_pow_re (q : ℝ) (hq : 0 ≤ q) (n : ℕ) : (triZeta q ^ n).re = triMom q n

theorem TriangleInflation.Graph.triAtom_add (q : ℝ) : triAtom q true + triAtom q false = 2

theorem TriangleInflation.Graph.triAtom_sub (q : ℝ) : -triAtom q true + triAtom q false = 2 * triZeta q

theorem TriangleInflation.Graph.prod_ite_mem_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (A B : ℂ) : (∏ v : ι, if v ∈ S then A else B) = A ^ S.card * B ^ (Fintype.card ι - S.card)

A two-valued product over a finite type.

theorem TriangleInflation.Graph.card_triSign (t : ℕ) : Fintype.card (TriSign t) = 3 * t

theorem TriangleInflation.Graph.prod_two_zeta (t : ℕ) (q : ℝ) (S : Finset (TriSign t)) : (∏ v : TriSign t, if v ∈ S then 2 * triZeta q else 2) = 2 ^ (3 * t) * triZeta q ^ S.card

The Walsh pairing of the two-valued weight 2ζ on S and 2 off S.

theorem TriangleInflation.Graph.triFactor_prod (t : ℕ) (q : ℝ) (s : TriSign t → Bool) : triFactor t q s 0 * triFactor t q s 1 * triFactor t q s 2 = ∏ v : TriSign t, triAtom q (s v)

The full product f_x f_z f_y is the product of the atoms over all auxiliary signs.

theorem TriangleInflation.Graph.sum_walsh_triProd (t : ℕ) (q : ℝ) (S : Finset (TriSign t)) : ∑ s : TriSign t → Bool, ↑(walsh S s) * (triFactor t q s 0 * triFactor t q s 1 * triFactor t q s 2) = 2 ^ (3 * t) * triZeta q ^ S.card

The Walsh moment of the product density.

theorem TriangleInflation.Graph.triFactor_as_prod (t : ℕ) (q : ℝ) (s : TriSign t → Bool) (g : Fin 3) : triFactor t q s g = ∏ v : TriSign t, if v.1 = g then triAtom q (s v) else 1

The family factor as a product over all auxiliary signs.

theorem TriangleInflation.Graph.sum_walsh_triFactor (t : ℕ) (q : ℝ) (S : Finset (TriSign t)) (g : Fin 3) : ∑ s : TriSign t → Bool, ↑(walsh S s) * triFactor t q s g = if ∀ v ∈ S, v.1 = g then 2 ^ (3 * t) * triZeta q ^ S.card else 0

The Walsh moment of a single family factor: zero unless S lies inside that family.

theorem TriangleInflation.Graph.sum_walsh_triOne (t : ℕ) (S : Finset (TriSign t)) : ∑ s : TriSign t → Bool, ↑(walsh S s) = if S = ∅ then 2 ^ (3 * t) else 0

The Walsh moment of the constant density.

def TriangleInflation.Graph.triCoeff {t : ℕ} (S : Finset (TriSign t)) : ℝ

The Fourier coefficient correction of AUDIT-NOTES B2 with c = 4: the characters that are nonempty and confined to one sign family have their moment multiplied by 1 − 4 = −3; every other character keeps the target moment.

Equations

• TriangleInflation.Graph.triCoeff S = if S = ∅ then 1 else if ∃ (g : Fin 3), ∀ v ∈ S, v.1 = g then -3 else 1

theorem TriangleInflation.Graph.triW_moment (t : ℕ) (q : ℝ) (hq : 0 ≤ q) (S : Finset (TriSign t)) : ∑ s : TriSign t → Bool, walsh S s * triW t q s = 2 ^ (3 * t) * (triCoeff S * triMom q S.card)

AUDIT-NOTES B2, the moment table of the corrected density. Against the uniform sign cube, ∑_s χ_S(s) W(s) = 2^{3t} c_S (−q)^{|S|/2} with c_S = 1 for S = ∅ or S meeting at least two families and c_S = −3 for a nonempty S inside one family; the moment vanishes for odd |S|.

theorem TriangleInflation.Graph.triW_sum (t : ℕ) (q : ℝ) (hq : 0 ≤ q) : ∑ s : TriSign t → Bool, triW t q s = 2 ^ (3 * t)

The density normalizes: E W = 1 against the uniform sign cube.

noncomputable def TriangleInflation.Graph.triDensity (t : ℕ) (q : ℝ) (s : TriSign t → Bool) : ℝ

ρ(s) = 2^{-3t} W(s), the witness density on the auxiliary signs.

Equations

• TriangleInflation.Graph.triDensity t q s = 1 / 2 ^ (3 * t) * TriangleInflation.Graph.triW t q s

theorem TriangleInflation.Graph.triDensity_isLaw (t : ℕ) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑t * q ≤ 1 / 16) : IsLaw (triDensity t q)

AUDIT-NOTES B2: the corrected density is a genuine probability law on the 3t auxiliary signs whenever tq ≤ 1/16.

theorem TriangleInflation.Graph.triParity_isLaw (q : ℝ) (hq0 : 0 ≤ q) (hq : q ≤ 1 / 3) : IsLaw (triParity q) ∧ triMeanA (triParity q) = -q ∧ triMeanB (triParity q) = -q ∧ triMeanC (triParity q) = -q

The parity-perfect triangle target is a law with all one- and two-point moments −q.