The seeded-CL adapter, part 1: the two games describe the same lines

The seeded CL test MIPRE.LIDT.CL.clGame and the canonical-line test MIPRE.LIDT.lidtGame present a line differently, and the adapter of planning/lidt-cl-adapter.md has to know that the two presentations agree where they should. This file settles the axis-parallel case, which is the one that needs the canonical representative of def:cl-canonical to be computed rather than used abstractly.

The seeded test's base point for direction w is rep w u = canonLin (span {w}) u, the canonical linear map with kernel span {w} applied to u. The canonical-line test's is the first component of Line.through u w, which for a normalized direction moves u so that the coordinate of the direction's first nonzero entry vanishes. For w = eᵢ both are u - uᵢ • eᵢ (rep_single, through_single), so on axis-parallel lines the two games agree on the base point exactly, with no choice involved. The seed is the only thing the seeded question carries beyond the line.

Getting rep to compute means computing the pivot set: pivots (span {eᵢ}) = {i} (pivots_line), from the dimension sequence dim (span {eᵢ} ⊓ tail n k), which is 1 for k ≤ i (inf_tail_of_le) and 0 above (inf_tail_of_gt), so the sequence drops exactly at i. card_pivots then pins the set, since a line has rank one.

projection_eq_of is the uniqueness of a complementary decomposition, stated as a rewriting rule because that is how canonLin is pinned down: canonLin S u is the element of the canonical complement congruent to u modulo S.

Two further discrepancies are settled here, both of them differences of presentation rather than of content.

The diagonal convention. The seeded test's diagonal directions have their first i coordinates zero (CL.zeroBelow), the canonical-line test's have their coordinates past j zero (Sample.extend). Coordinate reversal exchanges them, and is the ρ of the paper's own reduction, there for the same reason against the tensor code test.

The direction scale. A DLine question of the seeded test carries the direction itself, scale included, while the canonical-line test normalizes it. So the seeded questions (u₀, s, c • w), c ≠ 0, all describe one canonical line, and an answer in the parameter of u₀ + t (c • w) has to be reparametrized. The parameter scales inversely and the polynomial follows by rescale, which is a bijection of the coefficient vectors preserving the degree bound --- so no answer alphabet changes and no degree is lost.

What is not here is the reconciliation of CL.lineParam with Line.param, the last of the geometric discrepancies, nor anything about strategies or values.

The pivot set of a coordinate line

theorem MIPRE.LIDT.Adapter.inf_tail_of_le {F : Type u_1} [Field F] {n : ℕ} (i : Fin n) (k : ℕ) (hk : k ≤ ↑i) : F ∙ Pi.single i 1 ⊓ CL.tail n k = F ∙ Pi.single i 1

The coordinate line span {eᵢ} meets tail n k in itself when k ≤ i: a multiple of eᵢ has all its other coordinates zero already.

theorem MIPRE.LIDT.Adapter.inf_tail_of_gt {F : Type u_1} [Field F] {n : ℕ} (i : Fin n) (k : ℕ) (hk : ↑i < k) : F ∙ Pi.single i 1 ⊓ CL.tail n k = ⊥

And meets it in ⊥ when k > i: the i-th coordinate is then forced to vanish.

theorem MIPRE.LIDT.Adapter.single_ne_zero {F : Type u_1} [Field F] {n : ℕ} (i : Fin n) : Pi.single i 1 ≠ 0

theorem MIPRE.LIDT.Adapter.finrank_line {F : Type u_1} [Field F] {n : ℕ} (i : Fin n) : Module.finrank F ↥(F ∙ Pi.single i 1) = 1

theorem MIPRE.LIDT.Adapter.pivots_line {F : Type u_1} [Field F] {n : ℕ} (i : Fin n) : CL.pivots (F ∙ Pi.single i 1) = {i}

The pivot set of a coordinate line is the coordinate. The dimension sequence of span {eᵢ} is 1 up to i and 0 after it, so it drops exactly once, at i; and a line has one pivot in all, by card_pivots.

The two base points

theorem MIPRE.LIDT.Adapter.projection_eq_of {F : Type u_1} [Field F] {E : Type u_2} [AddCommGroup E] [Module F E] {p q : Submodule F E} (hpq : IsCompl p q) {x y : E} (hy : y ∈ p) (hxy : x - y ∈ q) : (p.projection q hpq) x = y

Uniqueness of the decomposition along complementary submodules, as a rewriting rule: an element of p congruent to x modulo q is the projection of x. This is how canonLin is computed, since canonLin S is the projection onto the canonical complement along S.

theorem MIPRE.LIDT.Adapter.rep_single {F : Type u_1} [Field F] {n : ℕ} (i : Fin n) (u : Fin n → F) : (CL.canonLin (F ∙ Pi.single i 1)) u = u - u i • Pi.single i 1

