Line interpolation: bad-mass comparison

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LineInterpolation/BadMass.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The main bad-mass comparison of ld-pasting.tex: the mismatch sums of the eligible sandwich family, the decomposition of a bipartite consistency defect against a measurement into single-outcome defects, the bad mass hBConsistencyBadMass and its bound by the line-point defects, and pastedInterpolation_verticalLine_defect_le_badMass, which bounds the consistency defect of the pasted interpolation restricted to a vertical line by that bad mass.

The slice family is an IdxPolyFamily params 𝔓 and a strategy a SymStrat params.next 𝔓 K, so the sandwiched, pasted and vertical-line families are local, in 𝔓 (the vendored Op ι). The lemmas that read no state (singleOutcomeRightSubMeas, the two postprocess_decide_* lemmas and postprocess_restrictSubMeas_outcome) are generic over an ordered ⋆-ring. The three bipartite defect lemmas take the symmetric model S : SymModel 𝔓 K as their first explicit argument, in place of the vendored ψ : QuantumState (ι × ι), and keep this file's namespace so that their vendored names pair; the strategy lemmas read the defects on strategy.state. The vendored normalization field strategy.isNormalized used by hBConsistencyBadMass_le_one is the hypothesis-free S.ev_one_of_isNormalized, and no statement carries a swap or normalization hypothesis, the vendored statements having none.

Not ported

Every declaration of the vendored file has a counterpart here.

New here

• instDecidableEqFqFqNext, instDecidableEqFqNextFq: scoped instances deciding equality between Fq params and Fq params.next, which the vendored file obtains from its file-wide respectTransparency false; ported dependants in MIPRE.LIDT.Co.Pasting that state the same mismatch conditions (OverAllOutcomes/NonglobalDecomposition) get them by importing this file.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch09_pasting.tex

@[instance_reducible]

def MIPRE.LIDT.Co.Pasting.instDecidableEqFqFqNext {params : MIPStarRE.LDT.Parameters} (x : MIPStarRE.LDT.Fq params) (y : MIPStarRE.LDT.Fq params.next) : Decidable (x = y)

Equality of a coordinate of params with one of params.next is decidable. The vendored file finds instDecidableEqFin here only under its file-wide backward.isDefEq.respectTransparency false, since Fq params.next and Fq params agree only after unfolding Parameters.next; this instance supplies the same decision procedure without the option, scoped to MIPRE.LIDT.Co.Pasting.

Equations

• MIPRE.LIDT.Co.Pasting.instDecidableEqFqFqNext x y = instDecidableEqFin params.q x y

@[instance_reducible]

def MIPRE.LIDT.Co.Pasting.instDecidableEqFqNextFq {params : MIPStarRE.LDT.Parameters} (x : MIPStarRE.LDT.Fq params.next) (y : MIPStarRE.LDT.Fq params) : Decidable (x = y)

Equality of a coordinate of params.next with one of params is decidable (the mirror of instDecidableEqFqFqNext).

Equations

• MIPRE.LIDT.Co.Pasting.instDecidableEqFqNextFq x y = instDecidableEqFin params.next.q x y

noncomputable def MIPRE.LIDT.Co.Pasting.singleOutcomeRightSubMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (B : SubMeas Outcome R) (a0 : Outcome) : SubMeas Bool R

The Boolean submeasurement that keeps only the outcome a0 of B, as its true outcome.

Equations

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

theorem MIPRE.LIDT.Co.Pasting.postprocess_decide_eq_true_outcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] [DecidableEq Outcome] (A : SubMeas Outcome R) (a0 : Outcome) : (postprocess A fun (a : Outcome) => decide (a = a0)).outcome true = A.outcome a0

The true outcome of the indicator postprocessing a ↦ decide (a = a0) is A_{a0}.

theorem MIPRE.LIDT.Co.Pasting.postprocess_decide_false_add_true_eq_total {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] [DecidableEq Outcome] (A : SubMeas Outcome R) (a0 : Outcome) : (postprocess A fun (a : Outcome) => decide (a = a0)).outcome false + A.outcome a0 = A.total

The false outcome of the indicator postprocessing at a0, plus A_{a0}, is the total of A.

theorem MIPRE.LIDT.Co.Pasting.postprocess_restrictSubMeas_outcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] (A : SubMeas α R) (p : α → Prop) [DecidablePred p] (f : α → β) (b : β) : (postprocess (restrictSubMeas A p) f).outcome b = ∑ a : α, if p a ∧ f a = b then A.outcome a else 0

The outcomes of a postprocessed restriction: the sum of the outcomes satisfying p and mapped to b.

