Formalpedia

The definitions of the module MIPRE.Foundations.Introspection.BasisProg of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Executable conversion to the introspection field basis. The sampler's field arithmetic uses canonical Shoup polynomial coordinates, whereas downsizing uses the constructed self-dual normal basis. These are two different encodings. The fixed programs below construct that basis from its unary odd degree and convert in both directions, including row-wise conversion. No basis matrix is supplied as an oracle or chosen independently of the code.

Definitions (5): MIPRE.Introspection.BasisProgram.fromBasisProg (Evaluate supplied basis coordinates in the canonical polynomial basis.); MIPRE.Introspection.BasisProgram.fromSelfDualProg (Effective self-dual coordinates to canonical field bits.); MIPRE.Introspection.BasisProgram.fromSelfDualRowsProg; MIPRE.Introspection.BasisProgram.toSelfDualProg (Canonical field bits to the effective self-dual basis coordinates.); MIPRE.Introspection.BasisProgram.toSelfDualRowsProg (Construct the basis once for the row list, then convert each row.).

Formalization Note The bundle is the module MIPRE.Foundations.Introspection.BasisProg (MIPRE/Foundations/Introspection/BasisProg.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 113 imported bundle(s).

Let $R$ be a noetherian commutative integral domain with $104$ invertible. The original inverse finite-model comparison identifies the actual finite coordinate scheme with its specified inverse-chart open $V$ in the order-thirteen curve: (...) This is the original chosen affine-open isomorphism, with its literal inclusion identities. In particular $V$ is affine.

Let $R$ be a commutative ring. Put $\delta=(w-1-z-z^3)(w-1-z+z^3)$ in the actual reciprocal coordinate ring. The original first-chart open is the union of the ordinary-chart image and the reciprocal principal-open image $D(\delta)$. The original coordinate, localization, spectral-map and open-image constructors are retained. This original open is definitionally equal to the first-chart open supplied by the public affine-complement theorem.

The definitions of the module MIPRE.Foundations.Introspection.AdaptivePlayerSwap of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Exchanging players in the actual parsed introspection game. The Pauli predicate is transposed explicitly; no symmetry of that predicate is assumed. The directed auxiliary checks already include both orientations, so the original decision predicate and role-indexed CL maps stay unchanged.

Definitions (3): MIPRE.Introspection.TypedEstimates.introAliceZError (Alice's primitive computational-basis error, with malformed Pauli answers kept as the separate option outcome.); MIPRE.Introspection.TypedEstimates.transposePauliPredicate (Transpose every Pauli input, including the actual question contents.); MIPRE.Introspection.TypedPresentation.edgeSwap (The exact involution of the uniformly sampled ordered type edges.).

Formalization Note The bundle is the module MIPRE.Foundations.Introspection.AdaptivePlayerSwap (MIPRE/Foundations/Introspection/AdaptivePlayerSwap.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 135 imported bundle(s).

A statement of the module MIPRE.Foundations.Introspection.AdaptiveInductionIteration of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Finite iteration of the actual Alice Introspect replacement. The auxiliary carrier and state are explicit at every level. Starting with the original projective family, each successor is constructed from the current game's tests. The numerical inverse threshold discharges every smallness premise. All other questions retain their iterated identity extensions, and all fixed hiding errors are preserved exactly.

A concrete projective strategy family exists after every finite Alice stage. The original primitive bounds and explicit positive threshold suffice; no future structural invariant, future error bound, or stage-smallness conclusion is assumed. The full option-valued invariant includes malformed answers and the support of all valid answers.

Formal statement. In Lean, with the scope shown:

open MIPRE
open MIPRE.Introspection
open MIPRE.Introspection.TypedEstimates
open Finset Matrix Classical
variable {H Ω : Type u} {K : Type*}
variable {I B : Type*} [Fintype I] [DecidableEq I] [Fintype B] [DecidableEq B]
variable {PauliType PauliAnswer κ : Type*} {F ι A : Type u}

theorem MIPRE.Introspection.TypedEstimates.exists_intro_iteration
    (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)
    (ξ : H × K → ℂ) (hξ : star ξ ⬝ᵥ ξ = 1)
    (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ →
      POVM (ParsedAnswer (ι → F) A PauliAnswer) ((ι → F) × H))
    (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ →
      POVM (ParsedAnswer (ι → F) A PauliAnswer) ((ι → F) × K))
    (hMA : ∀ q, IsPVM (fun a => ((MA q).mats a).val))
    (hMB : ∀ q, IsPVM (fun a => ((MB q).mats a).val))
    (q : κ → ZMod 2) (hq : ∀ z, (P Z).eval z = q)
    (w : Bool) (hL : (L w).SupportedOn univ)
    {initial η δ : ℝ} (hi0 : 0 ≤ initial) (hη0 : 0 ≤ η) (hδ0 : 0 ≤ δ)
    (hfail : 1 - povmValue (parsedGame E X Z P L projectPauli D DP)
      (registerState (ι → F) ξ) MA MB ≤ initial)
    (hZ : introBobZError projectPauli Z q ξ MB ≤ η)
    (hhide : ∀ j : Fin ℓ, hidingAliceError L w hL ξ MA j ≤ δ)
    (hi : initial ≤ adaptiveSmallThreshold ℓ (TypeGraph.edges E X Z ℓ).card ℓ)
    (hη : η ≤ adaptiveSmallThreshold ℓ (TypeGraph.edges E X Z ℓ).card ℓ)
    (hδ : δ ≤ adaptiveSmallThreshold ℓ (TypeGraph.edges E X Z ℓ).card ℓ)
    (n : ℕ) (hn : n ≤ ℓ) :
    ∃ (MN : CL.Detyping.Question (QuestionType PauliType ℓ) κ →
        POVM (ParsedAnswer (ι → F) A PauliAnswer)
          ((ι → F) × introIterationAux H (Option ((ι → F) × A)) n))
      (_ : IntroPrefixInvariant (L w) n
        ((MN (QuestionType.introspect w, 0)).map introspectPair)),
      (∀ t, IsPVM (fun a => ((MN t).mats a).val)) ∧
      1 - povmValue (parsedGame E X Z P L projectPauli D DP)
        (registerState (ι → F)
          (introIterationState ξ (none : Option ((ι → F) × A)) n)) MN MB ≤
            adaptiveFailureBudget ℓ (TypeGraph.edges E X Z ℓ).card η δ initial n ∧
      (∀ t, t ≠ (QuestionType.introspect w, 0) →
        MN t = introIterationExtend (Option ((ι → F) × A)) (MA t) n) ∧
      (∀ j : Fin ℓ, hidingAliceError L w hL
        (introIterationState ξ (none : Option ((ι → F) × A)) n) MN j =
          hidingAliceError L w hL ξ MA j)

Formalization Note MIPRE.Introspection.TypedEstimates.exists_intro_iteration is declared in MIPRE/Foundations/Introspection/AdaptiveInductionIteration.lean, lines 104–198. The binders, hypotheses and conclusion are exactly those of the Lean statement above; the uploaded statement elaborates to the same type as the declaration in the repository. The definitions it mentions are those of the published definition bundles of the module's import closure.

The definitions of the module MIPRE.Foundations.SAT.EffectiveNormalBasis of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). The effective self-dual normal basis theorem. Starting only with the unary odd degree, the program constructs Shoup's quotient field, a normal element by fixed-space projections, its self-dualized Frobenius orbit, and all multiplication-table bits. No abstract choice of a normal element occurs in the program. The underlying Shoup constructor is proved by a specified polynomial-time program, and the construction uses only the standard Lean axioms.

Definitions (2): MIPRE.SAT.shoupSelfDualNormalBasis; MIPRE.SAT.shoupSelfDualNormalBasisProg (The uniform unary-degree basis constructor.).

Embedded lemmas (1): the small results the bodies of these definitions need (proof fields, simp rules, decidability and finiteness instances), proved inside the bundle so that it imports no unproved statement: instFactPrimeOfNatNat_mIPRE_7.

Formalization Note The bundle is the module MIPRE.Foundations.SAT.EffectiveNormalBasis (MIPRE/Foundations/SAT/EffectiveNormalBasis.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 112 imported bundle(s).

The definitions of the module MIPRE.Foundations.Introspection.AdaptiveInductionIteration of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Finite iteration of the actual Alice Introspect replacement. The auxiliary carrier and state are explicit at every level. Starting with the original projective family, each successor is constructed from the current game's tests. The numerical inverse threshold discharges every smallness premise. All other questions retain their iterated identity extensions, and all fixed hiding errors are preserved exactly.

Definitions (5): MIPRE.Introspection.introIterationAux (The original auxiliary space with one fresh local register per step.); MIPRE.Introspection.introIterationAuxDecidableEq; MIPRE.Introspection.introIterationAuxFintype; MIPRE.Introspection.introIterationExtend (The exact repeated identity extension of an untouched measurement.); MIPRE.Introspection.introIterationState (Each added register is in the same fixed basis state on Alice's side.).

Embedded lemmas (2): the small results the bodies of these definitions need (proof fields, simp rules, decidability and finiteness instances), proved inside the bundle so that it imports no unproved statement: introIterationExtend_zero, introIterationState_zero.

Formalization Note The bundle is the module MIPRE.Foundations.Introspection.AdaptiveInductionIteration (MIPRE/Foundations/Introspection/AdaptiveInductionIteration.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 134 imported bundle(s).

A statement of the module MIPRE.Background.QLD.PauliQuestionPrograms of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Faithful extraction of the Pauli question's arithmetic fields. The basis metadata from finite routing selects the corresponding point and scalar. The explicit axis direction agrees with the original game after the same seed permutation used by the sampled-game transport.

Formal statement. In Lean, with the scope shown:

open MIPRE
open MIPRE.QLD
open MIPRE.Cost MIPRE.SAT MIPRE.Introspection.FieldQuestionProgram MIPRE.Introspection.SeedProgram MIPRE.QLD.PauliCL MIPRE.QLD.PauliBranchProgram

theorem MIPRE.QLD.PauliQuestionProgram.gammaProg_fieldEncoding (k : ℕ) (hk : 1 ≤ k) {m : ℕ}
    (x : Coord m → (shoupBinField k hk).carrier) :
    Introspection.FieldGammaProgram.gammaProg (unary k,
      (Introspection.PauliStageProgram.pointX (fieldEncoding (shoupBinField k hk) x)).zip
        (Introspection.PauliStageProgram.pointZ (fieldEncoding (shoupBinField k hk) x)),
      Introspection.PauliStageProgram.scalarX (fieldEncoding (shoupBinField k hk) x),
      Introspection.PauliStageProgram.scalarZ (fieldEncoding (shoupBinField k hk) x)) =
      LowDegree.BinaryLinear.bit (gam (vectorContent x).omega)

Formalization Note MIPRE.QLD.PauliQuestionProgram.gammaProg_fieldEncoding is declared in MIPRE/Background/QLD/PauliQuestionPrograms.lean, lines 44–63. The binders, hypotheses and conclusion are exactly those of the Lean statement above; the uploaded statement elaborates to the same type as the declaration in the repository. The definitions it mentions are those of the published definition bundles of the module's import closure.

A statement of the module MIPRE.Foundations.Introspection.AdaptiveInductionStep of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). A successor of the actual Introspect induction. The current game's tests construct the replacement. Canonicalization and decoder recovery discharge the selected-measurement identity, and decoding gives the next structural invariant. The fixed hiding and primitive Z errors can be reused on the enlarged auxiliary space.

The actual current tests produce a projective next family and its complete prefix invariant. No selected-measurement or mixing-error bound is assumed: those are derived from the supplied current invariant.

Formal statement. In Lean, with the scope shown:

open MIPRE
open MIPRE.Introspection
open MIPRE.Introspection.TypedEstimates
open Finset Matrix Classical MIPRE.Weyl
variable {PauliType PauliAnswer F ι κ A H K : Type*}

theorem MIPRE.Introspection.TypedEstimates.exists_intro_successor
    (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)
    (ξ : H × K → ℂ) (hξ : star ξ ⬝ᵥ ξ = 1)
    (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ →
      POVM (ParsedAnswer (ι → F) A PauliAnswer) ((ι → F) × H))
    (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ →
      POVM (ParsedAnswer (ι → F) A PauliAnswer) ((ι → F) × K))
    (hMA : ∀ q, IsPVM (fun a => ((MA q).mats a).val))
    (hMB : ∀ q, IsPVM (fun a => ((MB q).mats a).val))
    (q : κ → ZMod 2) (hq : ∀ z, (P Z).eval z = q)
    (w : Bool) (hL : (L w).SupportedOn univ) (j : Fin ℓ)
    (I : IntroPrefixInvariant (L w) j.val
      ((MA (QuestionType.introspect w, 0)).map introspectPair))
    {ε η δ : ℝ} (hε : 0 ≤ ε) (hη : 0 ≤ η) (hδ : 0 ≤ δ)
    (hfail : 1 - povmValue (parsedGame E X Z P L projectPauli D DP)
      (registerState (ι → F) ξ) MA MB ≤ ε)
    (hZ : introBobZError projectPauli Z q ξ MB ≤ η)
    (hhide : hidingAliceError L w hL ξ MA j ≤ δ)
    (hsmall : adaptiveStageBudget (ℓ - j.val)
      ((TypeGraph.edges E X Z ℓ).card * ε) η δ ≤ 1) :
    ∃ (MA' : CL.Detyping.Question (QuestionType PauliType ℓ) κ →
        POVM (ParsedAnswer (ι → F) A PauliAnswer)
          ((ι → F) × (H × Option ((ι → F) × A))))
      (_ : IntroPrefixInvariant (L w) (j.val + 1)
        ((MA' (QuestionType.introspect w, 0)).map introspectPair)),
      (∀ t, IsPVM (fun a => ((MA' t).mats a).val)) ∧
      1 - povmValue (parsedGame E X Z P L projectPauli D DP)
        (registerState (ι → F) (extVecA ξ (none : Option ((ι → F) × A)))) MA' MB ≤
          ε + adaptiveStepLoss (adaptiveStageBudget (ℓ - j.val)
            ((TypeGraph.edges E X Z ℓ).card * ε) η δ) ∧
      (∀ t, t ≠ (QuestionType.introspect w, 0) → MA' t = registeredExtendPOVM (MA t)) ∧
      (∀ i : Fin ℓ, hidingAliceError L w hL
        (extVecA ξ (none : Option ((ι → F) × A))) MA' i = hidingAliceError L w hL ξ MA i)

Formalization Note MIPRE.Introspection.TypedEstimates.exists_intro_successor is declared in MIPRE/Foundations/Introspection/AdaptiveInductionStep.lean, lines 88–166. The binders, hypotheses and conclusion are exactly those of the Lean statement above; the uploaded statement elaborates to the same type as the declaration in the repository. The definitions it mentions are those of the published definition bundles of the module's import closure.

The definitions of the module MIPRE.Foundations.Introspection.AdaptiveInductionStep of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). A successor of the actual Introspect induction. The current game's tests construct the replacement. Canonicalization and decoder recovery discharge the selected-measurement identity, and decoding gives the next structural invariant. The fixed hiding and primitive Z errors can be reused on the enlarged auxiliary space.

Definitions (3): MIPRE.Introspection.TypedEstimates.introBobZError (The primitive Bob-Z error in the common registered state.); MIPRE.Introspection.introSuccessorFamily (The actual question-indexed family after inserting the decoded replacement, with the original family retained at every other question.); MIPRE.Introspection.introSuccessorInvariant (The returned raw selected measurement carries the complete next option-valued product form, including valid-answer support.).

Formalization Note The bundle is the module MIPRE.Foundations.Introspection.AdaptiveInductionStep (MIPRE/Foundations/Introspection/AdaptiveInductionStep.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 132 imported bundle(s).

Let $R$ be a noetherian commutative integral domain with $104$ invertible. Let $B=R[S][a,b]$ be the actual inverse finite coordinate algebra and $v:\operatorname{Spec}B\to C$ the original glued comparison to the order-thirteen curve. Let $c:C\to\operatorname{Spec}R$ and $b:\operatorname{Spec}B\to\operatorname{Spec}R$ be their specified structural maps. Then (...) This compatibility supplies the actual $R$-algebra comparison for the inverse affine-chart section ring.

Let $R$ be a noetherian commutative integral domain with $104$ invertible, and let $B=R[S][a,b]$ be the actual inverse finite coordinate algebra of the order-thirteen curve $C$. The original glued comparison (...) is an open immersion. This supplies the geometric input identifying the literal inverse-chart open with the finite affine coordinate scheme.

The definitions of the module MIPRE.Background.QLD.PauliBranchPrograms of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Faithful finite routing of the Pauli decision rules. Only the fixed twenty-six types are tabulated. The route retains orientation, basis and actual Magic Square indices. Equal-type consistency is selected only for equal types, and every edge selects a substantive rule rather than the off-graph default. Field computations remain uniform programs supplied by the caller; this finite dispatcher never tabulates field elements or answers.

Definitions (8): MIPRE.QLD.PauliBranchProgram.Route (Rule number, orientation reversal, primary index, secondary index.); MIPRE.QLD.PauliBranchProgram.basisIndex; MIPRE.QLD.PauliBranchProgram.formatGuard (Reject either malformed payload before using the selected Boolean rule.); MIPRE.QLD.PauliBranchProgram.orientProg (Put the distinguished point, half-pair or constraint on the left before calling the corresponding uniform field/bit check.); MIPRE.QLD.PauliBranchProgram.pairRoute; MIPRE.QLD.PauliBranchProgram.route; MIPRE.QLD.PauliBranchProgram.routeProg; MIPRE.QLD.PauliBranchProgram.selectProg (The first eight supplied Boolean checks have the order of the route numbers.).

Embedded lemmas (1): the small results the bodies of these definitions need (proof fields, simp rules, decidability and finiteness instances), proved inside the bundle so that it imports no unproved statement: routeProg_apply.

Formalization Note The bundle is the module MIPRE.Background.QLD.PauliBranchPrograms (MIPRE/Background/QLD/PauliBranchPrograms.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 152 imported bundle(s).

Let $R$ be a noetherian commutative integral domain with $104$ invertible. The actual inverse finite coordinate scheme has its specified structural map to $\operatorname{Spec}R$, obtained by composing the polynomial parameter map with the coefficient inclusion. The original recovered reciprocal equivalence also gives the specified $R$-algebra map from the finite coordinate algebra to the positive reciprocal patch. These two literal constructors supply the base-compatibility theorem and the structural section-ring comparison.

Let $R$ be a noetherian commutative integral domain with $104$ invertible. Let $v:\operatorname{Spec}B\to C$ be the original glued comparison from the actual inverse finite coordinate algebra to the order-thirteen curve. Its image is exactly the union of the specified ordinary-parameter and positive-reciprocal chart images: (...) This identifies the underlying subset used by the actual inverse affine-chart presentation.

The definitions of the module MIPRE.Background.QLD.TypeEncoding of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Faithful type labels and the finite Pauli branch decoder. Only the fixed set of twenty-six question types is tabulated. Field elements, dimensions, seeds and answers are handled by uniform programs.

Definitions (3): MIPRE.QLD.PauliCL.typeTag; MIPRE.QLD.instSizedEncodingTy; _private.MIPRE.Background.QLD.TypeEncoding.0.MIPRE.QLD.PauliCL.typeTable.

Embedded lemmas (1): the small results the bodies of these definitions need (proof fields, simp rules, decidability and finiteness instances), proved inside the bundle so that it imports no unproved statement: typeTable_encode.

Formalization Note The bundle is the module MIPRE.Background.QLD.TypeEncoding (MIPRE/Background/QLD/TypeEncoding.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 151 imported bundle(s).

Let $R$ be a noetherian commutative integral domain with $104$ invertible. The actual inverse finite algebra $B=R[S][a,b]$ has the specified ordinary-localization and positive-reciprocal atlas. The publicly proved compatibility of its maps to the order-thirteen curve $C$ determines the original glued morphism $\operatorname{Spec}B\to C$. Its restrictions to both atlas members are the retained literal chart maps. The image and open-immersion assertions remain separate theorems.

Let $R$ be a commutative ring. The ordinary parameter localization and the positive reciprocal patch map to the actual order-thirteen curve by open immersions. Their specified open images determine the literal inverse chart (...) This is the original chart-open constructor used by the global inverse comparison and integral finite-map data.

A statement of the module MIPRE.Background.AnswerReduction.ParamsCost of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). The running time of the parameter routine. Piece AR-3f of planning/answer-reduction.md. The routine parProg of answer reduction computes the PCP's parameters pd n by loops whose lengths are the values λ, n, μ, Q = (λn + 1)^μ and the parameters k, m, s; so its time is polynomial in those values, and dominated in the sense of MIPRE.Pipeline.PDom by any W ≥ Q, λ, σ, n at K = μ (parProg_time), provided the PCP's parameters are polynomial in (log n, log T, Q, σ) (ParamsBound), as the paper's pcpparams are. The bit length of T = 2^{(Q + 5)(μ + 1)} is `(Q + 5)(μ +…

The running time of the routine's core, on ((λ, μ, σ), n).

Formal statement. In Lean, with the scope shown:

open MIPRE
open MIPRE.AnswerReduction
open MIPRE.Cost MIPRE.Cost.PolyTimeFun MIPRE.CL.Detyping.Program MIPRE.Pipeline MIPRE.SAT MIPRE.AnswerReduction.StageProg
open ParRoutine

theorem MIPRE.AnswerReduction.parCore_time (PD : PcpDecider) (R : Polynomial ℕ) : ∃ c m e, ∀ {W X : ℕ},
    ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X →
    arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W →
    PRuns W X mu c m e (core PD) (.cons (encode (lam, mu, sigma)) (encode n))
      ((family PD lam mu sigma).pd n)

Formalization Note MIPRE.AnswerReduction.parCore_time is declared in MIPRE/Background/AnswerReduction/ParamsCost.lean, lines 200–269. The binders, hypotheses and conclusion are exactly those of the Lean statement above; the uploaded statement elaborates to the same type as the declaration in the repository. The definitions it mentions are those of the published definition bundles of the module's import closure.

The definitions of the module MIPRE.Background.QLD.PauliStagePrograms of the MIP* = RE formalization (commit 70cbf1c of vidick/MIPRE-formalization). Correctness of every executable Pauli stage. These identities cover all twenty-six types and arbitrary prefix vectors. The executable diagonal stage consumes the prefix direction itself, as required by mapOfPrefix, rather than applying the selector a second time.

Definitions (3): MIPRE.QLD.PauliCL.fieldEncoding; MIPRE.QLD.PauliCL.programTag; MIPRE.QLD.PauliCL.stageInput.

Formalization Note The bundle is the module MIPRE.Background.QLD.PauliStagePrograms (MIPRE/Background/QLD/PauliStagePrograms.lean) with every declaration not listed removed, imports rewritten to the bundles of the module's import closure; the declarations keep their names, statements and bodies; the source module is split over 147 imported bundle(s).