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

AUDIT-NOTES B2(ii) / Theorem thm:trianglelinear: with the corrected density of Linear.lean (m = 3, c = 4) the parity-perfect triangle target Π(−q,−q,−q) lies in the ancestral-independence feasible set of the triangle module at every order t for q = 1/(16t) (triangle_linear_witness). Everything here is proved.

The triangle witness of Theorem thm:trianglelinear

The auxiliary development behind triangle_linear_witness: the copied observations A^{ij} = x_i z_j, B^{ik} = x_i y_k, C^{jk} = z_j y_k as exclusive ors of the auxiliary signs, the pushforward of triDensity along them, and the boundary computation of Lemma lem:boundary. Every character prescribed by the diagonal law, by an injectable marginal or by an ancestral-independence product has a boundary that is empty or meets two sign families, so the correction of triCoeff never reaches it and triW_moment returns the target value (−q)^{|∂|/2}.

Signs and Walsh characters

theorem TriangleInflation.Graph.TriWitnessAux.sgn_xor (a b : Bool) : sgn (a ^^ b) = sgn a * sgn b

The sign of an exclusive or is the product of the signs.

Pushforwards

theorem TriangleInflation.Graph.TriWitnessAux.sum_mul_pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (w : α → ℝ) (F : α → β) (f : β → ℝ) : ∑ b : β, f b * pushforward w F b = ∑ a : α, f (F a) * w a

theorem TriangleInflation.Graph.TriWitnessAux.pushforward_isLaw {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] {w : α → ℝ} (h : IsLaw w) (F : α → β) : IsLaw (pushforward w F)

theorem TriangleInflation.Graph.TriWitnessAux.funext_of_walsh_moments_equiv {α : Type u_1} [Fintype α] {ι : Type u_2} [Finite ι] (e : α ≃ (ι → Bool)) (P Q : α → ℝ) (h : ∀ (S : Finset ι), ∑ a : α, walsh S (e a) * P a = ∑ a : α, walsh S (e a) * Q a) : P = Q

Fourier uniqueness transported along an identification of a finite type with a sign cube.

The copied observations of the triangle witness

def TriangleInflation.Graph.TriWitnessAux.latSign {t : ℕ} : Latent t → TriSign t

The auxiliary sign coordinate of a copied latent variable: X_i ↦ (0,i), Z_j ↦ (1,j), Y_k ↦ (2,k).

Equations

• TriangleInflation.Graph.TriWitnessAux.latSign (TriangleInflation.Latent.X i) = (0, i)
• TriangleInflation.Graph.TriWitnessAux.latSign (TriangleInflation.Latent.Z j) = (1, j)
• TriangleInflation.Graph.TriWitnessAux.latSign (TriangleInflation.Latent.Y k) = (2, k)

theorem TriangleInflation.Graph.TriWitnessAux.latSign_injective {t : ℕ} : Function.Injective latSign

def TriangleInflation.Graph.TriWitnessAux.triObs {t : ℕ} (s : TriSign t → Bool) : Assign t

The copied observations of the witness: A^{ij} = x_i z_j, B^{ik} = x_i y_k, C^{jk} = z_j y_k, written as exclusive ors of the auxiliary signs.

Equations

• TriangleInflation.Graph.TriWitnessAux.triObs s (TriangleInflation.Obs.A i j) = (s (0, i) ^^ s (1, j))
• TriangleInflation.Graph.TriWitnessAux.triObs s (TriangleInflation.Obs.B i k) = (s (0, i) ^^ s (2, k))
• TriangleInflation.Graph.TriWitnessAux.triObs s (TriangleInflation.Obs.C j k) = (s (1, j) ^^ s (2, k))

Moments of the density and of the target

theorem TriangleInflation.Graph.TriWitnessAux.triDensity_moment (t : ℕ) (q : ℝ) (hq : 0 ≤ q) (S : Finset (TriSign t)) : ∑ s : TriSign t → Bool, walsh S s * triDensity t q s = triCoeff S * triMom q S.card

Moments of the parity-perfect target.

theorem TriangleInflation.Graph.TriWitnessAux.triParity_mom0 (q : ℝ) : ∑ w : ThreeBit, triParity q w = 1

theorem TriangleInflation.Graph.TriWitnessAux.triParity_momA (q : ℝ) : ∑ w : ThreeBit, sgn w.1 * triParity q w = -q

