Section 10 — commutativity points approximation layer #
Restricted-diagonal approximation infrastructure for commutativity at points: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/CommutativityPoints/Approximation.lean in the port of
planning/c6b-plan.md (milestone M1, section "Port conventions"). The diagonal branch of the
low individual degree test is evaluated at its last restriction index and transported to the
shared point-with-diagonal-line distribution, for a symmetric strategy
strategy : SymStrat params 𝔓 K and for an answer-valued one
strategy : AnswerSymStrat params 𝔓 K; the point answers are placed by strategy.state.L, the
line answers by strategy.state.R.
The classical half of the vendored file (the last restriction index, the decompositions of a
next-level point, and the equivalences between restricted diagonal samples, diagonal lines and
rebased questions) is not ported: this file imports the vendored file and names those
declarations through an explicit open MIPStarRE.LDT.CommutativityPoints (…) list.
opFamilyOfOutcome is ported, generic over an additive monoid R of operators (the vendored
Op ι); downstream it is applied to joint operators K →L[ℂ] K.
Not ported #
pointNextEquiv: classical, imported.avgOver_uniform_pointNext_decompose: classical, imported.avgOver_uniform_pointNext_height: classical, imported.pointPairOutcomeSwapEquiv: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/commutativity-points.texblueprint/src/chapter/ch08_commutativity.tex
In this repository: lem:co-commutativity-points in blueprint/src/content/08_downstream.tex.
The final restriction index, corresponding to the paper's m-restricted diagonal-lines test.
Upstream keeps it private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the
port carries its own copy.
Instances For
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.
At the final restriction index, a restricted diagonal direction records all
m coordinates, so it is equivalent to an unrestricted point of Point params.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.
At the final restriction index, a restricted diagonal sample is exactly a full diagonal line: the sample point becomes the base point and the restricted direction determines all line coefficients.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.
Rebase the last restricted diagonal sample so that its distinguished base point appears at the queried parameter. This identifies the corrected diagonal test sample space with the shared point-with-diagonal-line questions used in the commutativity-at-points argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Build an operator family from its outcomes, taking the total to be their sum.
Equations
- MIPRE.LIDT.Co.CommutativityPoints.opFamilyOfOutcome outcome = { outcome := outcome, total := ∑ a : Outcome, outcome a }
Instances For
Evaluate each restricted diagonal measurement at the distinguished base
parameter zeroCoord, matching the corrected paper definition of the diagonal
branch.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Consistency transfer for the corrected diagonal branch at the final restriction index.
The corrected test samples a restricted diagonal line and compares the point
measurement at its distinguished base point with the diagonal measurement
postprocessed by evaluation at zeroCoord. The global diagonal-line test bound
therefore controls this last restricted slice in particular.
Convert the corrected restricted diagonal consistency estimate into the corresponding SDD approximation bound.
This is the final-slice version of the diagonal branch that feeds the
commutativity-at-points argument. It packages the consistency estimate through
Preliminaries.simeqToApprox.
Transport the corrected restricted-diagonal approximation bound to the shared point-with-diagonal-line distribution used downstream.
The reindexing runs through rebasedLastRestrictedQuestionEquiv, which turns a
restricted sample together with an evaluation parameter into the corresponding
rebased diagonal-line question.
Evaluate each answer-valued restricted diagonal measurement at the
distinguished base parameter zeroCoord.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The answer-valued diagonal-line test controls the final restricted diagonal slice.
The answer-valued restricted diagonal test gives the same SDD approximation at the final restriction index as the ordinary diagonal test.
Answer-valued version of
sampledDiagonalLineApproximation_pointWithDiagonalLine.
This is the Section 10 diagonal approximation needed by the answer-valued commutativity route: it uses the answer-valued diagonal verifier relation directly and does not pass through an ordinary dummy diagonal measurement.