Exact recursion of the honest hiding checks

Adding one common local Z/dual outcome to two supported continuation answers preserves the actual parsed hiding predicate. These are identities for the source checks, including the later-answer choice of adaptive registers.

theorem MIPRE.Introspection.Honest.supported_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {V : Finset ι} {y : ι → F} (hy : (CL.proj V) y = y) {i : ι} (hi : i ∉ V) : y i = 0

theorem MIPRE.Introspection.Honest.proj_local_add {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S V : Finset ι} (z : Fin (Fintype.card ↥S) → F) (y : ι → F) (hy : (CL.proj (V \ S)) y = y) : (CL.proj S) ((coordinateInsert S) z + y) = (coordinateInsert S) z ∧ (CL.proj Sᶜ) ((coordinateInsert S) z + y) = y

The common local component and the supported tail are recovered by projection.

theorem MIPRE.Introspection.Honest.proj_tail_local_add {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S V T : Finset ι} (hT : T ⊆ V \ S) (z : Fin (Fintype.card ↥S) → F) (y : ι → F) : (CL.proj T) ((coordinateInsert S) z + y) = (CL.proj T) y

theorem MIPRE.Introspection.Honest.proj_union_local_add {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S V T : Finset ι} (hT : T ⊆ V \ S) (z : Fin (Fintype.card ↥S) → F) (y : ι → F) (hy : (CL.proj (V \ S)) y = y) : (CL.proj (S ∪ T)) ((coordinateInsert S) z + y) = (coordinateInsert S) z + (CL.proj T) y

theorem MIPRE.Introspection.Honest.proj_union_compl_tail {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S V T : Finset ι} (y : ι → F) (hy : (CL.proj (V \ S)) y = y) : (CL.proj (S ∪ T)ᶜ) y = (CL.proj Tᶜ) y

theorem MIPRE.Introspection.Honest.factorOfPrefix_subset {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {V : Finset ι} (h : P.SupportedOn V) (k : ℕ) (y : ι → F) : P.factorOfPrefix k y ⊆ V

theorem MIPRE.Introspection.Honest.outputPrefix_local_add {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (k : ℕ) (z : Fin (Fintype.card ↥S) → F) (y : ι → F) (hy : (CL.proj (V \ S)) y = y) : (CL.CLFun.cons S L next).outputPrefix (k + 1) ((coordinateInsert S) z + y) = (coordinateInsert S) z + (next ((coordinateInsert S) z)).outputPrefix k y

Claimed prefixes follow the tail continuation chosen by the common local Z value.

theorem MIPRE.Introspection.Honest.prefixRegister_local_add {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (k : ℕ) (z : Fin (Fintype.card ↥S) → F) (y : ι → F) (hy : (CL.proj (V \ S)) y = y) : CLChecks.prefixRegister (CL.CLFun.cons S L next) (k + 1) ((coordinateInsert S) z + y) = S ∪ CLChecks.prefixRegister (next ((coordinateInsert S) z)) k y

theorem MIPRE.Introspection.Honest.hidingNext_join {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (h : (CL.CLFun.cons S L next).SupportedOn V) (k : ℕ) (z : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (u v : HideLabel F ι) (hu : (CL.proj (V \ S)) u.1 = u.1 ∧ (CL.proj (V \ S)) u.2.1 = u.2.1 ∧ (CL.proj (V \ S)) u.2.2 = u.2.2) (hv : (CL.proj (V \ S)) v.1 = v.1 ∧ (CL.proj (V \ S)) v.2.1 = v.2.1 ∧ (CL.proj (V \ S)) v.2.2 = v.2.2) (ht : CLChecks.hidingNext (next ((coordinateInsert S) z.1)) k u v) : CLChecks.hidingNext (CL.CLFun.cons S L next) (k + 1) (joinHide S (z, u)) (joinHide S (z, v))

The adjacent-hiding check lifts through an actual common adaptive local outcome.

theorem MIPRE.Introspection.Honest.hidingRead_join {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (hℓ : 0 < ℓ) (z : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (u : HideLabel F ι) (v : ReadLabel F ι) (a : A) (hu : (CL.proj (V \ S)) u.1 = u.1) (hv : (CL.proj (V \ S)) v.1 = v.1) (ht : CLChecks.hidingRead (next ((coordinateInsert S) z.1)) u (v.1, v.2, a)) : CLChecks.hidingRead (CL.CLFun.cons S L next) (joinHide S (z, u)) ((joinRead S (z, v)).1, (joinRead S (z, v)).2, a)

The terminal hiding/Read check lifts through a common local outcome. The continuation has positive depth, as required when a terminal hiding level is itself recursively inside the tail.

theorem MIPRE.Introspection.Honest.hidingNext_stop_join {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (h : (CL.CLFun.cons S L next).SupportedOn V) (z : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (x : ↥(V \ S) → F) : CLChecks.hidingNext (CL.CLFun.cons S L next) 0 (stopLabel S V (z.2, x)) (joinHide S (z, stopHideAnswer (next ((coordinateInsert S) z.1)) (V \ S) x))

The first adjacent hiding check holds on the exact common X-tail labels appearing in the stopping measurement and its next adaptive refinement.