Finite iteration of the actual hiding rigidity step

Write e = |E| epsilon. The actual same-type loop and adjacent hiding edge give A_k <= 4e + 2B_k and B_(k+1) <= 6B_k + C, where C = (18 + 48 ell^2)e + 6delta. The closed bound has no dependence on the question or answer alphabet. The base and Introspect-prefix errors are the explicit inputs, to be supplied by the Pauli-X and Pauli-Z tests.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the state is the register model Ξ.reg (ι → F) of a normalized auxiliary model.

def MIPRE.Introspection.TypedEstimates.hidingStepBudget (ℓ : ℕ) (e δ : ℝ) : ℝ

Equations

• MIPRE.Introspection.TypedEstimates.hidingStepBudget ℓ e δ = (18 + 48 * ↑ℓ ^ 2) * e + 6 * δ

noncomputable def MIPRE.Introspection.TypedEstimates.hidingIterationBudget (ℓ : ℕ) (e δ β : ℝ) (k : ℕ) : ℝ

Equations

• MIPRE.Introspection.TypedEstimates.hidingIterationBudget ℓ e δ β k = 6 ^ k * β + (6 ^ k - 1) / 5 * MIPRE.Introspection.TypedEstimates.hidingStepBudget ℓ e δ

@[simp]

theorem MIPRE.Introspection.TypedEstimates.hidingIterationBudget_zero (ℓ : ℕ) (e δ β : ℝ) : hidingIterationBudget ℓ e δ β 0 = β

theorem MIPRE.Introspection.TypedEstimates.hidingIterationBudget_succ (ℓ : ℕ) (e δ β : ℝ) (k : ℕ) : hidingIterationBudget ℓ e δ β (k + 1) = 6 * hidingIterationBudget ℓ e δ β k + hidingStepBudget ℓ e δ

def MIPRE.Introspection.TypedEstimates.hidingUniformBudget (ℓ : ℕ) (e δ β : ℝ) : ℝ

Equations

• MIPRE.Introspection.TypedEstimates.hidingUniformBudget ℓ e δ β = 6 ^ ℓ * (β + MIPRE.Introspection.TypedEstimates.hidingStepBudget ℓ e δ)

theorem MIPRE.Introspection.TypedEstimates.hidingStepBudget_nonneg (ℓ : ℕ) {e δ : ℝ} (he : 0 ≤ e) (hδ : 0 ≤ δ) : 0 ≤ hidingStepBudget ℓ e δ

theorem MIPRE.Introspection.TypedEstimates.hidingIterationBudget_le_uniform {ℓ k : ℕ} (hk : k ≤ ℓ) {e δ β : ℝ} (he : 0 ≤ e) (hδ : 0 ≤ δ) (hβ : 0 ≤ β) : hidingIterationBudget ℓ e δ β k ≤ hidingUniformBudget ℓ e δ β

noncomputable def MIPRE.Introspection.TypedEstimates.hidingIntroPrefixError {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (L : Bool → CL.CLFun F ι ℓ) (w : Bool) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (j : Fin ℓ) : ℝ

Equations

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

theorem MIPRE.Introspection.TypedEstimates.hidingIntroPrefixError_nonneg {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (L : Bool → CL.CLFun F ι ℓ) (w : Bool) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (j : Fin ℓ) : 0 ≤ hidingIntroPrefixError L w Ξ MB j

theorem MIPRE.Introspection.TypedEstimates.hiding_register_recurrence {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) {ε : ℝ} (hε : 0 ≤ ε) (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (hMA : ∀ (j : Fin ℓ), IsPVMIn (MA (QuestionType.hide w j, 0)).op) (hMB : ∀ (j : Fin ℓ), IsPVMIn (MB (QuestionType.hide w j, 0)).op) (k j : Fin ℓ) (hk : ↑k + 1 = ↑j) {δ : ℝ} (hintro : hidingIntroPrefixError L w Ξ MB j ≤ δ) : hidingBobError L w hL Ξ MB j ≤ 6 * hidingBobError L w hL Ξ MB k + hidingStepBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δ

A single recurrence step uses actual tests in their given orientation.

theorem MIPRE.Introspection.TypedEstimates.hiding_register_iteration {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) {ε : ℝ} (hε : 0 ≤ ε) (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (hMA : ∀ (j : Fin ℓ), IsPVMIn (MA (QuestionType.hide w j, 0)).op) (hMB : ∀ (j : Fin ℓ), IsPVMIn (MB (QuestionType.hide w j, 0)).op) (hℓ : 0 < ℓ) {δ β : ℝ} (hbase : hidingBobError L w hL Ξ MB ⟨0, hℓ⟩ ≤ β) (hintro : ∀ (j : Fin ℓ), hidingIntroPrefixError L w Ξ MB j ≤ δ) (j : Fin ℓ) : hidingBobError L w hL Ξ MB j ≤ hidingIterationBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δ β ↑j ∧ hidingAliceError L w hL Ξ MA j ≤ 4 * ↑(TypeGraph.edges E X Z ℓ).card * ε + 2 * hidingIterationBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δ β ↑j

Finite induction over every real hiding level, starting with Bob's actual level-zero estimate and the actual Introspect-prefix estimates.

theorem MIPRE.Introspection.TypedEstimates.hiding_register_iteration_uniform {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) {ε : ℝ} (hε : 0 ≤ ε) (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (hMA : ∀ (j : Fin ℓ), IsPVMIn (MA (QuestionType.hide w j, 0)).op) (hMB : ∀ (j : Fin ℓ), IsPVMIn (MB (QuestionType.hide w j, 0)).op) (hℓ : 0 < ℓ) {δ β : ℝ} (hbase : hidingBobError L w hL Ξ MB ⟨0, hℓ⟩ ≤ β) (hintro : ∀ (j : Fin ℓ), hidingIntroPrefixError L w Ξ MB j ≤ δ) (j : Fin ℓ) : hidingBobError L w hL Ξ MB j ≤ hidingUniformBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δ β ∧ hidingAliceError L w hL Ξ MA j ≤ 4 * ↑(TypeGraph.edges E X Z ℓ).card * ε + 2 * hidingUniformBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δ β

One explicit bound holds at every level, with no extra nonnegativity premises on the supplied base and prefix budgets.