Completeness of the associated test (Theorem I:2126 (1))

A perfect Z-aligned permutation strategy of g gives an action of value 1 on the associated test (exists_value_one_of_hasPerfectZPC). A signed permutation s of Fin m is a permutation liftSP s of Bool × Fin m, (b, j) ↦ (b ⊕ s_j, s(j)), multiplicatively; the action lets the generator J act as the lift of -1 and X(x, i) as the lift of the signed permutation of U x i, on Fin (2m) ≃ Bool × Fin m. It passes Checks 1–3, and a point (b, j) passes the challenge at (x, y) when every constraint word of the readable class of j fixes (b, j): when the matrix of the word has 1 at (j, j). The trace identity at value 1 gives exactly this for the pairs of positive weight (consMat_apply_self_eq_one). Commutation along edges is not used.

Lifting signed permutations

def MIPRE.Tailored.Sofic.liftSP {Ω : Type u_1} (s : SignedPerm Ω) : Equiv.Perm (Bool × Ω)

A signed permutation of Ω as a permutation of Bool × Ω.

Equations

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

@[simp]

theorem MIPRE.Tailored.Sofic.liftSP_apply {Ω : Type u_1} (s : SignedPerm Ω) (b : Bool) (j : Ω) : (liftSP s) (b, j) = (b ^^ s.sign j, s.perm j)

theorem MIPRE.Tailored.Sofic.liftSP_mul {Ω : Type u_1} (s t : SignedPerm Ω) : liftSP (s * t) = liftSP s * liftSP t

theorem MIPRE.Tailored.Sofic.liftSP_one {Ω : Type u_1} : liftSP 1 = 1

def MIPRE.Tailored.Sofic.liftHom {Ω : Type u_1} {N : ℕ} (e : Bool × Ω ≃ Fin N) : SignedPerm Ω →* Equiv.Perm (Fin N)

The lift as a homomorphism to the permutations of Fin N, along e.

Equations

• MIPRE.Tailored.Sofic.liftHom e = { toFun := fun (s : MIPRE.Tailored.SignedPerm Ω) => e.permCongr (MIPRE.Tailored.Sofic.liftSP s), map_one' := ⋯, map_mul' := ⋯ }

theorem MIPRE.Tailored.Sofic.liftHom_apply {Ω : Type u_1} {N : ℕ} (e : Bool × Ω ≃ Fin N) (s : SignedPerm Ω) (b : Bool) (j : Ω) : ((liftHom e) s) (e (b, j)) = e (b ^^ s.sign j, s.perm j)

theorem MIPRE.Tailored.Sofic.liftHom_fix_iff {Ω : Type u_1} {N : ℕ} (e : Bool × Ω ≃ Fin N) (s : SignedPerm Ω) (b : Bool) (j : Ω) : ((liftHom e) s) (e (b, j)) = e (b, j) ↔ s.perm j = j ∧ s.sign j = false

theorem MIPRE.Tailored.Sofic.negOne_mul_negOne {Ω : Type u_1} : SignedPerm.negOne * SignedPerm.negOne = 1

theorem MIPRE.Tailored.Sofic.re_half_one_sub_eq_zero {Ω : Type u_1} [DecidableEq Ω] (s : SignedPerm Ω) (j : Ω) (h : (1 / 2 * (1 - s.toMatrix j j)).re = 0) : s.perm j = j ∧ s.sign j = false

The action of a Z-aligned permutation strategy

