The trace identity of a Z-aligned permutation strategy

The analytic heart of paper I's Proposition I:2279 and of the completeness of Theorem I:2126, by a trace identity in place of the paper's Fourier bases and orbit intersections (planning/aldous-lyons-track.md, A shorter route for the analytic heart).

For a Z-aligned permutation strategy S the readable observables at x are ±1 diagonals, so each basis point j carries readable signs rsgn x j, and the projection P_a vanishes outside the rows and columns whose readable signs are a's readable part (proj_apply_eq_zero_of_row, proj_apply_eq_zero_of_col). Hence, for any set G of readable values and any matrix X (sum_trace_proj_mul_mul_proj),

∑_{a, b : (a^R, b^R) ∈ G} Tr(P_a X Q_b) = ∑_{j : (rsgn x j, rsgn y j) ∈ G} X_{jj}.

A constraint c at (x, y) gives the matrix consMat c = (-1)^{c_J} U^α V^β (or -1 for a constraint of the wrong length), and P_a consMat Q_b = (-1)^{consBit} P_a Q_b, where consBit = false exactly when a b 1 satisfies c (proj_mul_consMat_mul_proj, satisfies_iff_consBit). So the violation of c is P_a (1 - consMat)/2 Q_b (ite_satisfies_smul), and its probability on a readable class is a sum of diagonal entries.

theorem MIPRE.Tailored.Sofic.lenAt_le_ansLen_fin (g : TailoredGameValue.TailoredGameData) (x : Fin (g.nV + 1)) : g.lenAt ↑x ≤ g.ansLen

theorem MIPRE.Tailored.Sofic.lenRAt_le_ansLen (g : TailoredGameValue.TailoredGameData) (x : Fin (g.nV + 1)) : g.lenRAt ↑x ≤ g.ansLen

Readable signs

noncomputable def MIPRE.Tailored.Sofic.ZStrat.rbit {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : ℕ) (j : Fin S.m) : Bool

The sign bit (true for -1) of the observable U x i at the basis point j, read on the diagonal.

Equations

• S.rbit x i j = if h : i < g.ansLen then decide (S.U x ⟨i, h⟩ j j = -1) else false

noncomputable def MIPRE.Tailored.Sofic.ZStrat.rsgn {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (j : Fin S.m) : List Bool

The readable signs at x of the basis point j.

Equations

• S.rsgn x j = List.map (fun (i : ℕ) => S.rbit x i j) (List.range (g.lenRAt ↑x))

theorem MIPRE.Tailored.Sofic.ZStrat.U_eq_diagonal {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) (hi : ↑i < g.lenRAt ↑x) : S.U x i = Matrix.diagonal fun (j : Fin S.m) => bitSign (S.rbit x (↑i) j)

A readable observable is the diagonal of its sign bits.

theorem MIPRE.Tailored.Sofic.ZStrat.readable_eq_rsgn_iff {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) (j : Fin S.m) : g.readable x a = S.rsgn x j ↔ ∀ (i : Fin g.ansLen), ↑i < g.lenRAt ↑x → a i = S.rbit x (↑i) j

theorem MIPRE.Tailored.Sofic.ZStrat.proj_apply_eq_zero_of_row {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) (j k : Fin S.m) (h : g.readable x a ≠ S.rsgn x j) : S.proj x a j k = 0

P_a vanishes on the rows whose readable signs are not a's.

theorem MIPRE.Tailored.Sofic.ZStrat.proj_apply_eq_zero_of_col {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) (j k : Fin S.m) (h : g.readable x a ≠ S.rsgn x k) : S.proj x a j k = 0

P_a vanishes on the columns whose readable signs are not a's.

The trace identity

theorem MIPRE.Tailored.Sofic.ZStrat.sum_trace_proj_mul_mul_proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (G : List Bool → Prop) [DecidablePred G] (X : Matrix (Fin S.m) (Fin S.m) ℂ) : (∑ a : Fin g.ansLen → Bool, ∑ b : Fin g.ansLen → Bool, if G (g.readable x a ++ g.readable y b) then (S.proj x a * X * S.proj y b).trace else 0) = ∑ j : Fin S.m, if G (S.rsgn x j ++ S.rsgn y j) then X j j else 0

The trace identity: for a set G of readable values and any matrix X, ∑_{a, b : (a^R, b^R) ∈ G} Tr(P_a X Q_b) = ∑_{j : (rsgn x j, rsgn y j) ∈ G} X_{jj}.

Constraints

def MIPRE.Tailored.Sofic.coefX (g : TailoredGameValue.TailoredGameData) (x : Fin (g.nV + 1)) (c : List Bool) : Fin g.ansLen → Bool

The coefficients of a constraint on the variables at x.

Equations

• MIPRE.Tailored.Sofic.coefX g x c i = (decide (↑i < g.lenAt ↑x) && c.getD (↑i) false)

def MIPRE.Tailored.Sofic.coefY (g : TailoredGameValue.TailoredGameData) (x y : Fin (g.nV + 1)) (c : List Bool) : Fin g.ansLen → Bool

The coefficients of a constraint on the variables at y.

Equations

• MIPRE.Tailored.Sofic.coefY g x y c i = (decide (↑i < g.lenAt ↑y) && c.getD (g.lenAt ↑x + ↑i) false)

def MIPRE.Tailored.Sofic.coefJ (g : TailoredGameValue.TailoredGameData) (x y : Fin (g.nV + 1)) (c : List Bool) : Bool

The coefficient of a constraint on J.

Equations

• MIPRE.Tailored.Sofic.coefJ g x y c = c.getD (g.lenAt ↑x + g.lenAt ↑y) false

def MIPRE.Tailored.Sofic.consBit (g : TailoredGameValue.TailoredGameData) (x y : Fin (g.nV + 1)) (c : List Bool) (a b : Fin g.ansLen → Bool) : Bool

The bit ⟨c, a b 1⟩ over F₂, true for a constraint of the wrong length, which is never satisfied.

Equations

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

theorem MIPRE.Tailored.Sofic.bitSign_eq_one_iff (b : Bool) : bitSign b = 1 ↔ b = false

theorem MIPRE.Tailored.Sofic.bitSign_dotBit {k : ℕ} (α a : Fin k → Bool) : bitSign (dotBit α a) = ∏ i : Fin k, bitSign (α i && a i)

theorem MIPRE.Tailored.Sofic.neg_one_pow_count_zipWith (c v : List Bool) (h : c.length = v.length) : (-1) ^ List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) c v) = ∏ i ∈ Finset.range c.length, bitSign (c.getD i false && v.getD i false)

