Axis-parallel point-line self-consistency transport #
The counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/SelfConsistencyTransport/PointLine.lean
in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the point-line
consistency and rebasing interfaces used in the middle two 2ε moves of the local-variance
transport chain in lem:local-variance-of-points (expansion.tex, lines 306--307 and 309--310).
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 ported axisParallelFailureProbability being the bipartiteConsError of
the point and line answer families by definition.
The weighted base-sample estimate axisParallelBaseEventApproximation_weighted_sample is
prop:cab-approx-delta (Preliminaries.cabApproxDelta on S.toVecState) with the multiplier
S.R ((G_g)^{1/2}), as in the vendored file; the selected line event is identified with
B^ℓ_{[f(u)=g(u)]} at the base point by generalizeBLeftOutcome_base, which is new here, in
place of the vendored simp unfolding of both postprocessings.
Not ported #
axisParallelBaseLineEvent_some: a private simplification step that upstream's Lean-module port (commit5fc363b, its audit of 2026-10-03) added to the vendored proof; the port's proof goes throughgeneralizeBLeftOutcome_baseinstead.
New here #
generalizeBLeftOutcome_base: at the base point of an axis-parallel test sample, the selected outcome of the postprocessed line answer isB^ℓ_{[f(u)=g(u)]}.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/expansion.tex
The ε consistency interface for the point-line event at the base point of
an axis-parallel test sample.
For a sample (u,i), the point side is the event A^u_{g(u)} and the line side
is the line-answer event obtained by evaluating the line polynomial at the base
parameter and testing equality with g(u). This is the consistency input that
feeds the 2ε approximation step at expansion.tex, line 307; the later
edge-transport proof still has to reindex from the base-point test sampling to
an arbitrary incident pair (ℓ,u) (using axis-line rebasing covariance) and then
apply prop:simeq-to-approx/prop:cab-approx-delta.
Point-event measurement used by the base-point point-line consistency step.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Line-event measurement used by the base-point point-line consistency step.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The symmetric 2ε approximation interface for the point-line event.
This is the orientation used in expansion.tex, lines 306--307 and 309--310:
the line event is placed on the left register and the point event on the right
register. It is obtained from axisParallelBaseEventConsistency by first
swapping the two prover roles, a theorem of the symmetric model, then applying
prop:simeq-to-approx.
At the base point of an axis-parallel test sample (u,i), the selected outcome of the
postprocessed line answer is the line event B^ℓ_{[f(u)=g(u)]} of the line question
(ℓ,u), ℓ the line through u in direction i.
The selected, square-root weighted point-line approximation on the native axis-parallel base-point sample distribution.
After prop:cab-approx-delta with multiplier S.R ((G_g)^{1/2}), the swapped
base-event approximation gives the paper's line-306 to line-307 move at a
sample (u,i): the line question is represented by the rebased line with base
u and direction i.
Rebasing an incident axis-parallel line question at its sampled point does not change the evaluated line event operator.
The left operator is the event f(t)=g(ℓ(t)) for the line measurement on ℓ.
After rebasing ℓ at t, the sampled point is the new base point and the same
event is read as f(0)=g(ℓ(t)). This is exactly the strategy's axis-parallel
measurement covariance, via AxisParallelCovariantMeasurement.reparamInvariant,
and is the operator-level reindexing used in expansion.tex:300-307.
Weighted version of
generalizeBLeftOperatorAtPolynomial_rebaseAt_pointAt.
Tensoring the line event with the fixed polynomial weight (G_g)^{1/2} preserves
the rebasing equality. This is the exact weighted operator identity needed to
transport the 2ε base-point estimate to arbitrary incident line questions in
steps 2 and 5 of lem:local-variance-of-points.
The weighted line-to-point approximation after reindexing the base-point test sample to an arbitrary incident line question.
This is the paper's step 5 (expansion.tex, line 309--310), before coupling the
line question with the second endpoint of the hypercube-edge presentation: for
v ∈ ℓ, B^ℓ_[f(v)=g(v)] ⊗ (G_g)^{1/2} is 2ε-close to
I ⊗ (G_g)^{1/2} A^v_{g(v)}.
The reverse weighted point-to-line approximation after incident-line reindexing.
This is the paper's step 2 (expansion.tex, line 306--307):
I ⊗ (G_g)^{1/2} A^u_{g(u)} is 2ε-close to
B^ℓ_[f(u)=g(u)] ⊗ (G_g)^{1/2} for an incident line question (ℓ,u).