Honest hiding checks on every parsed-answer label #
The adjacent Hide and terminal Hide/Read edges use the actual adaptive operators on the common register/source space. Both ordered orientations commute, and every rejected answer pair has zero operator product. Wrong constructors are retained as zero effects throughout.
theorem
MIPRE.Introspection.Honest.parsedHide_next_commute
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
(w : Bool)
(k : ℕ)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
:
Commute (parsedHideOp L D R w k h a) (parsedHideOp L D R w (k + 1) h b)
Consecutive hiding levels commute for all parsed labels, including wrong constructors.
theorem
MIPRE.Introspection.Honest.parsedHide_next_commute_reversed
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
(w : Bool)
(k : ℕ)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
:
Commute (parsedHideOp L D R w (k + 1) h a) (parsedHideOp L D R w k h b)
theorem
MIPRE.Introspection.Honest.parsedHide_read_commute
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
(w : Bool)
(k : ℕ)
(hk : ℓ ≤ k + 1)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
:
Commute (parsedHideOp L D R w k h a) (parsedReadOp L D R w h b)
The terminal hiding level commutes with the full Read measurement and its source answer.
theorem
MIPRE.Introspection.Honest.parsedRead_hide_commute
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
(w : Bool)
(k : ℕ)
(hk : ℓ ≤ k + 1)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
:
Commute (parsedReadOp L D R w h a) (parsedHideOp L D R w k h b)
theorem
MIPRE.Introspection.Honest.aux_check_swap
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
{P : Type u_5}
(X Z : P)
(projectPauli : PA → ι → F)
(DP : P → P → PA → PA → Bool)
(t u : AuxType ℓ × Bool)
(a b : ParsedAnswer (ι → F) A PA)
:
TypedPredicate.check L X Z projectPauli D DP (Sum.inr t) (Sum.inr u) a b = TypedPredicate.check L X Z projectPauli D DP (Sum.inr u) (Sum.inr t) b a
theorem
MIPRE.Introspection.Honest.hide_next_check
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
{P : Type u_5}
(X Z : P)
(projectPauli : PA → ι → F)
(DP : P → P → PA → PA → Bool)
(w : Bool)
(k j : Fin ℓ)
(hk : ↑k + 1 = ↑j)
(a b : HideLabel F ι)
:
TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.hide j, w))
(ParsedAnswer.hide a.1 a.2.1 a.2.2) (ParsedAnswer.hide b.1 b.2.1 b.2.2) = decide (CLChecks.hidingNext (L w) (↑k) a b)
theorem
MIPRE.Introspection.Honest.hide_read_check
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
{P : Type u_5}
(X Z : P)
(projectPauli : PA → ι → F)
(DP : P → P → PA → PA → Bool)
(w : Bool)
(k : Fin ℓ)
(hk : ↑k + 1 = ℓ)
(a : HideLabel F ι)
(b : ReadLabel F ι × A)
:
TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.read, w))
(ParsedAnswer.hide a.1 a.2.1 a.2.2) (ParsedAnswer.read b.1.1 b.1.2 b.2) = decide (CLChecks.hidingRead (L w) a (b.1.1, b.1.2, b.2))
theorem
MIPRE.Introspection.Honest.parsedHide_next_reject_zero
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
{P : Type u_5}
(X Z : P)
(projectPauli : PA → ι → F)
(DP : P → P → PA → PA → Bool)
(w : Bool)
(k j : Fin ℓ)
(hk : ↑k + 1 = ↑j)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
(hr :
TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.hide j, w)) a b = false)
:
Rejection by the actual adjacent-Hide predicate annihilates the honest full-space product.
theorem
MIPRE.Introspection.Honest.parsedHide_next_reject_zero_reversed
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
{P : Type u_5}
(X Z : P)
(projectPauli : PA → ι → F)
(DP : P → P → PA → PA → Bool)
(w : Bool)
(k j : Fin ℓ)
(hk : ↑k + 1 = ↑j)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
(hr :
TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.hide j, w)) (Sum.inr (AuxType.hide k, w)) a b = false)
:
theorem
MIPRE.Introspection.Honest.parsedHide_read_reject_zero
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
{P : Type u_5}
(X Z : P)
(projectPauli : PA → ι → F)
(DP : P → P → PA → PA → Bool)
(w : Bool)
(k : Fin ℓ)
(hk : ↑k + 1 = ℓ)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
(hr :
TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.read, w)) a b = false)
:
Rejection by the terminal Hide/Read predicate annihilates the actual operator product.
theorem
MIPRE.Introspection.Honest.parsedRead_hide_reject_zero
{F : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{PA : Type u_4}
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PA]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(D : (ι → F) → (ι → F) → A → A → Bool)
(R : SyncStrategy (sourceGame L D).doubled)
{P : Type u_5}
(X Z : P)
(projectPauli : PA → ι → F)
(DP : P → P → PA → PA → Bool)
(w : Bool)
(k : Fin ℓ)
(hk : ↑k + 1 = ℓ)
(h : (L w).SupportedOn Finset.univ)
(a b : ParsedAnswer (ι → F) A PA)
(hr :
TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.read, w)) (Sum.inr (AuxType.hide k, w)) a b = false)
: