Concrete ideal prefixes for honest hiding

The next Z prefix is a marginal of the adjacent honest hiding PVM. Thus its commutation with the preceding honest hiding family follows from the proved adjacent commutation, without a new commutation assumption.

def MIPRE.Introspection.Honest.hidingPrefixOp {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : Option (ι → F) → Matrix (ι → F) (ι → F) ℂ

The ideal prefix retains an explicit zero operator for malformed labels.

Equations

• MIPRE.Introspection.Honest.hidingPrefixOp P k = MIPRE.Introspection.readout fun (x : ι → F) => some ((MIPRE.CL.CLFun.truncate k P).eval x)

@[simp]

theorem MIPRE.Introspection.Honest.hidingPrefixOp_none {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : hidingPrefixOp P k none = 0

@[simp]

theorem MIPRE.Introspection.Honest.hidingPrefixOp_some {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : hidingPrefixOp P k (some y) = readout (CL.CLFun.truncate k P).eval y

theorem MIPRE.Introspection.Honest.hidingPrefixOp_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : IsPVM (hidingPrefixOp P k)

theorem MIPRE.Introspection.Honest.hidingPrefixOp_commute_hideOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (y : Option (ι → F)) (a : HideLabel F ι) : Commute (hidingPrefixOp P (k + 1) y) (hideOp P k h a)

The next ideal Z prefix commutes with every actual preceding honest Hide operator, including prefixes whose readout projector is zero.

theorem MIPRE.Introspection.Honest.hidingPrefixOp_commute_coarse {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) {J : Type u_3} [Fintype J] [DecidableEq J] (f : HideLabel F ι → J) (y : Option (ι → F)) (j : J) : Commute (hidingPrefixOp P (k + 1) y) (fibSum (hideOp P k h) f j)

The same explicit prefix commutes with any coarse family of the preceding honest hiding measurement. This applies to the retained fine label in the soundness induction.

theorem MIPRE.Introspection.Honest.hideOp_entry_prefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (a : HideLabel F ι) (x x' : ι → F) (ha : hideOp P k h a x x' ≠ 0) : (CL.CLFun.truncate k P).eval x = a.1

theorem MIPRE.Introspection.Honest.hideOp_prefix_fixed {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (a : HideLabel F ι) (ha : hideOp P k h a ≠ 0) : P.outputPrefix k a.1 = a.1

theorem MIPRE.Introspection.Honest.readout_mul_hideOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (y : ι → F) (a : HideLabel F ι) : readout (CL.CLFun.truncate k P).eval y * hideOp P k h a = if a.1 = y then hideOp P k h a else 0

def MIPRE.Introspection.Honest.hideLabelAnswer {F : Type u_1} {ι : Type u_2} (a : HideLabel F ι) : ParsedAnswer (ι → F) Unit Unit

Interpret a register hiding label as a correctly formatted parsed answer.

Equations

• MIPRE.Introspection.Honest.hideLabelAnswer a = MIPRE.Introspection.ParsedAnswer.hide a.1 a.2.1 a.2.2

def MIPRE.Introspection.Honest.hideLabelCoarse {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (a : HideLabel F ι) : Option (HideLabel F ι)

Equations

• MIPRE.Introspection.Honest.hideLabelCoarse P k a = MIPRE.Introspection.TypedEstimates.hidingCoarse P k (MIPRE.Introspection.Honest.hideLabelAnswer a)

def MIPRE.Introspection.Honest.hideLabelNext {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (a : HideLabel F ι) : Option (ι → F) × Option (HideLabel F ι)

Equations

• MIPRE.Introspection.Honest.hideLabelNext P k a = MIPRE.Introspection.TypedEstimates.hidingNextLater P k (MIPRE.Introspection.Honest.hideLabelAnswer a)

theorem MIPRE.Introspection.Honest.hidingPrefixOp_mul_next {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (y : Option (ι → F)) (a : HideLabel F ι) : hidingPrefixOp P (k + 1) y * hideOp P (k + 1) h a = if (hideLabelNext P k a).1 = y then hideOp P (k + 1) h a else 0

The next prefix selects exactly the conditioning key of an honest next Hide outcome. The fixed-prefix property is proved from matrix support.

theorem MIPRE.Introspection.Honest.hideLabel_guarded_of_check {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (a b : HideLabel F ι) (hab : CLChecks.hidingNext P k a b) : TypedEstimates.hidingNextGuarded P k (hideLabelNext P k b).1 (hideLabelCoarse P k a) = (hideLabelNext P k b).2

theorem MIPRE.Introspection.Honest.hideOp_conditionalIdeal_eq_next {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : k + 1 < ℓ) (h : P.SupportedOn Finset.univ) (p : Option (ι → F) × Option (HideLabel F ι)) : conditionalIdeal (hideOp P k h) (hidingPrefixOp P (k + 1)) (fun (y : Option (ι → F)) (a : HideLabel F ι) => TypedEstimates.hidingNextGuarded P k y (hideLabelCoarse P k a)) p = fibSum (hideOp P (k + 1) h) (hideLabelNext P k) p

Exact identification of the conditional ideal product with the next honest hiding PVM coarsened by the actual test's retained answer map. Every premise is supplied by the recursively constructed honest operators.

noncomputable def MIPRE.Introspection.Honest.hideCoarseOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) : Option (HideLabel F ι) → Matrix (ι → F) (ι → F) ℂ

The preceding ideal hiding family retains precisely the fine label used by the parsed soundness induction.

Equations

• MIPRE.Introspection.Honest.hideCoarseOp P k h = MIPRE.fibSum (MIPRE.Introspection.Honest.hideOp P k h) (MIPRE.Introspection.Honest.hideLabelCoarse P k)

theorem MIPRE.Introspection.Honest.hideCoarseOp_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) : IsPVM (hideCoarseOp P k h)

theorem MIPRE.Introspection.Honest.hideCoarseOp_conditionalIdeal_eq_next {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : k + 1 < ℓ) (h : P.SupportedOn Finset.univ) (p : Option (ι → F) × Option (HideLabel F ι)) : conditionalIdeal (hideCoarseOp P k h) (hidingPrefixOp P (k + 1)) (TypedEstimates.hidingNextGuarded P k) p = fibSum (hideOp P (k + 1) h) (hideLabelNext P k) p

The guarded conditional ideal formed from the actual retained fine family is exactly the next honest test-coarse measurement.

def MIPRE.Introspection.Honest.hideNextRetain {F : Type u_1} {ι : Type u_2} : Option (ι → F) × Option (HideLabel F ι) → Option (HideLabel F ι)

Discard the now redundant old prefix and retain the new prefix, current dual label, and tail. Dummy or inconsistent formats remain a dummy outcome.

Equations

• MIPRE.Introspection.Honest.hideNextRetain (some y, some (fst, yp, x_1)) = some (y, yp, x_1)
• MIPRE.Introspection.Honest.hideNextRetain x✝ = none

theorem MIPRE.Introspection.Honest.hideCoarseOp_conditionalIdeal_step {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : k + 1 < ℓ) (h : P.SupportedOn Finset.univ) (z : Option (HideLabel F ι)) : fibSum (conditionalIdeal (hideCoarseOp P k h) (hidingPrefixOp P (k + 1)) (TypedEstimates.hidingNextGuarded P k)) hideNextRetain z = hideCoarseOp P (k + 1) h z

Forgetting the redundant conditioning bookkeeping yields precisely the next fine ideal hiding family, ready for the next induction stage.