Section 12 pasting: fourth-term chain helpers

Internal helpers by convention for the fourth-term chain in commutativitySwitcheroo. These were extracted from SwitcherooCompletion to keep that file under the 1000-line threshold.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateMixedScalar_point {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (q : SlicePairQuestion params) : ∑ g : Polynomial params, ∑ o : Outcome, ev ψbi (rightTensor ((family.meas q.1).outcome g) * leftTensor ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o)) = ∑ g : Polynomial params, ∑ o : Outcome, ev ψbi (leftTensor ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o) * rightTensor ((family.meas q.1).outcome g))

Pointwise identity rewriting the mixed scalar expression into right/left tensor order.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateMixedScalar_close_leftFrontScalar {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (zeta : Error) (hselfG : GCompleteSelfConsistencyStatement params ψbi family zeta) : |switcherooAggregateMixedScalar params ψbi family M - switcherooAggregateLeftFrontScalar params ψbi family M| ≤ √zeta

The mixed scalar expression is within √ζ of the left-front scalar expression.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateOnceCommutedScalar_point {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (q : SlicePairQuestion params) : ∑ g : Polynomial params, ∑ o : Outcome, ev ψbi (leftTensor ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o * (family.meas q.1).outcome g)) = ∑ go : Polynomial params × Outcome, ev ψbi (leftTensor ((completePartSubMeas params family q.1).total * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1))

Sum-rewrite identity collapsing the product-type sum for the once-commuted scalar.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateOnceCommutedScalar_close_mixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (zeta : Error) (hselfG : GCompleteSelfConsistencyStatement params ψbi family zeta) : |switcherooAggregateOnceCommutedScalar params ψbi family M - switcherooAggregateMixedScalar params ψbi family M| ≤ √zeta

The once-commuted scalar expression is within √ζ of the mixed scalar expression.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateLeftFrontScalar_close_firstSplitScalar {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (chi : Error) (hcomm : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (switcherooPointProductLeft params family M) (switcherooPointProductRight params family M) chi) : |switcherooAggregateLeftFrontScalar params ψbi family M - switcherooAggregateFirstSplitScalar params ψbi family M| ≤ √chi

The final sqrt chi comparison in the fourth-term chain: compare the left-front scalar expression with the split-by-g scalar that later collapses to the first positive switcheroo term.