Final-fields completeness construction

The completeness transport that fills the completeness field of SelfImprovementFinalFields: from helper-stage completeness, through the orthonormalization SDD step, to the projective final-field completeness estimate. The counterpart of the vendored SelfImprovement/Theorems/Results/SelfImprovementTop/Completeness.lean (under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

Contents

• idx_sub_meas_mass_uniform_unit_const_sub_meas_family_lift_left: the Unit-indexed mass of a constant family is the mass of its one submeasurement.
• completeness_transport_through_orthonormalization: the generic transport, by Preliminaries.completenessTransferSelfConsistentA at Question = Unit.
• final_fields_completeness_of_helper_completeness and …_of_small_errors: its specialization to the self-improvement errors, at the natural and at the literal threshold.

The theorems take the orthonormalization SDD bound as a hypothesis and call no orthonormalization, so they carry no finite-pair, abelian-projection or ζ > 0 hypothesis.

The translation is that of BoundednessTransport/BoundednessGap.lean: a strategy is a SymStrat params 𝔓 K, ψ : QuantumState (ι × ι) is S : SymModel 𝔓 K, A.liftLeft is A.liftLeft S (SubMeas.liftLeft S A), IdxSubMeas.liftLeft F is IdxSubMeas.liftLeft S F, the relations CompletenessAtLeast, BipartiteSSCRel, SDDRel and the masses are read on strategy.state, and Error is ℝ. The lemma idx_sub_meas_mass_uniform_unit_const_sub_meas_family_lift_left places by S.L, so its vendored state ψ is the model S, an explicit first argument. The vendored call completenessTransferSelfConsistentA strategy.state strategy.permInvState strategy.isNormalized … is the M3 form completenessTransferSelfConsistentA strategy.state 𝒟 h𝒟 …, swap symmetry and normalization being theorems of the model. No statement of the vendored file carries a swap, density or normalization hypothesis, so no statement changed beyond the translation; the file sets no option, the vendored file-wide respectTransparency false not being needed.

The classical threshold lemma final_fields_completeness_error_le_selfImprovementError (vendored Thresholds/Final.lean) is imported; the imports mirror the vendored ones.

Not ported

Every declaration of the vendored file has a counterpart here.

References

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

• references/ldt-paper/self_improvement.tex lines 351--414 and 713--717
• blueprint/src/chapter/ch07_self_improvement.tex lines 101--142

theorem MIPRE.LIDT.Co.SelfImprovement.idx_sub_meas_mass_uniform_unit_const_sub_meas_family_lift_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (A : SubMeas α 𝔓) : S.idxSubMeasMass (MIPStarRE.LDT.uniformDistribution Unit) (IdxSubMeas.liftLeft S (constSubMeasFamily A)) = S.subMeasMass (SubMeas.liftLeft S A)

The Unit-indexed mass of the left lift of a constant family is the mass of the left lift of its one submeasurement.

theorem MIPRE.LIDT.Co.SelfImprovement.completeness_transport_through_orthonormalization {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (A B : SubMeas α 𝔓) (m δ ε : ℝ) (hcomplete : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state A) m) (hssc : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) δ) (hsdd : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (IdxSubMeas.liftLeft strategy.state (constSubMeasFamily A)) (IdxSubMeas.liftLeft strategy.state (constSubMeasFamily B)) ε) : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state B) (m - δ - 2 * √ε)

Completeness transport through helper-stage strong self-consistency and the orthonormalization SDD step, for the Unit-indexed constant families of the self-improvement pipeline.

Given the completeness hcomplete of the helper-stage submeasurement A at level m, its bipartite strong self-consistency hssc at δ, and the orthonormalization SDD bound hsdd between the left lifts of A and B at ε, the left lift of B is complete at m - δ - 2 √ε. The proof is Preliminaries.completenessTransferSelfConsistentA at Question = Unit, after rewriting the Unit-indexed masses.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_completeness_of_helper_completeness {𝔓 : 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 𝔓 K) (eps delta nu : ℝ) (Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hhelperCompleteness : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state Hhat) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)) (hssc : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)) (horth : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft strategy.state Hhat)) (constSubMeasFamily (SubMeas.liftLeft strategy.state H.toSubMeas)) (MIPStarRE.LDT.SelfImprovement.selfImprovementOrthogonalizationError params eps delta)) : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta - 2 * √(MIPStarRE.LDT.SelfImprovement.selfImprovementOrthogonalizationError params eps delta))

Final-fields completeness construction.

From the helper-stage completeness of Hhat.liftLeft at (1 - nu) - selfImprovementHelperError, the helper-stage strong self-consistency of Hhat and the orthonormalization SDD bound between Hhat.liftLeft and H.toSubMeas.liftLeft, the completeness field of SelfImprovementFinalFields at the natural paper sum `(1 - nu) - selfImprovementHelperError - selfImprovementHelperError

• 2 √selfImprovementOrthogonalizationError. The comparison with (1 - nu) - selfImprovementErroris the separate numerical step of `final_fields_completeness_of_helper_completeness_of_small_errors`.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_completeness_of_helper_completeness_of_small_errors {𝔓 : 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 𝔓 K) (eps delta nu : ℝ) (heps : 0 ≤ eps) (heps_le_one : eps ≤ 1) (hdelta : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (hd_le_q : ↑params.d ≤ ↑params.q) (Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hhelperCompleteness : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state Hhat) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)) (hssc : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)) (horth : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft strategy.state Hhat)) (constSubMeasFamily (SubMeas.liftLeft strategy.state H.toSubMeas)) (MIPStarRE.LDT.SelfImprovement.selfImprovementOrthogonalizationError params eps delta)) : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

Literal-threshold completeness construction under the standard unit-interval hypotheses: final_fields_completeness_of_helper_completeness with the numerical absorption final_fields_completeness_error_le_selfImprovementError, giving exactly the completeness threshold of SelfImprovementFinalFields.