Section 12 pasting: complete and incomplete part self-consistency

Scalar and state-dependent-distance consequences for the complete and incomplete parts of the pasted slice family.

theorem MIPStarRE.LDT.Pasting.first_construction_scalar_inequality (lambda : Error) (d : ℕ) (h0 : 0 ≤ lambda) (h1 : lambda ≤ 1) : lambda * (1 - lambda ^ d) ≤ 2 * Real.rpow (lambda ^ (d + 1) * (1 - lambda)) (1 / ↑(d + 1))

Scalar inequality for the first spectral construction in lem:ld-pasting.

theorem MIPStarRE.LDT.Pasting.qSDD_completePart_le_slice {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (x : Fq params) : qSDD ψbi (completePartSubMeas params family x).liftLeft (completePartSubMeas params family x).liftRight ≤ qSDD ψbi (family.meas x).liftLeft (family.meas x).liftRight

lem:q-sdd-complete-part-slice-bound.

theorem MIPStarRE.LDT.Pasting.gCompleteSelfConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) (_hperm : PermInvState ψbi) (hself : family.StronglySelfConsistent ψbi zeta) : GCompleteSelfConsistencyStatement params ψbi family zeta

lem:g-complete-self-consistency. This is exactly the slice strong self-consistency hypothesis, stated under the Section 12 statement name.

theorem MIPStarRE.LDT.Pasting.gBotSelfConsistency_ofCompleteSelfConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) (_hperm : PermInvState ψbi) (hcomplete : GCompleteSelfConsistencyStatement params ψbi family zeta) : GBotSelfConsistencyStatement params ψbi family zeta

Internal form of cor:g-bot-self-consistency after applying lem:g-complete-self-consistency.

Source: The proof in references/ldt-paper/ld-pasting.tex:537-558 uses lem:g-complete-self-consistency internally. The paper-facing theorem gBotSelfConsistency below derives that input from strong self-consistency rather than exposing it as a public hypothesis.

theorem MIPStarRE.LDT.Pasting.gBotSelfConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) (hperm : PermInvState ψbi) (hself : family.StronglySelfConsistent ψbi zeta) : GBotSelfConsistencyStatement params ψbi family zeta

cor:g-bot-self-consistency, source-facing form.