Section 12 pasting: from-H-to-G collapsed bounds

Collapses the paper endpoint M₄ to the next Lean stage and records the scalar bounds used by the final telescope.

noncomputable def MIPStarRE.LDT.Pasting.fromHToGAdjacentStageCollapsed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (k ℓ : ℕ) : Error

Equations

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

theorem MIPStarRE.LDT.Pasting.fromHToGAdjacentStageCollapsed_eq_stage_succ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (hstageExact : FromHToGAdjacentStageExactFacts params ψbi family) (k ℓ : ℕ) : fromHToGAdjacentStageCollapsed params ψbi family k ℓ = fromHToGStageMass params ψbi family k (ℓ + 1)

The collapsed branch expression is exactly the next Lean stage.

theorem MIPStarRE.LDT.Pasting.fromHToGAdjacentStageM4_eq_collapsed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (hcomplete : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total) (hincomplete : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total) (k ℓ : ℕ) : fromHToGAdjacentStageM4 params ψbi family k ℓ = fromHToGAdjacentStageCollapsed params ψbi family k ℓ

M₄ collapses exactly to the branch-averaged recurrence expression.

theorem MIPStarRE.LDT.Pasting.fromHToG_headTail_qSDDCore_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψbi family gamma zeta j) {n k : ℕ} (hn : 2 ≤ n + 1) (hnk : n + 1 ≤ k) : (avgOver (uniformDistribution (Fq params × PointTuple params n)) fun (q : Fq params × PointTuple params n) => qSDDCore ψbi (fun (ogs : GHatOutcome params × GHatTupleOutcome params n) => leftTensor ((gHatIdxMeas params family q.1).outcome ogs.1 * gHatHalfProductOutcomeOperator params family n q.2 ogs.2)) fun (ogs : GHatOutcome params × GHatTupleOutcome params n) => leftTensor (gHatHalfProductOutcomeOperator params family n q.2 ogs.2 * (gHatIdxMeas params family q.1).outcome ogs.1)) ≤ commuteGHalfSandwichError params gamma zeta k

Raw qSDDCore form of the half-sandwich commutation hypothesis after splitting a nonempty sandwich into its head and tail, with the error weakened to the ambient length k.

theorem MIPStarRE.LDT.Pasting.fromHToG_selfConsistency_qSDDCore_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) (hcompleted : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family) (gHatSelfConsistencyRightFamily params family) (gHatSelfConsistencyError zeta)) {n : ℕ} : (avgOver (uniformDistribution (Fq params × PointTuple params n)) fun (q : Fq params × PointTuple params n) => qSDDCore ψbi (fun (g : GHatOutcome params) => leftTensor ((gHatIdxMeas params family q.1).outcome g)) fun (g : GHatOutcome params) => rightTensor ((gHatIdxMeas params family q.1).outcome g)) ≤ 2 * zeta

The completed self-consistency estimate used in the first and final move-right steps, after adjoining an irrelevant uniform suffix-question register.

theorem MIPStarRE.LDT.Pasting.fromHToG_headTail_adjoint_qSDDCore_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψbi family gamma zeta j) {n k : ℕ} (hn : 2 ≤ n + 1) (hnk : n + 1 ≤ k) : (avgOver (uniformDistribution (Fq params × PointTuple params n)) fun (q : Fq params × PointTuple params n) => qSDDCore ψbi (fun (ogs : GHatOutcome params × GHatTupleOutcome params n) => leftTensor (Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family n q.2 ogs.2) * (gHatIdxMeas params family q.1).outcome ogs.1)) fun (ogs : GHatOutcome params × GHatTupleOutcome params n) => leftTensor ((gHatIdxMeas params family q.1).outcome ogs.1 * Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family n q.2 ogs.2))) ≤ commuteGHalfSandwichError params gamma zeta k

Adjoint-oriented raw qSDDCore form of the half-sandwich commutation hypothesis. This is the orientation used by the paper's Cauchy--Schwarz decompositions in eq:call-this-later and eq:call-again-later-part-dos.