Section 12 pasting: commute G half-sandwich setup โ definitions #
Operator definitions and family constructions for the half-sandwich commutation chain, with the
small helper lemmas used by the sum-bound and step-commutation submodules: 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 slice family is an IdxPolyFamily params ๐, and the reverse half-product is a local
operator in ๐ that reads no state. The placed families take the symmetric model
S : SymModel ๐ K as their first explicit argument, in place of the vendored named carriers
(ฮนโ := ฮน), (ฮนโ := ฮน), so their outcomes are products of S.L (โฆ) and S.R (โฆ); callers write
headTailOrderedFamily strategy.state params family r where the vendored text was
headTailOrderedFamily params family r. The lemmas take the vendored state in its vendored
argument position: S : SymModel ๐ K where it carries placed families, and V : VecState K
in the same-space sddOpRel_uniform_equiv and sddOpRel_uniform_fst, to which callers pass
strategy.state or S. No vendored lemma here has a swap, density or normalization hypothesis.
The split lemmas hold by S.leftTensor_mul_leftTensor up to definitional equality, where the
vendored proofs unfold by simp; gHatSelfConsistency_sddOpRel and
commuteGHalfSandwich_move_recursive_zero hold by definitional equality and S.leftTensor_one,
S.rightTensor_one.
Not ported #
pointTupleConsEquiv: classical, imported.thirdSliceFrontEquiv: classical, imported.splitQuestionEquiv: classical, imported.prefixTripleOutcomeEquiv: classical, imported.pairTailOutcomeEquiv: classical, imported.splitSuccQuestionEquiv: classical, imported.splitSuccOutcomeEquiv: classical, imported.moveTailQuestionEquiv: classical, imported.moveTailOutcomeEquiv: classical, imported.firstSliceBackQuestionEquiv: classical, imported.firstSliceBackOutcomeEquiv: classical, imported.pointTupleOneEquiv: classical, imported.gHatTupleOutcomeOneEquiv: classical, imported.splitQuestionEquivOne: classical, imported.splitOutcomeEquivOne: classical, imported.thirdSliceFrontOutcomeEquiv: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
Sandwich-chain comparison lemmas #
These lemmas capture the infrastructure needed for the lem:commute-g-half-sandwich
through cor:h-a-consistency chain in ld-pasting.tex ยง9.3.
The n-step SDDOpRel composition lemma (sddOpRel_chain) lives in
MIPRE.LIDT.Co.Preliminaries (Co/Preliminaries/CompletionTransfer.lean) alongside
sddOpRel_triangle, since it is a general-purpose result used by multiple chapters.
Reverse-ordered half-product of completed-slice outcome operators,
\widehat G^{x_k}_{g_k} \cdots \widehat G^{x_1}_{g_1}.
Equations
- One or more equations did not get rendered due to their size.
- MIPRE.LIDT.Co.Pasting.gHatReverseHalfProductOutcomeOperator params family 0 _xs _gs = 1
Instances For
Ordered head-tail family with the head completed-slice operator followed by the remaining half-product on the left tensor register.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rotated head-tail family with the tail half-product placed before the head completed-slice operator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Move-family endpoint with two distinguished left-register factors and the reverse half-product on the right register.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Commuted endpoint obtained by interchanging the two distinguished left-register completed-slice factors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The outcomes of the (k + 1)-fold half-sandwich are those of the ordered head-tail family,
after splitting off the first coordinate of the question and outcome tuples.
The total of the (k + 1)-fold half-sandwich is that of the ordered head-tail family.
The outcomes of the rotated (k + 1)-fold half-sandwich are those of the rotated head-tail
family, after splitting off the first coordinate of the question and outcome tuples.
The total of the rotated (k + 1)-fold half-sandwich is that of the rotated head-tail
family.
Under uniform questions, an operator-family distance relation is invariant under
reindexing the questions along an equivalence e : ฮฑ โ ฮฒ.
Base cases and consistency lifts #
The self-consistency of the completed slices, as a relation between submeasurements, is the same relation between the underlying operator families.
An operator-family distance relation over uniform questions a persists when an unused
uniform coordinate b is adjoined to the question.
The commutation of completed-slice pairs, restated on the triple questions
(x, y, xs) of the move chain.
Move-step and source families #
Source family for a single move step: three distinguished completed-slice operators and the tail half-product all lie on the left tensor register.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Target family for a single move step: the exposed tail coordinate and the reverse tail half-product have been moved to the right tensor register.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Intermediate family for a move step, after the third distinguished completed-slice operator but before that operator is moved to the right.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Source endpoint of the move chain before the first tail coordinate has been exposed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Move-source splitting lemmas #
The source endpoint of the move chain is the ordered head-tail family of length r + 1,
with the second distinguished coordinate consed onto the tail.
At tail length 0 the move source and the move endpoint agree, so they are at distance
0.