Raw auxiliary soundness of the complete decision kernel

theorem MIPRE.Introspection.DecisionKernel.format_iff_valid (z : AuxiliaryDecision.Input QLD.Ty 7) : AuxiliaryDecision.format.toFun z = true ↔ AuxiliaryAnswer.Valid (AuxiliaryDecision.width.toFun z) (AuxiliaryDecision.originalBound.toFun z) (AuxiliaryDecision.leftType.toFun z) (AuxiliaryDecision.leftBits.toFun z)

theorem MIPRE.Introspection.DecisionKernel.program_auxiliary_facts (W : Cost.ClockedUniversalMachine) (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) (h : (program W).toFun (canonicalInput V lam n Q R p T U x y a b) = true) : AuxiliaryAnswer.Valid Q R T a ∧ AuxiliaryAnswer.Valid Q R U b ∧ (T = U → a = b)

theorem MIPRE.Introspection.DecisionKernel.program_auxiliary_check (W : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) (hab : Q ≤ List.length a + List.length b) (h : (program W).toFun (canonicalInput V lam n Q R p T U x y a b) = true) : (AuxiliaryDecision.check W (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) project).toFun (AuxiliaryDecision.canonical V lam n Q R p T U a b) = true

theorem MIPRE.Introspection.DecisionKernel.project_rawProject_canonical (V : Verifier 7) (lam n R k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j m : ℕ) (W : QLD.Bas) (U : Label) (a b : Cost.BitStr) (ha : (QLD.PauliAnswerProgram.parser.toFun (QLD.Ty.pauli W, Cost.unary m, Cost.unary k, Cost.unary 1, a)).1 = true) : project.toFun (AuxiliaryDecision.canonical V lam n (2 ^ m * k) R (Cost.unary k, Cost.unary j, Cost.unary m) (Sum.inl (QLD.Ty.pauli W)) U a b) = CL.toBits (Answer.rawProject (Cost.unary k, Cost.unary j, Cost.unary m) (2 ^ m * k) a)

noncomputable def MIPRE.Introspection.DecisionKernel.rawPauliCheck (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (x y : Cost.BitStr) (T U : QLD.Ty) (a b : Cost.BitStr) : Bool

The Pauli decision relation after the actual raw question and answer decoders.

Equations

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

theorem MIPRE.Introspection.DecisionKernel.program_raw_quotient_sound (W : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k) (hQ : 4 ≤ 2 ^ 2 ^ j * k) (hR : 3 * (2 ^ n) ^ lam ≤ 2 ^ 2 ^ j * k) (T U : Label) (x y a b : Cost.BitStr) (h : (program W).toFun (canonicalInput V lam n (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) T U x y a b) = true) : AuxiliaryQuotient.check (AuxiliaryDecision.padded V hs) (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (Answer.rawProject (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) (2 ^ 2 ^ j * k)) (AuxiliaryDecision.sourcePredicate V hs) (rawPauliCheck k hk hodd j hm x y) T U (AuxiliaryAnswer.decode (2 ^ 2 ^ j * k) T a) (AuxiliaryAnswer.decode (2 ^ 2 ^ j * k) U b) = true

All auxiliary checks are sound on every accepted raw tuple. The short Pauli/Pauli case is handled without allocating an artificial full prefix.