Section 6 β Pasting Assembly: Averaged Family Fields #
The scalar side condition ΞΆ β€ 1 of the small-error branch, the averaged slice errors of the
answer-valued slice route, and the averaged family fields (completeness, point consistency,
strong self-consistency, boundedness) that the answer-valued successor route feeds to pasting.
This is the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/PastingAssembly/Basic.lean in
the port of planning/c6b-plan.md (milestone M12, section "Port conventions").
Translation #
A strategy is a SymStrat params.next π K or an AnswerSymStrat params.next π K
(Co/Test/StrategyCore.lean), whose state is the symmetric model strategy.state : SymModel π K;
a state Ο : QuantumState (ΞΉ Γ ΞΉ) alone is a model S : SymModel π K, in the same position.
Polynomial params is MIPStarRE.LDT.Polynomial params, Error is β, ev Ο is S.ev,
leftTensor/rightTensor are S.L/S.R, SubMeas.liftLeft is .liftLeft S,
leftPlacedSubMeas (ΞΉB := ΞΉ) and rightPlacedSubMeas (ΞΉA := ΞΉ) are S.leftPlacedSubMeas and
S.rightPlacedSubMeas, and the quantities and relations (subMeasMass, bipartiteConsError,
qSDD, sddError, ConsRel, SDDRel, CompletenessAtLeast) are read on the model. The
error functions (mainInductionError, mainInductionNu, selfImprovementInInductionError),
mainInductionNu_lt_one_of_mainInductionError_lt_one and
avgOver_uniform_pointNext_decompose are the vendored classical declarations, reached through
explicit open lists. No vendored statement here has a swap, density or normalization
hypothesis, so none is dropped; no statement takes a new hypothesis. The vendored file-wide
respectTransparency false is not needed: the file sets no option.
Swap use #
The boundedness field of idxPolyFamily_sliceBoundednessInput_of_slice_bounds exchanges the two
factors of β¨Ξ¨| (I - G^x) β Z^x |Ξ¨β©; the vendored proof does so with
ev_opTensor_swap_of_density_fixed strategy.state strategy.permInvState.density_swap, and here
with the keystone's SymModel.ev_L_mul_R_comm, which takes no hypothesis.
Proofs that differ from the vendored ones #
- The two
ΞΆ β€ 1lemmas are one term each,ΞΆ β€ Ξ½ < 1, through CoselfImprovementInInductionError_le_mainInductionNuand the importedmainInductionNu_lt_one_of_mainInductionError_lt_one. average_answerSliceSelfImprovementError_leandaverage_answerSliceError_leare the Coaverage_sliceSelfImprovementError_leandaverage_sliceError_leapplied toSliceRestrictionData.ofAnswerandPerSliceInductionData.ofAnswer, whose fields are those of the answer-valued data by definitional equality, so there is nosimpa.idxPolyFamily_averagedMass_eq_avgisS.ev_leftTensor_averageOperatorOverDistributionby definitional equality, andidxPolyFamily_complete_of_slice_boundsaverages the slice lower bounds withavgOver_monoand closes withavgOver_sub,avgOver_uniform_constandlinarith.- The three point-consistency averaging identities, which the vendored file proves three times by
the same
calcandavg_congr(whose vendored tactic is not used here), share the private theorembipartiteConsError_evaluatedAtNextPoint_eq_avg, stated for any point-indexed family onF_q^{m+1}; each is that theorem by definitional equality of the restricted point measurements. idxPolyFamily_stronglySelfConsistent_of_slice_boundsand the boundedness field read the slice bounds throughavgOver_uniform_constandavgOver_mono, with nosimpa; the positivity of the slice witnesses isaverageOperatorOverDistribution_nonneg.
Not ported #
ldPastingInInductionNu_le_fifth_mainInductionNu: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/inductive_step.texblueprint/src/chapter/ch10_induction.tex
The nontrivial main-induction branch supplies the scalar side condition
ΞΆ β€ 1 needed by the averaged pasting assembly.
Paper origin: references/ldt-paper/inductive_step.tex:486-551, where the
small-error branch is the one in which the averaged self-improvement and
pasting estimates are used.
Answer-valued analogue of
selfImprovementInInductionError_le_one_of_mainInductionError_lt_one.
This is a scalar consequence of the small-error branch for an ambient answer-valued strategy. It does not use the ordinary carrier strategy and does not assert that the answer-valued diagonal measurement is controlled by an ordinary diagonal test.
The average of the answer-slice self-improvement errors is bounded by the ambient induction self-improvement error.
This is the ordinary ambient version: the restricted slices use the
answer-valued interface, but the ambient strategy is an ordinary SymStrat.
The average recursive answer-slice induction error satisfies the same bound as in the ordinary slice route.
The proof is a transport of the already checked ordinary averaging estimate through the answer-valued slice-to-ordinary data conversion.
The mass of the averaged polynomial family is the average of the masses of the slice measurements.
This is the linearity calculation underlying the completeness part of the averaged pasting assembly.
Averaged completeness of a slice-indexed polynomial family from pointwise slice completeness.
This is the completeness component of the Section 6 averaging argument. The statement is family-level: it does not mention diagonal measurements, and hence can be reused in the answer-valued successor route.
Point-consistency averaging for the slices of a self-improvement data record: the consistency of the evaluated family with the ambient point measurement is the average of the slice-wise consistencies with the restricted point measurements.
Point-consistency averaging for answer-valued restricted slices of an ordinary ambient successor strategy.
Answer-valued point-consistency averaging over the last coordinate.
This is the same Fubini/reindexing calculation as
family_pointConsistencyError_eq_avg, but for an ambient answer-valued
successor strategy. It is one of the identities needed to assemble the
answer-valued successor branch without replacing the diagonal-line answer
measurement by an ordinary polynomial-valued one.
Average slice-wise point consistency for an answer-valued successor strategy.
If the slice family is point-consistent with each answer-valued restricted
strategy at error sliceError x, and the slice errors average to at most
zeta, then the evaluated family is point-consistent with the ambient
answer-valued point measurement at error zeta.
Average slice-wise left/right closeness into strong self-consistency of the slice-indexed family.
This is the strong self-consistency component of the Section 6 averaging argument. It depends only on the state and the slice measurements, not on the diagonal part of a strategy.
Average slice-wise boundedness into the boundedness input used by the induction-section pasting theorem.
This is the boundedness component of the Section 6 averaging argument for an
ordinary successor strategy. The hypotheses are exactly the slice-wise
residual estimate and the paper domination condition
E_u A^{u,x}_{g(u)} <= Z^x.
Lean-only: This is an internal adapter for the induction-section pasting
interface, tracked in issue #1507. Paper origin:
references/ldt-paper/inductive_step.tex:461-551. Discharge: proved here by
averaging the slice-wise boundedness estimates and the domination condition.