Propagating reported question prefixes through the actual hiding chain

The adjacent hiding, terminal hiding/Read, and Read/Introspect tests preserve every earlier question prefix. Coarse-graining these accepted-answer relations before using consistency loops gives a polynomial chain loss, without an answer-cardinality factor or an assumption that claimed answers are CL images.

def MIPRE.Introspection.TypedEstimates.reportedPrefix {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (m : ℕ) : AuxType ℓ → ParsedAnswer (ι → F) A PauliAnswer → Option (ι → F)

The reported question prefix, with a shared dummy outcome for answer constructors that do not fit the specified auxiliary question type.

Equations

• MIPRE.Introspection.TypedEstimates.reportedPrefix P m MIPRE.Introspection.AuxType.introspect (MIPRE.Introspection.ParsedAnswer.pair y a) = some (P.outputPrefix m y)
• MIPRE.Introspection.TypedEstimates.reportedPrefix P m MIPRE.Introspection.AuxType.sample (MIPRE.Introspection.ParsedAnswer.pair y a) = some (P.outputPrefix m y)
• MIPRE.Introspection.TypedEstimates.reportedPrefix P m MIPRE.Introspection.AuxType.read (MIPRE.Introspection.ParsedAnswer.read y yp a) = some (P.outputPrefix m y)
• MIPRE.Introspection.TypedEstimates.reportedPrefix P m (MIPRE.Introspection.AuxType.hide k) (MIPRE.Introspection.ParsedAnswer.hide y yp x_2) = some (P.outputPrefix m y)
• MIPRE.Introspection.TypedEstimates.reportedPrefix P m x✝¹ x✝ = none

theorem MIPRE.Introspection.TypedEstimates.check_hiding_next_prefix {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (k j : Fin ℓ) (hk : ↑k + 1 = ↑j) (m : ℕ) (hm : m ≤ ↑k) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.hide w k) (QuestionType.hide w j) a b = true) : reportedPrefix (L w) m (AuxType.hide k) a = reportedPrefix (L w) m (AuxType.hide j) b

Every prefix already present at the earlier hiding level agrees on an accepted adjacent hiding edge, including arbitrary off-image claimed outputs.

theorem MIPRE.Introspection.TypedEstimates.check_hiding_read_prefix {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (k : Fin ℓ) (hk : ↑k + 1 = ℓ) (m : ℕ) (hm : m ≤ ↑k) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.hide w k) (QuestionType.read w) a b = true) : reportedPrefix (L w) m (AuxType.hide k) a = reportedPrefix (L w) m AuxType.read b

The last hiding/Read test preserves every question prefix available at the last hiding level.

theorem MIPRE.Introspection.TypedEstimates.check_read_introspect_prefix {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (m : ℕ) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.read w) (QuestionType.introspect w) a b = true) : reportedPrefix (L w) m AuxType.read a = reportedPrefix (L w) m AuxType.introspect b

Read and Introspect preserve every question prefix in this orientation.

def MIPRE.Introspection.TypedEstimates.prefixChainType {ℓ : ℕ} (j : Fin ℓ) (i : ℕ) : AuxType ℓ

The actual auxiliary path starting at hiding level j, followed by Read and Introspect. Beyond the endpoint it remains at Introspect.

Equations

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

@[simp]

theorem MIPRE.Introspection.TypedEstimates.prefixChainType_zero {ℓ : ℕ} (j : Fin ℓ) : prefixChainType j 0 = AuxType.hide j

@[simp]

theorem MIPRE.Introspection.TypedEstimates.prefixChainType_end {ℓ : ℕ} (j : Fin ℓ) : prefixChainType j (ℓ - ↑j + 1) = AuxType.introspect

theorem MIPRE.Introspection.TypedEstimates.prefixChainType_adj {PauliType : Type u_1} {ℓ : ℕ} (X Z : PauliType) [DecidableEq PauliType] (E : PauliType → PauliType → Bool) (w : Bool) (j : Fin ℓ) (i : ℕ) (hi : i < ℓ - ↑j + 1) : TypeGraph.Adj E X Z (Sum.inr (prefixChainType j i, w)) (Sum.inr (prefixChainType j (i + 1), w))

Every step of this path is an actual edge of the introspection graph.

theorem MIPRE.Introspection.TypedEstimates.prefixChainType_check {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) [DecidableEq PauliType] (w : Bool) (hL : (L w).SupportedOn Finset.univ) (j : Fin ℓ) (m : ℕ) (hm : m ≤ ↑j) (i : ℕ) (hi : i < ℓ - ↑j + 1) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (Sum.inr (prefixChainType j i, w)) (Sum.inr (prefixChainType j (i + 1), w)) a b = true) : reportedPrefix (L w) m (prefixChainType j i) a = reportedPrefix (L w) m (prefixChainType j (i + 1)) b

Accepted answers on every actual path edge preserve the requested earlier prefix. There is no additional accepted-answer hypothesis in the final bound.