Bridge, part 1: parameters and the field coding

The MIPStarRE development works with a coded field Fq params := Fin params.q together with a FieldModel params.q instance carrying an actual field K and an equivalence K ≃ Fin q; all arithmetic is transported through the coding (encodeScalar, decodeScalar, addCoord, ...). This file instantiates that setup for our finite field F: the parameters lidtParams F m d (with q = Fintype.card F) and the field model with K := F, and it records how the coding interacts with points, lines and the arithmetic of F.

@[reducible, inline]

abbrev MIPRE.LIDT.Bridge.lidtParams (F : Type u_1) [Field F] [Fintype F] (m d : ℕ) [NeZero m] : MIPStarRE.LDT.Parameters

The MIPStarRE parameters of the (m, q, d) test, q = |F|.

Equations

• MIPRE.LIDT.Bridge.lidtParams F m d = { m := m, q := Fintype.card F, d := d, hm := ⋯, hq := ⋯, hqPrimePower := ⋯ }

@[instance_reducible]

noncomputable instance MIPRE.LIDT.Bridge.fieldModel (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] : MIPStarRE.LDT.FieldModel (Fintype.card F)

The field model with carrier F itself, coded by an arbitrary enumeration.

Equations

• MIPRE.LIDT.Bridge.fieldModel F = { K := F, instField := inferInstance, instFintype := inferInstance, instDecidableEq := inferInstance, equiv := Fintype.equivFin F }

Coding of scalars and points

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Bridge.enc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x : F) : MIPStarRE.LDT.Fq (lidtParams F m d)

Encode a scalar of F into the coded field of the parameters.

Equations

• MIPRE.LIDT.Bridge.enc x = MIPStarRE.LDT.encodeScalar x

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Bridge.dec {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x : MIPStarRE.LDT.Fq (lidtParams F m d)) : F

Decode a coded scalar into F.

Equations

• MIPRE.LIDT.Bridge.dec x = MIPStarRE.LDT.decodeScalar x

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Bridge.encP {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u : Point F m) : MIPStarRE.LDT.Point (lidtParams F m d)

Encode a point of F^m.

Equations

• MIPRE.LIDT.Bridge.encP u i = MIPRE.LIDT.Bridge.enc (u i)

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Bridge.decP {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u : MIPStarRE.LDT.Point (lidtParams F m d)) : Point F m

Decode a coded point.

Equations

• MIPRE.LIDT.Bridge.decP u i = MIPRE.LIDT.Bridge.dec (u i)

@[simp]

theorem MIPRE.LIDT.Bridge.dec_enc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x : F) : dec (enc x) = x

@[simp]

theorem MIPRE.LIDT.Bridge.enc_dec {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x : MIPStarRE.LDT.Fq (lidtParams F m d)) : enc (dec x) = x

theorem MIPRE.LIDT.Bridge.enc_injective {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : Function.Injective enc

theorem MIPRE.LIDT.Bridge.dec_injective {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : Function.Injective dec

@[simp]

theorem MIPRE.LIDT.Bridge.decP_encP {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u : Point F m) : decP (encP u) = u

@[simp]

theorem MIPRE.LIDT.Bridge.encP_decP {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u : MIPStarRE.LDT.Point (lidtParams F m d)) : encP (decP u) = u

noncomputable def MIPRE.LIDT.Bridge.pointEquiv {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : Point F m ≃ MIPStarRE.LDT.Point (lidtParams F m d)

The coding of points, as an equivalence.

Equations

• MIPRE.LIDT.Bridge.pointEquiv = { toFun := MIPRE.LIDT.Bridge.encP, invFun := MIPRE.LIDT.Bridge.decP, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MIPRE.LIDT.Bridge.pointEquiv_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u : Point F m) : pointEquiv u = encP u

@[simp]

theorem MIPRE.LIDT.Bridge.pointEquiv_symm_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u : MIPStarRE.LDT.Point (lidtParams F m d)) : pointEquiv.symm u = decP u

noncomputable def MIPRE.LIDT.Bridge.scalarEquiv {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : F ≃ MIPStarRE.LDT.Fq (lidtParams F m d)

The coding of scalars, as an equivalence.

Equations

• MIPRE.LIDT.Bridge.scalarEquiv = { toFun := MIPRE.LIDT.Bridge.enc, invFun := MIPRE.LIDT.Bridge.dec, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MIPRE.LIDT.Bridge.scalarEquiv_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x : F) : scalarEquiv x = enc x

@[simp]

theorem MIPRE.LIDT.Bridge.scalarEquiv_symm_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x : MIPStarRE.LDT.Fq (lidtParams F m d)) : scalarEquiv.symm x = dec x

@[simp]

theorem MIPRE.LIDT.Bridge.decodePoint_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u : MIPStarRE.LDT.Point (lidtParams F m d)) : MIPStarRE.LDT.decodePoint u = decP u

Arithmetic through the coding

@[simp]

theorem MIPRE.LIDT.Bridge.dec_zeroCoord {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : dec MIPStarRE.LDT.zeroCoord = 0

@[simp]

theorem MIPRE.LIDT.Bridge.dec_addCoord {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x y : MIPStarRE.LDT.Fq (lidtParams F m d)) : dec (MIPStarRE.LDT.addCoord x y) = dec x + dec y

@[simp]

theorem MIPRE.LIDT.Bridge.dec_mulCoord {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (x y : MIPStarRE.LDT.Fq (lidtParams F m d)) : dec (MIPStarRE.LDT.mulCoord x y) = dec x * dec y

@[simp]

theorem MIPRE.LIDT.Bridge.decP_addPoint {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (u v : MIPStarRE.LDT.Point (lidtParams F m d)) : decP (MIPStarRE.LDT.addPoint u v) = decP u + decP v

@[simp]

theorem MIPRE.LIDT.Bridge.decP_smulPoint {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (t : MIPStarRE.LDT.Fq (lidtParams F m d)) (u : MIPStarRE.LDT.Point (lidtParams F m d)) : decP (MIPStarRE.LDT.smulPoint t u) = dec t • decP u

@[simp]

theorem MIPRE.LIDT.Bridge.decP_zeroPoint {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : decP MIPStarRE.LDT.zeroPoint = 0

theorem MIPRE.LIDT.Bridge.decP_axis_pointAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.AxisParallelLine (lidtParams F m d)) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : decP (ℓ.pointAt t) = decP ℓ.base + dec t • Pi.single ℓ.direction 1

The decoded point at parameter t of an axis-parallel line.

theorem MIPRE.LIDT.Bridge.decP_diag_pointAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d)) (t : MIPStarRE.LDT.Fq (lidtParams F m d)) : decP (ℓ.pointAt t) = decP ℓ.base + dec t • decP ℓ.direction

The decoded point at parameter t of a diagonal line.