noncomputable def MIPRE.Tailored.Sofic.ZStrat.spU {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : SignedPerm (Fin S.m)

The signed permutation of an observable.

Equations

• S.spU x i = Classical.choose ⋯

theorem MIPRE.Tailored.Sofic.ZStrat.toMatrix_spU {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : (S.spU x i).toMatrix = S.U x i

noncomputable def MIPRE.Tailored.Sofic.ZStrat.genSP {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (k : ℕ) : SignedPerm (Fin S.m)

The signed permutation of each generator: -1 for J, that of U x i for X(x, i).

Equations

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

theorem MIPRE.Tailored.Sofic.ZStrat.genSP_J {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : S.genSP genJ = SignedPerm.negOne

theorem MIPRE.Tailored.Sofic.ZStrat.genSP_X {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : S.genSP (genX g ↑x ↑i) = S.spU x i

theorem MIPRE.Tailored.Sofic.ZStrat.genSP_of_ge {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (k : ℕ) (hk : nGen g ≤ k) : S.genSP k = 1

theorem MIPRE.Tailored.Sofic.ZStrat.toMatrix_genSP_X {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (z : Fin (g.nV + 1)) (i : ℕ) (hi : i < g.lenAt ↑z) : (S.genSP (genX g (↑z) i)).toMatrix = S.Unat z i

theorem MIPRE.Tailored.Sofic.ZStrat.spU_mul_self {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : S.spU x i * S.spU x i = 1

theorem MIPRE.Tailored.Sofic.ZStrat.spU_comm {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i j : Fin g.ansLen) : S.spU x i * S.spU x j = S.spU x j * S.spU x i

theorem MIPRE.Tailored.Sofic.ZStrat.spU_perm {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) (hi : ↑i < g.lenRAt ↑x) : (S.spU x i).perm = 1

def MIPRE.Tailored.Sofic.ZStrat.ptEquiv (m : ℕ) : Bool × Fin m ≃ Fin (2 * m)

The points Bool × Fin m as Fin (2m).

Equations

• MIPRE.Tailored.Sofic.ZStrat.ptEquiv m = (finTwoEquiv.symm.prodCongr (Equiv.refl (Fin m))).trans finProdFinEquiv

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Sofic.ZStrat.toAction {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : SubgroupTestValue.FiniteAction (nGen g)

The action of a Z-aligned permutation strategy.

Equations

• S.toAction = { N := 2 * S.m, N_pos := ⋯, σ := fun (k : Fin (MIPRE.Tailored.Sofic.nGen g)) => (MIPRE.Tailored.Sofic.liftHom (MIPRE.Tailored.Sofic.ZStrat.ptEquiv S.m)) (S.genSP ↑k) }

theorem MIPRE.Tailored.Sofic.ZStrat.genPerm_toAction {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (k : ℕ) : genPerm S.toAction k = (liftHom (ptEquiv S.m)) (S.genSP k)

theorem MIPRE.Tailored.Sofic.ZStrat.wordPerm_toAction {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (w : SubgroupTestValue.Word) : S.toAction.wordPerm w = (liftHom (ptEquiv S.m)) (wordSP S.genSP w)

theorem MIPRE.Tailored.Sofic.ZStrat.exists_pt {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (p : Fin S.toAction.N) : ∃ (b : Bool) (j : Fin S.m), p = (ptEquiv S.m) (b, j)

theorem MIPRE.Tailored.Sofic.ZStrat.checks_toAction {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) : Checks g S.toAction

The action passes Checks 1–3.

theorem MIPRE.Tailored.Sofic.ZStrat.rbit_eq {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (i : ℕ) (hi : i < g.lenRAt ↑x) (j : Fin S.m) : S.rbit x i j = (S.genSP (genX g (↑x) i)).sign j

theorem MIPRE.Tailored.Sofic.ZStrat.rdv_toAction {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (b : Bool) (j : Fin S.m) : rdv S.toAction (↑x) (↑y) ((ptEquiv S.m) (b, j)) = S.rsgn x j ++ S.rsgn y j

theorem MIPRE.Tailored.Sofic.ZStrat.consMat_eq {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (c : List Bool) : S.consMat x y c = (wordSP S.genSP (consWord g (↑x) (↑y) c)).toMatrix

theorem MIPRE.Tailored.Sofic.ZStrat.consMat_apply_self_eq_one {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (hS : S.value = 1) (x y : Fin (g.nV + 1)) (hμ : 0 < g.toGame.μ x y) {e : ℕ × ℕ × List Bool × List Bool} (he : e ∈ consAt g ↑x ↑y) (j : Fin S.m) (hj : S.rsgn x j ++ S.rsgn y j = e.2.2.1) : (wordSP S.genSP (consWord g (↑x) (↑y) e.2.2.2)).perm j = j ∧ (wordSP S.genSP (consWord g (↑x) (↑y) e.2.2.2)).sign j = false

At value 1, every constraint word of a pair of positive weight has 1 on the diagonal of its readable class.

theorem MIPRE.Tailored.Sofic.exists_value_one_of_hasPerfectZPC (g : TailoredGameValue.TailoredGameData) (h : g.HasPerfectZPC) : ∃ (σ : SubgroupTestValue.FiniteAction (nGen g)), (assocTest g).value σ = 1

Completeness of the associated test (Theorem I:2126 (1)): a tailored game with a perfect Z-aligned permutation strategy (commuting along edges, which is not used) has an associated test of value 1.