Axis-parallel point-line self-consistency transport #
This module contains 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 ε 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.
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 using the symmetric strategy state, then applying
prop:simeq-to-approx.
The selected, square-root weighted point-line approximation on the native axis-parallel base-point sample distribution.
After prop:cab-approx-delta with multiplier I ⊗ (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).