The seeded test's canonical base point for an axis-parallel direction: rep eᵢ u zeroes the i-th coordinate of u.

theorem MIPRE.LIDT.Adapter.through_single {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] (i : Fin n) (u : Fin n → F) : Line.through u (Pi.single i 1) = (u - u i • Pi.single i 1, Pi.single i 1)

The canonical-line test's presentation of an axis-parallel line: the direction is already normalized, so it is unchanged, and the base point zeroes the i-th coordinate.

Coordinate reversal, and the two diagonal conventions

The seeded test's diagonal directions have their first i coordinates zero (CL.zeroBelow); the canonical-line test's have their coordinates past j zero (Sample.extend). Coordinate reversal exchanges the two, and is the ρ of the paper's own reduction (there it exchanges the seeded test's convention with the tensor code test's, for the same reason).

def MIPRE.LIDT.Adapter.revPoint {F : Type u_1} {n : ℕ} : (Fin n → F) ≃ (Fin n → F)

Coordinate reversal of F^n, an involution.

Equations

• MIPRE.LIDT.Adapter.revPoint = { toFun := fun (x : Fin n → F) (j : Fin n) => x j.rev, invFun := fun (x : Fin n → F) (j : Fin n) => x j.rev, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MIPRE.LIDT.Adapter.revPoint_apply {F : Type u_1} {n : ℕ} (x : Fin n → F) (j : Fin n) : revPoint x j = x j.rev

@[simp]

theorem MIPRE.LIDT.Adapter.revPoint_revPoint {F : Type u_1} {n : ℕ} (x : Fin n → F) : revPoint (revPoint x) = x

@[simp]

theorem MIPRE.LIDT.Adapter.revPoint_add {F : Type u_1} [Field F] {n : ℕ} (x y : Fin n → F) : revPoint (x + y) = revPoint x + revPoint y

@[simp]

theorem MIPRE.LIDT.Adapter.revPoint_smul {F : Type u_1} [Field F] {n : ℕ} (c : F) (x : Fin n → F) : revPoint (c • x) = c • revPoint x

@[simp]

theorem MIPRE.LIDT.Adapter.revPoint_sub {F : Type u_1} [Field F] {n : ℕ} (x y : Fin n → F) : revPoint (x - y) = revPoint x - revPoint y

theorem MIPRE.LIDT.Adapter.revPoint_single {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] (i : Fin n) : revPoint (Pi.single i 1) = Pi.single i.rev 1

Reversal sends the i-th coordinate direction to the rev i-th.

theorem MIPRE.LIDT.Adapter.revPoint_rep_single {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] (i : Fin n) (u : Fin n → F) : revPoint ((CL.canonLin (F ∙ Pi.single i.rev 1)) (revPoint u)) = (CL.canonLin (F ∙ Pi.single i 1)) u

Reversal exchanges the two tests' base points on an axis-parallel line. The adapter sends the canonical line through u in direction eᵢ to a seeded question with base point rep e_{rev i} (ρ u); reversing that back gives exactly the base point the seeded test produces for the unreversed data. This is the form the weight bookkeeping needs, since the seeded test's own samples carry the unreversed point.

The direction scale

A DLine question of the seeded test carries the direction v' itself, scale included, while the canonical-line test normalizes the direction. So one canonical diagonal line is described by the seeded questions (u₀, s, c • w) for every c ≠ 0, and an answer given in the parameter of u₀ + t (c • w) has to be reparametrized into that of u₀ + t w; rescale does it for the polynomial.

def MIPRE.LIDT.Adapter.rescale {F : Type u_1} [Field F] (c : F) {k : ℕ} (f : LinePoly F k) : LinePoly F k

Rescaling the variable of a polynomial: rescale c f is t ↦ f (c t), on coefficients.

Equations

• MIPRE.LIDT.Adapter.rescale c f i = f i * c ^ ↑i

@[simp]

theorem MIPRE.LIDT.Adapter.eval_rescale {F : Type u_1} [Field F] (c : F) {k : ℕ} (f : LinePoly F k) (t : F) : (rescale c f).eval t = f.eval (c * t)

theorem MIPRE.LIDT.Adapter.find_smul {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {c : F} (hc : c ≠ 0) {w : Fin n → F} (hex : ∃ (j : Fin n), w j ≠ 0) (hex' : ∃ (j : Fin n), (c • w) j ≠ 0) : Fin.find (fun (j : Fin n) => (c • w) j ≠ 0) hex' = Fin.find (fun (j : Fin n) => w j ≠ 0) hex

Scaling the direction does not move the first nonzero coordinate.

The two parameter conventions

CL.lineParam u₀ w x divides by the direction's first nonzero coordinate; Line.param ℓ x reads off that coordinate of x, which is correct only because the canonical-line test's directions are normalized and its base points vanish there. Both compute the parameter t of a point u₀ + t w on the line, and that is the form in which they can be compared.

theorem MIPRE.LIDT.Adapter.lineParam_eq_of_mem {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {w : Fin n → F} (hw : ∃ (j : Fin n), w j ≠ 0) (u₀ : Fin n → F) (t : F) : CL.lineParam u₀ w (u₀ + t • w) = t

CL.lineParam recovers the parameter of a point on the line.

theorem MIPRE.LIDT.Adapter.param_through_eq_of_mem {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {v : Fin n → F} (hv : ∃ (j : Fin n), v j ≠ 0) (u : Fin n → F) (t : F) : (Line.through u v).param ((Line.through u v).1 + t • (Line.through u v).2) = t

And so does Line.param, on the canonical presentation the canonical-line test uses: the direction's first nonzero coordinate is 1 and the base point vanishes there, which is what makes reading off that one coordinate correct.

The seeded test's canonical representative, in general

rep w x zeroes the coordinate of x at the first nonzero coordinate of w. Under reversal, the first nonzero coordinate of ρ dir is the reversal of the last nonzero coordinate of dir, whereas Line.through zeroes the coordinate at the first nonzero coordinate of dir. So on a diagonal line the two tests pick different base points, and the reparametrization between their answer polynomials is affine rather than linear --- this is the "canonicalization and rebasing" of rem:lidt-cl-adapter. On an axis-parallel line the first and last nonzero coordinates coincide and the shift vanishes, which is why the two base points agree there.

theorem MIPRE.LIDT.Adapter.pivots_span_singleton {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {w : Fin n → F} (hw : ∃ (j : Fin n), w j ≠ 0) : CL.pivots (F ∙ w) = {Fin.find (fun (j : Fin n) => w j ≠ 0) hw}

The pivot set of any line is its direction's first nonzero coordinate.

theorem MIPRE.LIDT.Adapter.rep_eq {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {w : Fin n → F} (hw : ∃ (j : Fin n), w j ≠ 0) (x : Fin n → F) : (CL.canonLin (F ∙ w)) x = x - (x (Fin.find (fun (j : Fin n) => w j ≠ 0) hw) / w (Fin.find (fun (j : Fin n) => w j ≠ 0) hw)) • w

The seeded test's base point, in closed form.

theorem MIPRE.LIDT.Adapter.rep_add_smul {F : Type u_1} [Field F] {n : ℕ} (w x : Fin n → F) (t : F) : (CL.canonLin (F ∙ w)) (x + t • w) = (CL.canonLin (F ∙ w)) x

The base point depends only on the line, not on the point of it that produced it.

When two lines through a point coincide

The diagonal weight count needs this: the canonical-line test's diagonal samples (j, v) that produce a given line are exactly those whose direction is proportional to it, which is why several of them contribute and the weight is a sum rather than a single term.

theorem MIPRE.LIDT.Adapter.through_eq {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {u z : Fin n → F} (hz : ∃ (k : Fin n), z k ≠ 0) : Line.through u z = (u - u (Fin.find (fun (k : Fin n) => z k ≠ 0) hz) • (z (Fin.find (fun (k : Fin n) => z k ≠ 0) hz))⁻¹ • z, (z (Fin.find (fun (k : Fin n) => z k ≠ 0) hz))⁻¹ • z)

The canonical presentation, unfolded.

theorem MIPRE.LIDT.Adapter.through_snd {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {u z : Fin n → F} (hz : ∃ (k : Fin n), z k ≠ 0) : (Line.through u z).2 = (z (Fin.find (fun (k : Fin n) => z k ≠ 0) hz))⁻¹ • z

The canonical direction, projected out.

theorem MIPRE.LIDT.Adapter.through_fst {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {u z : Fin n → F} (hz : ∃ (k : Fin n), z k ≠ 0) : (Line.through u z).1 = u - u (Fin.find (fun (k : Fin n) => z k ≠ 0) hz) • (z (Fin.find (fun (k : Fin n) => z k ≠ 0) hz))⁻¹ • z

The canonical base point, projected out.

theorem MIPRE.LIDT.Adapter.through_mem {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {u z : Fin n → F} (hz : ∃ (k : Fin n), z k ≠ 0) : u = (Line.through u z).1 + u (Fin.find (fun (k : Fin n) => z k ≠ 0) hz) • (Line.through u z).2

The point a canonical presentation was built from lies on the line it presents.

theorem MIPRE.LIDT.Adapter.through_eq_through_iff {F : Type u_1} [Field F] {n : ℕ} [DecidableEq F] {u w z : Fin n → F} (hw : ∃ (k : Fin n), w k ≠ 0) (hz : ∃ (k : Fin n), z k ≠ 0) : Line.through u z = Line.through u w ↔ ∃ (c : F), c ≠ 0 ∧ z = c • w

Two lines through the same point coincide exactly when their directions are proportional.