theorem TriangleInflation.Graph.TriWitnessAux.triParity_momB (q : ℝ) : ∑ w : ThreeBit, sgn w.2.1 * triParity q w = -q

theorem TriangleInflation.Graph.TriWitnessAux.triParity_momC (q : ℝ) : ∑ w : ThreeBit, sgn w.2.2 * triParity q w = -q

theorem TriangleInflation.Graph.TriWitnessAux.triParity_momAB (q : ℝ) : ∑ w : ThreeBit, sgn w.1 * sgn w.2.1 * triParity q w = -q

theorem TriangleInflation.Graph.TriWitnessAux.triParity_momAC (q : ℝ) : ∑ w : ThreeBit, sgn w.1 * sgn w.2.2 * triParity q w = -q

theorem TriangleInflation.Graph.TriWitnessAux.triParity_momBC (q : ℝ) : ∑ w : ThreeBit, sgn w.2.1 * sgn w.2.2 * triParity q w = -q

theorem TriangleInflation.Graph.TriWitnessAux.triParity_momABC (q : ℝ) : ∑ w : ThreeBit, sgn w.1 * sgn w.2.1 * sgn w.2.2 * triParity q w = 1

The boundary of an injectable block

theorem TriangleInflation.Graph.TriWitnessAux.walsh_pair {ι : Type u_1} [DecidableEq ι] {v w : ι} (h : v ≠ w) (s : ι → Bool) : walsh {v, w} s = sgn (s v) * sgn (s w)

theorem TriangleInflation.Graph.TriWitnessAux.pair_ne {t : ℕ} {v w : TriSign t} (h : v.1 ≠ w.1) : v ≠ w

theorem TriangleInflation.Graph.TriWitnessAux.pair_card {t : ℕ} {v w : TriSign t} (h : v.1 ≠ w.1) : {v, w}.card = 2

theorem TriangleInflation.Graph.TriWitnessAux.pair_fam {t : ℕ} {v w : TriSign t} (h : v.1 ≠ w.1) : ∃ a ∈ {v, w}, ∃ b ∈ {v, w}, a.1 ≠ b.1

theorem TriangleInflation.Graph.TriWitnessAux.triMom_two (q : ℝ) : triMom q 2 = -q

theorem TriangleInflation.Graph.TriWitnessAux.triMom_zero (q : ℝ) : triMom q 0 = 1

theorem TriangleInflation.Graph.TriWitnessAux.subset_triple {α : Type u_1} [DecidableEq α] {U : Finset α} {a b c : α} (h : U ⊆ {a, b, c}) : U = ∅ ∨ U = {a} ∨ U = {b} ∨ U = {c} ∨ U = {a, b} ∨ U = {a, c} ∨ U = {b, c} ∨ U = {a, b, c}

A subset of a three-element set is one of eight explicit sets.

noncomputable def TriangleInflation.Graph.TriWitnessAux.tgt {t : ℕ} (q : ℝ) (U : Finset (Obs t)) : ℝ

The moment that the parity-perfect target prescribes for a set of copied observations.

Equations

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

theorem TriangleInflation.Graph.TriWitnessAux.block_boundary {t : ℕ} (q : ℝ) (i j k : Fin t) (U : Finset (Obs t)) (hU : U ⊆ copiedTriangle i j k) : ∃ (B : Finset (TriSign t)), (∀ (s : TriSign t → Bool), ∏ u ∈ U, sgn (triObs s u) = walsh B s) ∧ B ⊆ Finset.image latSign (ancestorsOf U) ∧ B.card % 2 = 0 ∧ (B = ∅ ∨ ∃ a ∈ B, ∃ b ∈ B, a.1 ≠ b.1) ∧ triMom q B.card = tgt q U

The boundary of a subset of a copied triangle: an explicit set of auxiliary signs that carries the character of the subset, lies inside the image of its copied ancestry, has even cardinality, is empty or meets two families, and whose moment is the prescribed one.

The master character computation

theorem TriangleInflation.Graph.TriWitnessAux.triMom_add (q : ℝ) {a b : ℕ} (ha : a % 2 = 0) (hb : b % 2 = 0) : triMom q (a + b) = triMom q a * triMom q b

