Add-in-u Cauchy--Schwarz algebraic alignment #
Operator identities that align the differences of the add-in-u scalar chains with the forms
used in the Cauchy--Schwarz estimates of the paper: the counterpart of the vendored
SelfImprovement/Theorems/Results/AddInUStep12/Algebra.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
Contents #
addInU_step1_pointwise_op_eqโฆaddInU_step4_pointwise_op_eq: the operator-level difference identities for the four scalar moves, as identities inK โL[โ] KbetweenS.opTensor,S.LandS.Rterms. They take the model(S : SymModel ๐ K)as an explicit first argument and local operators๐, where the vendored lemmas are generic over a finite carrierฮบ. The vendored proofs compute withopTensor_mulandsimp [Matrix.mul_assoc]; here they are rewrites with the keystone's oriented placement lemmas (leftTensor_mul_opTensor,rightTensor_mul_opTensor,opTensor_mul_leftTensor,opTensor_sub_left) andmul_assoc.addInU_cs_chain_step1_diff_eqโฆaddInU_cs_chain_step4_diff_eqand their reverse forms: the differences of the diagonal chainaddInUCSChainQ0โQ4in commutator-times-PSD form.addInU_selected_cs_chain_step1_diff_eqโฆaddInU_selected_cs_chain_step4_diff_eqand their reverse forms: the same identities for the selected chainaddInUSelectedCSChainQ0โQ4.
Every scalar is strategy.state.ev of a joint operator; leftTensor A, rightTensor A and
opTensor A B are strategy.state.L A, strategy.state.R A and strategy.state.opTensor A B.
No statement carries a swap, density or normalization hypothesis, and none of the vendored ones
did.
The vendored file imports SelfImprovement/Theorems/Thresholds/Final.lean, wholly classical and
without a Co file; so does this 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/self_improvement.texlines 255โ297blueprint/src/chapter/ch07_self_improvement.tex
Algebraic CS-alignment for the add-in-u Step 1/2 differences #
Pure operator-algebra rewrites that bring the differences addInUCSChainQ1 - addInUCSChainQ0
and addInUCSChainQ2 - addInUCSChainQ1 into the shapes required by the paper's
Cauchy--Schwarz steps eq:move-one-cauchy-schwarz and eq:move-another-cauchy-schwarz
(self_improvement.tex, lines 261--266 and 285--289). The reverse-difference companions give
the downstream orientation Qโ - Qโ and Qโ - Qโ.
They do not discharge the Cauchy--Schwarz estimate itself; they reduce the raw
|Qโ - Qโ| โค โ(2ฮด) and |Qโ - Qโ| โค โ(2ฮด) bounds to a sandwich-form Cauchy--Schwarz on the
resulting D ยท (M^u_h โ T_h) ยท D' expression, plus the two square-root inputs
addInU_pointMeasurement_snd_selfConsistency and
addInU_filtered_sandwiched_tensor_sum_le_one.
Operator identity for the Qโ โ Qโ move:
(A^v M) โ (T A^v) โ M โ (A^v T A^v) = (A^v โ I โ I โ A^v) ยท (M โ T) ยท (I โ A^v).
Operator identity for the Qโ โ Qโ move:
(A^v M A^v) โ T โ (A^v M) โ (T A^v) = (A^v โ I) ยท (M โ T) ยท (A^v โ I โ I โ A^v).
Operator algebra reduction for the Qโ โ Qโ add-in-u step.
The operator difference of the bipartite-tensor expectations of
A^v ยท H^u_h ยท A^v and A^u ยท H^u_h ยท A^v (with shared right factor T_h)
factors as (A^v โ A^u) ยท H^u_h ยท A^v on the left tensor factor, leaving the
right factor T_h untouched.
Operator algebra reduction for the Qโ โ Qโ add-in-u step.
The operator difference of the bipartite-tensor expectations of
A^u ยท H^u_h ยท A^v and A^u ยท H^u_h ยท A^u (with shared right factor T_h)
factors as A^u ยท H^u_h ยท (A^v โ A^u) on the left tensor factor, leaving the
right factor T_h untouched.
Algebraic CS-alignment for the Qโ โ Qโ step.
Rewrites the difference addInUCSChainQ1 - addInUCSChainQ0 in the exact form
appearing on the LHS of eq:move-one-cauchy-schwarz (paper lines 261--266):
the inner-product of the commutator
A^v_{h(v)} โ I โ I โ A^v_{h(v)} with M^u_h โ T_h ยท (I โ A^v_{h(v)}),
averaged over (u, v) and summed over h.
This identity is purely algebraic; the actual โ(2ฮด) bound still requires
the operator Cauchy--Schwarz step plus
addInU_pointMeasurement_snd_selfConsistency.
Algebraic CS-alignment for the Qโ โ Qโ step.
Rewrites the difference addInUCSChainQ2 - addInUCSChainQ1 in the exact form
appearing on the LHS of eq:move-another-cauchy-schwarz (paper lines 285--289):
the inner-product of (A^v_{h(v)} ยท M^u_h) โ T_h with the commutator
A^v_{h(v)} โ I โ I โ A^v_{h(v)}, averaged over (u, v) and summed over h.
The Lean statement keeps the equivalent factored form
(A^v_{h(v)} โ I) ยท (M^u_h โ T_h) before the commutator.
This identity is purely algebraic; the actual โ(2ฮด) bound still requires
the operator Cauchy--Schwarz step plus
addInU_pointMeasurement_snd_selfConsistency and
addInU_filtered_sandwiched_tensor_sum_le_one.
Reverse-orientation form of addInU_cs_chain_step1_diff_eq.
This is the same algebraic identity as the Qโ โ Qโ rewrite, stated in the
Qโ - Qโ orientation used by the later absolute-value chain.
Reverse-orientation form of addInU_cs_chain_step2_diff_eq.
This is the same algebraic identity as the Qโ โ Qโ rewrite, stated in the
Qโ - Qโ orientation used by the later absolute-value chain.
Algebraic CS-alignment for the Qโ โ Qโ step.
Rewrites the difference addInUCSChainQ2 - addInUCSChainQ3 in the exact form
appearing on the LHS of eq:change-one-cauchy-schwarz (paper lines 306--311):
the expectation of ((A^v_{h(v)} - A^u_{h(u)}) ยท H^u_h ยท A^v_{h(v)}) โ T_h,
averaged over (u, v) and summed over h.
The paper writes the middle factor as the fiber operator M^u_o; in this
formalization the preceding o-sum has already been collapsed along
o = h(u), so the same factor appears as
H^u_h = (sandwichedPolynomialSubMeasAt params strategy T u).outcome h.
This identity is purely algebraic; the operator Cauchy--Schwarz estimate is
proved downstream by add_in_u_cs_chain_q2_q3_factored_cs.
Selection-parametrized Step 1/2 algebraic identities #
Algebraic CS-alignment for the selected Qโ โ Qโ step.
This is the selection-parametrized form of addInU_cs_chain_step1_diff_eq.
The identity is stated in the same orientation as the diagonal chain, namely
as Qโ - Qโ. It rewrites the scalar difference using the same commutator
A^v_{h(v)} โ I โ I โ A^v_{h(v)}, but sums only over the selected pairs
(o,h) โ S_u and leaves the arbitrary outcome operator M^u_o in place.
Algebraic CS-alignment for the selected Qโ โ Qโ step.
This is the selection-parametrized form of addInU_cs_chain_step2_diff_eq,
with the arbitrary selected outcome operator M^u_o in the left tensor factor.
Reverse-orientation selected form of addInU_selected_cs_chain_step1_diff_eq.
Reverse-orientation selected form of addInU_selected_cs_chain_step2_diff_eq.
Algebraic CS-alignment for the selected Qโ โ Qโ step.
This rewrites the first point-replacement move for an arbitrary selected
outcome family. The only changed factor is the left copy of the point
projector, from A^v_{h(v)} to A^u_{h(u)}.
Algebraic CS-alignment for the selected Qโ โ Qโ step.
This rewrites the second point-replacement move for an arbitrary selected
outcome family. The only changed factor is the right copy of the point
projector, from A^v_{h(v)} to A^u_{h(u)}.
Reverse-orientation selected form of addInU_selected_cs_chain_step3_diff_eq.
Reverse-orientation selected form of addInU_selected_cs_chain_step4_diff_eq.
Algebraic CS-alignment for the Qโ โ Qโ step.
Rewrites the difference addInUCSChainQ3 - addInUCSChainQ4 in the exact form
appearing on the left-hand side of eq:change-another (paper lines 326--332):
the expectation of (A^u_{h(u)} ยท H^u_h ยท (A^v_{h(v)} - A^u_{h(u)})) โ T_h,
averaged over (u, v) and summed over h.
This identity is purely algebraic; the actual operator Cauchy--Schwarz step
is provided by add_in_u_cs_chain_q3_q4_factored_cs.