Section 12 pasting: commute G half-sandwich move lemmas #
The move-chain lemmas for the half-sandwich commutation chain: the counterpart of the vendored
file of the same path under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of
planning/c6b-plan.md (milestone M11, section "Port conventions"). The split reindexing lemmas
and the two-term base case are in StepLemmas/Split.
The placed families are those of Setup/Definitions, which take the symmetric model
S : SymModel 𝔓 K as their first explicit argument. Every lemma here takes S where the vendored
ψbi was, second, after params: gHatSelfConsistency_sddOpRel_quadThird params S family zeta r hsc, commuteGHalfSandwich_step_commute params S family gamma zeta r hcom,
commuteGHalfSandwich_prefixFirstSliceLeft_move params S family r δ hAB and
commuteGHalfSandwich_moveStepMid_toTarget params S family zeta r hsc. No vendored lemma here has
a swap, density or normalization hypothesis.
Each move is the vendored one: a sandwich by an auxiliary family C of contraction norm at most
one (Preliminaries.cabApproxDelta_raw), a reindexing of the outcomes
(CommutativityPoints.sddOpRel_reindex) and an identification of the outcomes
(CommutativityPoints.sddOpRel_congr_outcome). The identifications, which the vendored proofs
carry out by simp and calc chains through the Kronecker identities, are here one rewrite each by
S.leftTensor_mul_leftTensor, S.rightTensor_mul_leftTensor_eq_opTensor or S.L_comm_R, the
reindexed families unfolding by definitional equality. The contraction bounds on a single
placement are the private sum_star_leftTensor_mul_le_one and sum_star_rightTensor_mul_le_one.
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/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
The self-consistency of the completed slices, restated on the quadruple questions
(x₁, x₂, x₃, xs) with the slice read at the third coordinate.
The commutation of completed-slice pairs, sandwiched by the reverse half-product on the right register: the move family and the commuted family are at the commutation error.
A move-source comparison lifts, after left multiplication by the completed slice at a new first question coordinate, to the move-step source and middle families.
The self-consistency of the completed slices moves the third distinguished factor of the move-step middle family from the left register to the right one, at the self-consistency error.