theorem TriangleInflation.Graph.TriWitnessAux.triMom_sum {ι : Type u_1} (q : ℝ) (s : Finset ι) (c : ι → ℕ) (h : ∀ m ∈ s, c m % 2 = 0) : triMom q (∑ m ∈ s, c m) = ∏ m ∈ s, triMom q (c m)

theorem TriangleInflation.Graph.TriWitnessAux.triCoeff_eq_one {t : ℕ} (B : Finset (TriSign t)) (h : B = ∅ ∨ ∃ a ∈ B, ∃ b ∈ B, a.1 ≠ b.1) : triCoeff B = 1

noncomputable def TriangleInflation.Graph.TriWitnessAux.triGamma (t : ℕ) (q : ℝ) : Assign t → ℝ

The witness law on the copied observations: the pushforward of the corrected density along A^{ij} = x_i z_j, B^{ik} = x_i y_k, C^{jk} = z_j y_k.

Equations

• TriangleInflation.Graph.TriWitnessAux.triGamma t q = TriangleInflation.pushforward (TriangleInflation.Graph.triDensity t q) TriangleInflation.Graph.TriWitnessAux.triObs

theorem TriangleInflation.Graph.TriWitnessAux.master1 {t : ℕ} (q : ℝ) (hq : 0 ≤ q) (i j k : Fin t) (U : Finset (Obs t)) (hU : U ⊆ copiedTriangle i j k) : ∑ s : TriSign t → Bool, (∏ u ∈ U, sgn (triObs s u)) * triDensity t q s = tgt q U

One injectable block: the character of any subset of a copied triangle has the moment that the parity-perfect target prescribes.

