The seeded-CL adapter, part 4: the question and answer maps #
The reduction plays a strategy for the seeded CL test as a strategy for the canonical-line
test, through MIPRE.TensorProductStrategy.adapt. That needs two maps, and this file defines
them and the bookkeeping that identifies them.
qmap hm σ sends a question of the canonical-line test to the seeded question it is played
through:
- a point
uto the pointρ u, reversal exchanging the two diagonal conventions; - an axis-parallel line to
(ρ ℓ.1, s)— norepis needed, the two tests' base points agree exactly there — withsthe chosen seed of the fibre overrev (axisIdx ℓ); - a diagonal line to
(rep (ρ ℓ.2) (ρ ℓ.1), s, ρ ℓ.2), carrying the direction unrescaled. That is legitimate because the seeded test'sDLinequestions carry the raw direction, and it is what makes the answer conversion a pure shift rather than a shift and a scaling.
amap sends a seeded answer to a canonical-line answer, and depends on the question — the
shift does. Its unreachable branches are unreachable because clGame rejects an answer
whose format does not match its question's type; before that was repaired the branches would
have been live.
shiftOf ℓ is the shift, read off rep_eq: the two base points differ by shiftOf ℓ times the
direction (rep_rev_eq), so the two parameters of a point of the line differ by shiftOf ℓ.
Reading the direction off a line #
A default index, for the branches of the maps below that the support never reaches.
Equations
Instances For
The direction index of an axis-parallel line.
Equations
- MIPRE.LIDT.Adapter.axisIdx ℓ = if h : ∃ (i : Fin m), ℓ.2 = Pi.single i 1 then h.choose else MIPRE.LIDT.Adapter.idx0
Instances For
The χ-index the adapter uses for a diagonal line: the first nonzero coordinate of the
reversed direction, which is the pivot of its span and so the coordinate rep zeroes.
The fallback for a singleton line (direction zero) is rev idx0 = m - 1, not idx0, and the
choice is forced by the weight bookkeeping rather than free. The seeded test's DLine samples
with zeroBelow (χ s) V = 0 number q^{χ s}, so its mass on (u₀, s, 0) grows with χ s;
the canonical-line test puts mass ≈ 1/(6 m q^m q) on a singleton line, which only the largest
χ can dominate. Sending singleton lines to χ = 0 costs a factor q^{m-1}, which the error
term of thm:lidt-cl-soundness does not allow. See planning/lidt-cl-adapter.md.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The shift between the two presentations of a line.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The seeded test's base point, in terms of the shift #
canonLin of the zero subspace is the identity: there are no pivots.
The two maps #
The seeded question a canonical-line question is played through, for the seed choice σ and
the direction scale c.
The scale is averaged over along with the seed, and it has to be: the seeded test's DLine
questions carry the raw direction, so one geometric line has q - 1 of them, and an adapter
using only one would concentrate its push-forward on a 1/(q-1) fraction of them and need a
q-dependent constant. See the second correction in planning/lidt-cl-adapter.md.
Scaling the direction does not move the base point, rep depending only on the span.
Equations
- One or more equations did not get rendered due to their size.
- MIPRE.LIDT.Adapter.qmap hm σ c (MIPRE.LIDT.Question.point u) = MIPRE.LIDT.CL.Question.point (MIPRE.LIDT.Adapter.revPoint u)
Instances For
The canonical-line answer a seeded answer becomes. It depends on the question because the
shift does, and on the scale c; the branches not listed are the ones clGame rejects on
format.
A point of the line at the target's parameter t sits at the source's parameter
(t + shiftOf ℓ) / c, so the substitution to undo is t ↦ c⁻¹ t + c⁻¹ · shiftOf ℓ.
Equations
- MIPRE.LIDT.Adapter.amap c (MIPRE.LIDT.Question.point u) (MIPRE.LIDT.CL.Answer.values a) = MIPRE.LIDT.Answer.value (a 0)
- MIPRE.LIDT.Adapter.amap c (MIPRE.LIDT.Question.axisLine ℓ) (MIPRE.LIDT.CL.Answer.apolys f) = MIPRE.LIDT.Answer.axisPoly (f 0)
- MIPRE.LIDT.Adapter.amap c (MIPRE.LIDT.Question.diagLine ℓ) (MIPRE.LIDT.CL.Answer.dpolys f) = MIPRE.LIDT.Answer.diagPoly (MIPRE.LIDT.Adapter.reparam c⁻¹ (c⁻¹ * MIPRE.LIDT.Adapter.shiftOf ℓ) (f 0))
- MIPRE.LIDT.Adapter.amap c x✝¹ x✝ = MIPRE.LIDT.Answer.value 0
Instances For
The support of the canonical-line test's distribution #
Transporting membership through the reversal #
Reading the answer format off the acceptance #
hD: acceptance survives the two maps #
One lemma per case of Sample, since the source's acceptance says something different in each.
The self-consistency case: both players are asked the same point, and both tests check that the two answers agree.
The axis-parallel case: the source checks the point is on the seeded line and the answer evaluates correctly there, and after reversal that is the same equation the target checks.
The diagonal case, and the one the affine rebasing exists for. The two tests' base points
differ by shiftOf ℓ times the direction and the directions by the scale c, so the point at
the target's parameter t sits at the source's (t + shiftOf ℓ) / c; reparam c⁻¹ (c⁻¹ · shiftOf ℓ)
undoes exactly that, through the general two-parameter reparam.
The swapped cases #
Each test hands the line to either player, so the two mirrored cases have to be done too. The proofs are the previous two with the roles exchanged; both games' predicates carry the mirrored clause explicitly.
hD_axis with the players exchanged.
hD_diag with the players exchanged.
hD, assembled #
The five cases above are exactly the five shapes a question pair of positive weight can have, so
this is the hypothesis MIPRE.TensorProductStrategy.one_sub_value_adapt_le asks for. Note it is
asked only on the support: off it the claim is false, since a pair of two line questions is a
real question pair of the seeded test and the canonical-line test has no subtest for it.