theorem MIPRE.Tailored.Sofic.bitSign_dotBit_coefX {g : TailoredGameValue.TailoredGameData} (x : Fin (g.nV + 1)) (c : List Bool) (a : Fin g.ansLen → Bool) : bitSign (dotBit (coefX g x c) a) = ∏ i ∈ Finset.range (g.lenAt ↑x), bitSign (c.getD i false && TailoredGameValue.TailoredGameData.bit a i)

theorem MIPRE.Tailored.Sofic.bitSign_dotBit_coefY {g : TailoredGameValue.TailoredGameData} (x y : Fin (g.nV + 1)) (c : List Bool) (b : Fin g.ansLen → Bool) : bitSign (dotBit (coefY g x y c) b) = ∏ i ∈ Finset.range (g.lenAt ↑y), bitSign (c.getD (g.lenAt ↑x + i) false && TailoredGameValue.TailoredGameData.bit b i)

theorem MIPRE.Tailored.Sofic.length_full {g : TailoredGameValue.TailoredGameData} (z : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) : (g.full z a).length = g.lenAt ↑z

theorem MIPRE.Tailored.Sofic.getD_full {g : TailoredGameValue.TailoredGameData} (z : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) {i : ℕ} (hi : i < g.lenAt ↑z) : (g.full z a).getD i false = TailoredGameValue.TailoredGameData.bit a i

theorem MIPRE.Tailored.Sofic.getD_vec_left {g : TailoredGameValue.TailoredGameData} (x y : Fin (g.nV + 1)) (a b : Fin g.ansLen → Bool) {i : ℕ} (hi : i < g.lenAt ↑x) : (g.full x a ++ g.full y b ++ [true]).getD i false = TailoredGameValue.TailoredGameData.bit a i

theorem MIPRE.Tailored.Sofic.getD_vec_mid {g : TailoredGameValue.TailoredGameData} (x y : Fin (g.nV + 1)) (a b : Fin g.ansLen → Bool) {i : ℕ} (hi : i < g.lenAt ↑y) : (g.full x a ++ g.full y b ++ [true]).getD (g.lenAt ↑x + i) false = TailoredGameValue.TailoredGameData.bit b i

theorem MIPRE.Tailored.Sofic.getD_vec_last {g : TailoredGameValue.TailoredGameData} (x y : Fin (g.nV + 1)) (a b : Fin g.ansLen → Bool) : (g.full x a ++ g.full y b ++ [true]).getD (g.lenAt ↑x + g.lenAt ↑y) false = true

theorem MIPRE.Tailored.Sofic.satisfies_iff_consBit {g : TailoredGameValue.TailoredGameData} (x y : Fin (g.nV + 1)) (c : List Bool) (a b : Fin g.ansLen → Bool) : TailoredGameValue.TailoredGameData.Satisfies c (g.full x a ++ g.full y b ++ [true]) ↔ consBit g x y c a b = false

A constraint is satisfied exactly when its bit vanishes.

noncomputable def MIPRE.Tailored.Sofic.ZStrat.consMat {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (c : List Bool) : Matrix (Fin S.m) (Fin S.m) ℂ

The matrix (-1)^{c_J} U^α V^β of a constraint c at (x, y), or -1 for a constraint of the wrong length.

Equations

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

theorem MIPRE.Tailored.Sofic.ZStrat.proj_mul_obsChar {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (a α : Fin g.ansLen → Bool) : S.proj x a * obsChar (S.U x) α = bitSign (dotBit α a) • S.proj x a

P_a lies in the (-1)^{⟨α, a⟩}-eigenspace of U^α, on the right.

theorem MIPRE.Tailored.Sofic.ZStrat.proj_mul_consMat_mul_proj {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (c : List Bool) (a b : Fin g.ansLen → Bool) : S.proj x a * S.consMat x y c * S.proj y b = bitSign (consBit g x y c a b) • (S.proj x a * S.proj y b)

P_a consMat Q_b = (-1)^{⟨c, a b 1⟩} P_a Q_b.

theorem MIPRE.Tailored.Sofic.ZStrat.ite_satisfies_smul {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (c : List Bool) (a b : Fin g.ansLen → Bool) : (if TailoredGameValue.TailoredGameData.Satisfies c (g.full x a ++ g.full y b ++ [true]) then 0 else 1) • (S.proj x a * S.proj y b) = S.proj x a * (1 / 2) • (1 - S.consMat x y c) * S.proj y b

The violation of a constraint: [a b 1 violates c] P_a Q_b = P_a (1 - consMat)/2 Q_b.