theorem TriangleInflation.Graph.TriWitnessAux.master {t : ℕ} (q : ℝ) (hq : 0 ≤ q) {n : ℕ} (S : Fin n → Finset (Obs t)) (hinj : ∀ (m : Fin n), Injectable (S m)) (hindep : ∀ (m m' : Fin n), m ≠ m' → AncestrallyIndependent (S m) (S m')) (U : Fin n → Finset (Obs t)) (hUS : ∀ (m : Fin n), U m ⊆ S m) : ∑ s : TriSign t → Bool, (∏ m : Fin n, ∏ u ∈ U m, sgn (triObs s u)) * triDensity t q s = ∏ m : Fin n, tgt q (U m)

Pairwise ancestrally independent injectable blocks: the joint character factorizes into the prescribed moments.

Symmetry of the witness

def TriangleInflation.Graph.TriWitnessAux.famPerm {t : ℕ} (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) : Fin 3 → Equiv.Perm (Fin t)

The permutation of copy indices attached to a sign family.

Equations

• TriangleInflation.Graph.TriWitnessAux.famPerm π g = if g = 0 then π.1 else if g = 1 then π.2.1 else π.2.2

def TriangleInflation.Graph.TriWitnessAux.signPerm {t : ℕ} (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) : Equiv.Perm (TriSign t)

The induced permutation of the auxiliary signs.

Equations

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

def TriangleInflation.Graph.TriWitnessAux.signPermFun {t : ℕ} (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) : (TriSign t → Bool) ≃ (TriSign t → Bool)

Relabelling the auxiliary signs, as a permutation of sign assignments.

Equations

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

def TriangleInflation.Graph.TriWitnessAux.obsPerm {t : ℕ} (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) : Equiv.Perm (Obs t)

The relabelling of copied observations, as a permutation.

Equations

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

theorem TriangleInflation.Graph.TriWitnessAux.relabel_injective {t : ℕ} (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) : Function.Injective (relabel π)

theorem TriangleInflation.Graph.TriWitnessAux.triFactor_perm (t : ℕ) (q : ℝ) (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) (s : TriSign t → Bool) (g : Fin 3) : triFactor t q (fun (v : TriSign t) => s ((signPerm π) v)) g = triFactor t q s g

theorem TriangleInflation.Graph.TriWitnessAux.triDensity_perm (t : ℕ) (q : ℝ) (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) (s : TriSign t → Bool) : (triDensity t q fun (v : TriSign t) => s ((signPerm π) v)) = triDensity t q s

theorem TriangleInflation.Graph.TriWitnessAux.triObs_perm (t : ℕ) (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) (s : TriSign t → Bool) : (triObs fun (v : TriSign t) => s ((signPerm π) v)) = relabel π (triObs s)

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

theorem TriangleInflation.Graph.TriWitnessAux.triGamma_symmetric (t : ℕ) (q : ℝ) : SymmetricLaw t (triGamma t q)

The injectable marginals

theorem TriangleInflation.Graph.TriWitnessAux.triGamma_injectable (t : ℕ) (q : ℝ) (hq : 0 ≤ q) : InjectableMarginals t (triGamma t q) (triParity q)

The ancestral-independence products

def TriangleInflation.Graph.TriWitnessAux.sigmaFun {n : ℕ} (β : Fin n → Type) : ((m : Fin n) → β m → Bool) ≃ ((m : Fin n) × β m → Bool)

Uncurrying a family of sign assignments.

Equations

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

theorem TriangleInflation.Graph.TriWitnessAux.triGamma_ancestral (t : ℕ) (q : ℝ) (hq : 0 ≤ q) : AncestralProducts t (triGamma t q) (triParity q)

The diagonal law

def TriangleInflation.Graph.TriWitnessAux.bitOf : Fin 3 → ThreeBit → Bool

The bit that the g-th party reads off a three-bit outcome.

Equations

• TriangleInflation.Graph.TriWitnessAux.bitOf g w = if g = 0 then w.1 else if g = 1 then w.2.1 else w.2.2

def TriangleInflation.Graph.TriWitnessAux.obsDiag {t : ℕ} (l : Fin t) (g : Fin 3) : Obs t

The g-th copied observation of the diagonal triangle Δ_{lll}.

Equations

• TriangleInflation.Graph.TriWitnessAux.obsDiag l g = if g = 0 then TriangleInflation.Obs.A l l else if g = 1 then TriangleInflation.Obs.B l l else TriangleInflation.Obs.C l l

def TriangleInflation.Graph.TriWitnessAux.flatD (t : ℕ) : (Fin t → ThreeBit) ≃ ((_ : Fin t) × Fin 3 → Bool)

The three diagonal outcomes, flattened into signs.

Equations

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

theorem TriangleInflation.Graph.TriWitnessAux.obsDiag_mem {t : ℕ} (l : Fin t) (g : Fin 3) : obsDiag l g ∈ copiedTriangle l l l

theorem TriangleInflation.Graph.TriWitnessAux.obsDiag_injective {t : ℕ} (l : Fin t) : Function.Injective (obsDiag l)

theorem TriangleInflation.Graph.TriWitnessAux.flatD_readDiagonal {t : ℕ} (ω : Assign t) (x : (_ : Fin t) × Fin 3) : (flatD t) (readDiagonal ω) x = ω (obsDiag x.fst x.snd)

theorem TriangleInflation.Graph.TriWitnessAux.partyBit_obsDiag {t : ℕ} (l : Fin t) (g : Fin 3) (w : ThreeBit) : partyBit (obsDiag l g).party w = bitOf g w

theorem TriangleInflation.Graph.TriWitnessAux.diagonalTriangle_indep {t : ℕ} {l l' : Fin t} (h : l ≠ l') : AncestrallyIndependent (diagonalTriangle l) (diagonalTriangle l')

theorem TriangleInflation.Graph.TriWitnessAux.triGamma_diagonal (t : ℕ) (q : ℝ) (hq : 0 ≤ q) : pushforward (triGamma t q) readDiagonal = tensorPow t (triParity q)

theorem TriangleInflation.Graph.triangle_linear_witness (t : ℕ) (ht : 1 ≤ t) (q : ℝ) (hq : q = 1 / (16 * ↑t)) : AIFeasible t (triParity q)

AUDIT-NOTES B2(ii), stated in the triangle types of TriangleInflation so that it can be proved against the existing definitions. With the m = 3, c = 4 density (W ≥ 3/5 for tq ≤ 1/16) and A^{ij} = x_i z_j, B^{ik} = x_i y_k, C^{jk} = z_j y_k, the parity-perfect target Π(−q,−q,−q) lies in I^AI_t for q = 1/(16t).

AUDIT-NOTES records this as a new consequence, not claimed in the packet, which "MUST be confirmed by the exact checker at t = 1, 2, 3 (positivity of every atom of the witness, symmetry, full diagonal law, all AI character equalities) before it enters the paper".