Sum-form (cardinality-free) 2ε axis-parallel consistency endpoints #
The counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/SelfConsistencyTransportSum.lean
in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the
polynomial-sum (unnormalized ∑_g) analogues of the per-g 2ε endpoints of
SelfConsistencyTransport/PointLine.lean. They keep the answer space at Fq params rather than
postprocessing to the per-g Option Unit event, and group polynomials by the common value
g(u) through the cabApproxDelta multiplier if a = g s.1 then S.R ((G_g)^{1/2}) else 0
(cabApproxDelta_sum_from_sdd). With the contraction ∑_{g : g(u) = a} G_g ≤ I this gives 2ε
for the whole polynomial sum, with no polynomial-cardinality loss: the steps 2 and 5 sum-level
inputs to eq:equivalent-local-variance (references/ldt-paper/expansion.tex:317--321).
The vendored swap of the two prover roles, consRel_symm_of_density_fixed applied to
strategy.densityFixed, is the model's theorem SymModel.consRel_symm_of_density_fixed, so no
swap hypothesis appears; the axis-parallel consistency hypothesis is the axisParallelTest field
of IsGood itself. The base-sample sum bound is a single application of
cabApproxDelta_sum_from_sdd, its two bridges being S.rightTensor_mul_leftTensor_eq_opTensor
after liftLeft_lineAnswerMeasurement_outcome_at_g, and S.rightTensor_mul_rightTensor.
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/expansion.tex
The point answers of the axis-parallel test, s ↦ A^{s.1}, as an indexed measurement.
Equations
- MIPRE.LIDT.Co.GlobalVariance.axisParallelPointAnswerMeasurement params strategy s = (MIPRE.LIDT.Co.axisParallelPointAnswerFamily strategy s).toMeasurement ⋯
Instances For
The line answers of the axis-parallel test, evaluated at the base point, as an indexed measurement.
Equations
- MIPRE.LIDT.Co.GlobalVariance.axisParallelLineAnswerMeasurement params strategy s = (MIPRE.LIDT.Co.axisParallelLineAnswerFamily strategy s).toMeasurement ⋯
Instances For
The lifted line-answer family outcome at value a = g(s.1) is the left placement of the
lem:generalize-b left operator at the incident question (ℓ, s.1) with
ℓ = {base := s.1, direction := s.2}.
This is the operator identity bridging the un-postprocessed Fq params-valued
line answer family to the per-g line operator used in
weightedGeneralizeBLeftOperatorAtPolynomial; it is generalizeBLeftOutcome_base after
collapsing the postprocessing to the event a = g(s.1).
The lifted point-answer family outcome at value a = g(s.1) is the right placement of the
point-conditioned operator at the base point s.1.
Sum-level base-sample form of the 2ε axis-parallel consistency move,
oriented with the line event on the left register and the point event on the
right register.
This is the polynomial-sum version of
axisParallelBaseEventApproximation_weighted_sample: instead of fixing g
and postprocessing both sides to the Option Unit event a = g(u), we keep
the full Fq params answer space and use the multiplier
C s a g := if a = g s.1 then S.R ((G_g)^{1/2}) else 0 inside
prop:cab-approx-delta. The contraction ∀ s a, ∑_g (C s a g)† * (C s a g) ≤ I is
rightPolynomialWeightSqrt_grouped_contraction, from the submeasurement
inequality ∑_{g : g(s.1) = a} G_g ≤ I. Consequently the bound is 2ε for
the polynomial sum, with no polynomial-cardinality loss.
Sum-level form of the weighted line-to-point approximation
(expansion.tex:309--310, paper step 5) on the
axisParallelLineQuestionDistribution distribution.
This is the polynomial-sum analogue of
axisParallelPointLineConsistency_weighted_leftToRightLineQuestion. After
reindexing the line-question sampling along its incident-pair structure (using
the rebasing covariance of the line operator), it reduces to the
sum-level base-sample bound axisParallelBaseEventApproximation_weighted_sample_sum.
Sum-level form of the reverse weighted point-to-line approximation
(expansion.tex:306--307, paper step 2) on the
axisParallelLineQuestionDistribution distribution.
This is the polynomial-sum analogue of
axisParallelPointLineConsistency_weighted_rightToLeftLineQuestion. Each
summand is unchanged after swapping the two endpoint operators, so this reduces
to axisParallelPointLineConsistency_weighted_leftToRightLineQuestion_sum.