Perfect PCC play of the full Pauli basis game

All question types use the actual honest field-register measurements and a single extra qubit. The sampler's support supplies one common content for both questions; every graph edge is handled, including its reverse and every self-loop. Wrong-format answers retain zero effects throughout.

theorem MIPRE.QLD.Honest.pairTest_reverse {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (a b : Answer F m d) : pairTest hm x y a b = pairTest hm y x b a

theorem MIPRE.QLD.Honest.accepts_reverse {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (a b : Answer F m d) : accepts hm x y a b = accepts hm y x b a

theorem MIPRE.QLD.Honest.qldGame_positive_content {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (h : 0 < (qldGame hm).μ x y) : ∃ (c : Content F m) (t : Ty) (u : Ty), adj t u = true ∧ x = Content.question hm c t ∧ y = Content.question hm c u

Every positive-probability question pair comes from one actual content and an adjacent ordered pair of types.

theorem MIPRE.QLD.Honest.answerOp_self_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (q : Question F m) (a b : Answer F m d) : Commute (answerOp hm q a) (answerOp hm q b)

Same-question effects commute, including zero effects of malformed answers.

theorem MIPRE.QLD.Honest.answerOp_self_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (q : Question F m) (a b : Answer F m d) (hr : accepts hm q q a b = false) : answerOp hm q a * answerOp hm q b = 0

The actual self-loop rejects only products that vanish.

theorem MIPRE.QLD.Honest.adjRaw_cases (t u : Ty) (h : adjRaw t u = true) : (∃ (W : Bas), t = Ty.aline W ∧ u = Ty.point W) ∨ (∃ (W : Bas), t = Ty.dline W ∧ u = Ty.point W) ∨ (∃ (W : Bas), t = Ty.point W ∧ u = Ty.pauli W) ∨ (∃ (W : Bas), t = Ty.point W ∧ u = Ty.pairB W) ∨ (∃ (W : Bas), t = Ty.pairB W ∧ u = Ty.pair) ∨ (∃ (W : Bas), t = Ty.point W ∧ u = Ty.var (distinguished W)) ∨ ∃ (i : Fin LCS.MagicSquare.layout.r) (j : Fin LCS.MagicSquare.layout.s), t = Ty.con i ∧ u = Ty.var j ∧ j ∈ LCS.MagicSquare.layout.V i

theorem MIPRE.QLD.Honest.answerOp_adjRaw_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (c : Content F m) (t u : Ty) (h : adjRaw t u = true) (a b : Answer F m d) : Commute (answerOp hm (Content.question hm c t) a) (answerOp hm (Content.question hm c u) b)

Commutation on every forward non-loop type-graph edge.

theorem MIPRE.QLD.Honest.answerOp_adjRaw_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (c : Content F m) (t u : Ty) (h : adjRaw t u = true) (a b : Answer F m d) (hr : accepts hm (Content.question hm c t) (Content.question hm c u) a b = false) : answerOp hm (Content.question hm c t) a * answerOp hm (Content.question hm c u) b = 0

Rejected effects vanish on every forward non-loop edge.

theorem MIPRE.QLD.Honest.answerOp_sampled_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (c : Content F m) (t u : Ty) (h : adj t u = true) (a b : Answer F m d) : Commute (answerOp hm (Content.question hm c t) a) (answerOp hm (Content.question hm c u) b)

Every sampled edge, including reverse edges and self-loops, commutes.

theorem MIPRE.QLD.Honest.answerOp_sampled_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (c : Content F m) (t u : Ty) (h : adj t u = true) (a b : Answer F m d) (hr : accepts hm (Content.question hm c t) (Content.question hm c u) a b = false) : answerOp hm (Content.question hm c t) a * answerOp hm (Content.question hm c u) b = 0

Every rejected outcome pair on the sampler's support has zero product.

theorem MIPRE.QLD.Honest.answerOp_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (h : 0 < (qldGame hm).μ x y) (a b : Answer F m d) : Commute (answerOp hm x a) (answerOp hm y b)

Commutation on the actual question distribution, without replacing it by a type-only support condition.

theorem MIPRE.QLD.Honest.answerOp_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (x y : Question F m) (h : 0 < (qldGame hm).μ x y) (a b : Answer F m d) (hr : (qldGame hm).D x y a b = false) : answerOp hm x a * answerOp hm y b = 0

The actual Pauli-game predicate vanishes on every rejected honest product.

noncomputable def MIPRE.QLD.Honest.strategy {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) : SyncStrategy (qldGame hm).doubled

One honest finite-dimensional strategy for all twenty-six question types.

Equations

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

theorem MIPRE.QLD.Honest.doubled_positive {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (p q : Bool × Question F m) (h : 0 < (qldGame hm).doubled.μ p q) : (p.1 = false ∧ q.1 = true) ∧ 0 < (qldGame hm).μ p.2 q.2

theorem MIPRE.QLD.Honest.strategy_isPCC {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) : (strategy hm).IsPCC

theorem MIPRE.QLD.Honest.strategy_value {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) : (strategy hm).value = 1

theorem MIPRE.QLD.Honest.exists_perfectPCC {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) : ∃ (S : SyncStrategy (qldGame hm).doubled), S.IsPCC ∧ S.value = 1 ∧ S.d = 2 * Fintype.card (Register F m)

The actual Pauli basis game has a perfect PCC strategy, using its field register and one additional qubit.