theorem MIPRE.LIDT.Co.Pasting.interpolationEligibleSandwich_mismatch_sum_mono {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) (hxs : Function.Injective xs) (f : MIPStarRE.LDT.AxisLinePolynomial params.next) : (∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, if MIPStarRE.LDT.Pasting.IsGloballyConsistent params xs gs ∧ MIPStarRE.LDT.Pasting.tupleInterpolatedVerticalLine params u xs gs ≠ f then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ≤ ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, if ∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0

On globally consistent tuples, a vertical line interpolant different from f forces a slice answer that disagrees with f at its height, so the first mismatch sum is bounded by the second.

theorem MIPRE.LIDT.Co.Pasting.interpolationEligibleSandwich_exists_mismatch_sum_le_sum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) (f : MIPStarRE.LDT.AxisLinePolynomial params.next) : (∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, if ∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ≤ ∑ i : Fin k, ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, if ∃ (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0

A mismatch at some slice is bounded by the sum over slices of the mismatches at each slice.

theorem MIPRE.LIDT.Co.Pasting.pastedInterpolation_verticalLine_singleOutcome_postprocess {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) (f : MIPStarRE.LDT.AxisLinePolynomial params.next) : (postprocess (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) fun (h : MIPStarRE.LDT.AxisLinePolynomial params.next) => decide (h = f)) = postprocess (restrictSubMeas (interpolationEligibleSandwichFamily params family k xs) (MIPStarRE.LDT.Pasting.IsGloballyConsistent params xs)) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k) => decide (MIPStarRE.LDT.Pasting.tupleInterpolatedVerticalLine params u xs gs = f)

Reading the pasted interpolation on the vertical line through u against the single line polynomial f is reading the globally consistent eligible sandwich against the interpolated vertical line.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteConsDefect_eq_false_mass_of_bool_right_true {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (A B : SubMeas Bool 𝔓) (hfalse : B.outcome false = 0) (htrue : B.outcome true = B.total) : S.qBipartiteConsDefect A B = S.ev (S.opTensor (A.outcome false) B.total)

If the right-hand Boolean submeasurement has only the true outcome, the consistency defect is exactly the left false mass against its total operator.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteConsDefect_postprocess_eq_singleOutcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] [DecidableEq Outcome] (S : SymModel 𝔓 K) (A B : SubMeas Outcome 𝔓) (a0 : Outcome) : S.qBipartiteConsDefect (postprocess A fun (a : Outcome) => decide (a = a0)) (singleOutcomeRightSubMeas B a0) = S.ev (S.opTensor ((postprocess A fun (a : Outcome) => decide (a = a0)).outcome false) (B.outcome a0))

The defect of the indicator postprocessing at a0 against the single outcome a0 of B is the mass of A off a0 against B_{a0}.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteConsDefect_eq_sum_singleOutcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] [DecidableEq Outcome] (S : SymModel 𝔓 K) (A : SubMeas Outcome 𝔓) (B : Measurement Outcome 𝔓) : S.qBipartiteConsDefect A B.toSubMeas = ∑ a0 : Outcome, S.qBipartiteConsDefect (postprocess A fun (a : Outcome) => decide (a = a0)) (singleOutcomeRightSubMeas B.toSubMeas a0)

The defect of A against a measurement B is the sum over outcomes a0 of the single-outcome defects.

noncomputable def MIPRE.LIDT.Co.Pasting.hBConsistencyBadMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) : ℝ

The bad mass of the vertical-line consistency: the mass of the eligible sandwich on tuples with a slice answer disagreeing at its height with the line polynomial f, against B^u_f, summed over f.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointRightMeasurement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (i : Fin k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) : Measurement (Option (MIPStarRE.LDT.Fq params)) 𝔓

The one-point right family of the i-th slot, as a measurement.

Equations

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointRightMeasurement_outcome_some_eq_sum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (i : Fin k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (a : MIPStarRE.LDT.Fq params) : (ldSandwichLineOnePointRightMeasurement params strategy family i q).outcome (some a) = ∑ f : MIPStarRE.LDT.AxisLinePolynomial params.next, if f.toFun (q.2 i) = a then (verticalLineMeasurementFamily params strategy q.1).outcome f else 0

The some a outcome of the one-point right measurement is the sum of the vertical line outcomes whose polynomial takes the value a at the slot's height.

theorem MIPRE.LIDT.Co.Pasting.grouped_coordinate_mismatch_le_left_falseOutcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) (i : Fin k) (a : MIPStarRE.LDT.Fq params) : (∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, if ∃ (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ a then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ≤ (postprocess (ldSandwichLineOnePointLeftFamily params strategy family k ↑i (u, xs)) fun (o : Option (MIPStarRE.LDT.Fq params)) => decide (o = some a)).outcome false

The mismatch mass of the i-th slot against the value a is bounded by the false outcome of the one-point left family read against some a.

theorem MIPRE.LIDT.Co.Pasting.hBConsistencyCoordMass_le_linePointDefect {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) (i : Fin k) : ∑ f : MIPStarRE.LDT.AxisLinePolynomial params.next, strategy.state.ev (strategy.state.opTensor (∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, if ∃ (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ((verticalLineMeasurementFamily params strategy u).outcome f)) ≤ strategy.state.qBipartiteConsDefect (ldSandwichLineOnePointLeftFamily params strategy family k ↑i (u, xs)) (ldSandwichLineOnePointRightFamily params strategy family k ↑i (u, xs))

The bad mass of the i-th slot is bounded by the i-th line-point consistency defect.

theorem MIPRE.LIDT.Co.Pasting.hBConsistencyBadMass_le_linePointDefectSum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) : hBConsistencyBadMass params strategy family u xs ≤ ∑ i : Fin k, strategy.state.qBipartiteConsDefect (ldSandwichLineOnePointLeftFamily params strategy family k ↑i (u, xs)) (ldSandwichLineOnePointRightFamily params strategy family k ↑i (u, xs))

The bad mass is bounded by the sum over slots of the line-point consistency defects.

theorem MIPRE.LIDT.Co.Pasting.hBConsistencyBadMass_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) : 0 ≤ hBConsistencyBadMass params strategy family u xs

The bad mass is nonnegative.

theorem MIPRE.LIDT.Co.Pasting.hBConsistencyBadMass_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) : hBConsistencyBadMass params strategy family u xs ≤ 1

The bad mass is at most one.

theorem MIPRE.LIDT.Co.Pasting.pastedInterpolation_verticalLine_defect_le_badMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k : ℕ} (u : MIPStarRE.LDT.Point params) (xs : MIPStarRE.LDT.PointTuple params k) (hxs : Function.Injective xs) : strategy.state.qBipartiteConsDefect (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) (verticalLineMeasurementFamily params strategy u) ≤ hBConsistencyBadMass params strategy family u xs

The consistency defect of the pasted interpolation restricted to the vertical line through u, against the vertical line measurement, is bounded by the bad mass.