Section 12 pasting: commute G half-sandwich split lemmas #
The split reindexing lemmas and the two-term base case 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 placed families are those of Setup/Definitions, which take the symmetric model
S : SymModel ๐ K as their first explicit argument. The lemmas take S in the vendored state's
argument position, second, after params, as the split lemmas of Setup/Definitions do: the
outcome lemmas gHatHalfSandwich{Left,Right}_split_outcome_cons and
headTail{Ordered,Rotated}Family_split_one_outcome, whose vendored versions have no state, gain
it there, and commuteGHalfSandwich_split_iff, commuteGHalfSandwich_split_one_iff and
commuteGHalfSandwich_core_two take it where the vendored ฯbi was. No vendored lemma here has
a swap, density or normalization hypothesis.
The one-tuple outcome lemmas hold by S.leftTensor_mul_leftTensor and mul_one up to
definitional equality, where the vendored proofs unfold by simp. In
commuteGHalfSandwich_core_two, the bound ฮฝโ โค 426 ยท 2ยฒ ยท m ยท (โฆ) uses that each sixteenth
root is nonnegative (rpow_oneSixteenth_nonneg), rather than the nonnegativity of the averaged
hypothesis.
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 outcomes of the (k + 1)-fold half-sandwich at the consed question and outcome are
those of the ordered head-tail family.
The outcomes of the rotated (k + 1)-fold half-sandwich at the consed question and outcome
are those of the rotated head-tail family.
At tail length one, the ordered head-tail family is the ordered pair product.
At tail length one, the rotated head-tail family is the reversed pair product.
The half-sandwich commutation relation on (k + 1)-tuples is equivalent to the head-tail
relation obtained by splitting off the first coordinate.
At tail length one, the head-tail commutation relation is equivalent to the commutation of completed-slice pairs.
Base case k = 2 of the half-sandwich commutation: the commutation of completed-slice pairs
gives the commutation of the two-fold half-sandwich at the displayed error.