The seeded-CL adapter, part 3: choosing a seed

The adapter must turn a line of the canonical-line test into a seeded description of that line, which means choosing one of the q/m seeds in the relevant χ-fibre (MIPRE.LIDT.CL.card_chi_fiber). seedOf is the explicit choice, indexed by the fibre position: seedOf hm i r is the r-th seed with χ = i, and chi_seedOf says so.

card_chi_fiber proves the fibre has q/m elements by exhibiting an equivalence with Fin (q/m); seedOf is that equivalence's inverse, extracted so that the adapter can name a seed rather than merely know one exists. seedOf_injective is the other half, and it is what makes the averaging count: the q/m seeds seedOf hm i r are distinct, so averaging a choice over r is averaging over the whole fibre, which is where the reduction pays back the factor q/m that a fixed choice would cost (see MIPRE.TensorProductStrategy.exists_one_sub_value_adapt_le and the discussion in planning/lidt-cl-adapter.md).

noncomputable def MIPRE.LIDT.Adapter.seedOf {F : Type u_1} [Fintype F] {m : ℕ} (hm : m ∣ Fintype.card F) (i : Fin m) (r : Fin (Fintype.card F / m)) : F

The r-th seed of the χ-fibre over i, under the fixed bijection F ≃ Fin q.

Equations

• MIPRE.LIDT.Adapter.seedOf hm i r = (Fintype.equivFin F).symm ⟨↑i * (Fintype.card F / m) + ↑r, ⋯⟩

@[simp]

theorem MIPRE.LIDT.Adapter.equivFin_seedOf {F : Type u_1} [Fintype F] {m : ℕ} (hm : m ∣ Fintype.card F) (i : Fin m) (r : Fin (Fintype.card F / m)) : ↑((Fintype.equivFin F) (seedOf hm i r)) = ↑i * (Fintype.card F / m) + ↑r

@[simp]

theorem MIPRE.LIDT.Adapter.chi_seedOf {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (i : Fin m) (r : Fin (Fintype.card F / m)) : CL.chi hm (seedOf hm i r) = i

seedOf hm i r lies in the fibre over i.

theorem MIPRE.LIDT.Adapter.seedOf_injective {F : Type u_1} [Fintype F] {m : ℕ} (hm : m ∣ Fintype.card F) (i : Fin m) : Function.Injective (seedOf hm i)

The q/m seeds of a fibre are distinct, so averaging a choice over r averages over the whole fibre.