Diagonal lines for the low individual degree test

Diagonal-line geometry and rebasing operations.

References

• references/ldt-paper/test_definition.tex
• blueprint/src/chapter/ch02_test.tex

structure MIPStarRE.LDT.DiagonalLine (params : Parameters) : Type

A genuinely affine diagonal line in F_q^m.

• base : Point params
• direction : Point params

@[instance_reducible]

instance MIPStarRE.LDT.instDecidableEqDiagonalLine {params✝ : Parameters} : DecidableEq (DiagonalLine params✝)

Equations

• MIPStarRE.LDT.instDecidableEqDiagonalLine = MIPStarRE.LDT.instDecidableEqDiagonalLine.decEq

def MIPStarRE.LDT.instDecidableEqDiagonalLine.decEq {params✝ : Parameters} (x✝ x✝¹ : DiagonalLine params✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MIPStarRE.LDT.instInhabitedDiagonalLine {a✝ : Parameters} : Inhabited (DiagonalLine a✝)

Equations

• MIPStarRE.LDT.instInhabitedDiagonalLine = { default := MIPStarRE.LDT.instInhabitedDiagonalLine.default }

def MIPStarRE.LDT.DiagonalLine.pointAt {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) : Fq params → Point params

The canonical affine parameterization t ↦ base + t · direction.

Equations

• ℓ.pointAt t = MIPStarRE.LDT.addPoint ℓ.base (MIPStarRE.LDT.smulPoint t ℓ.direction)

noncomputable def MIPStarRE.LDT.DiagonalLine.nonzeroDirectionSupport {params : Parameters} [FieldModel params.q] (v : Point params) : Finset (Fin params.m)

The support of the nonzero coordinates of a direction vector.

Equations

• MIPStarRE.LDT.DiagonalLine.nonzeroDirectionSupport v = {i : Fin params.m | v i ≠ MIPStarRE.LDT.zeroCoord}

noncomputable def MIPStarRE.LDT.DiagonalLine.firstNonzeroCoord? {params : Parameters} [FieldModel params.q] (v : Point params) : Option (Fin params.m)

The least nonzero coordinate of a direction vector, when one exists.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.DiagonalLine.normalizeDirection {params : Parameters} [FieldModel params.q] (v : Point params) : Point params

Normalize a direction vector so its first nonzero coordinate becomes 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.DiagonalLine.throughPointDirection {params : Parameters} [FieldModel params.q] (u v : Point params) : DiagonalLine params

Canonical geometric diagonal line through u in direction v.

For nonzero v, we normalize by the first nonzero coordinate and shift the base point so that this pivot coordinate is 0. The degenerate v = 0 case is kept as the singleton line through u.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.DiagonalLine.sampleParameter {params : Parameters} [FieldModel params.q] (u v : Point params) : Fq params

Affine parameter of the sampled point on the canonical diagonal line through u in direction v.

Equations

• MIPStarRE.LDT.DiagonalLine.sampleParameter u v = match MIPStarRE.LDT.DiagonalLine.firstNonzeroCoord? v with | none => MIPStarRE.LDT.zeroCoord | some i => u i

@[simp]

theorem MIPStarRE.LDT.DiagonalLine.throughPoint_pointAt_sampleParameter {params : Parameters} [FieldModel params.q] (u : Point params) (i : Fin params.m) : (AxisParallelLine.throughPoint u i).pointAt (AxisParallelLine.sampleParameter u i) = u

@[simp]

theorem MIPStarRE.LDT.DiagonalLine.throughPointDirection_pointAt_sampleParameter {params : Parameters} [FieldModel params.q] (u v : Point params) : (throughPointDirection u v).pointAt (sampleParameter u v) = u

def MIPStarRE.LDT.DiagonalLine.rebaseAt {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) (t : Fq params) : DiagonalLine params

Rebase a diagonal line so that the old point ℓ.pointAt t becomes the new base point.

Equations

• ℓ.rebaseAt t = { base := ℓ.pointAt t, direction := ℓ.direction }

@[simp]

theorem MIPStarRE.LDT.DiagonalLine.rebaseAt_pointAt_zero {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) (t : Fq params) : (ℓ.rebaseAt t).pointAt zeroCoord = ℓ.pointAt t

theorem MIPStarRE.LDT.DiagonalLine.rebaseAt_pointAt {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) (t s : Fq params) : (ℓ.rebaseAt t).pointAt s = ℓ.pointAt (addCoord t s)

@[simp]

theorem MIPStarRE.LDT.DiagonalLine.rebaseAt_zero {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) : ℓ.rebaseAt zeroCoord = ℓ

theorem MIPStarRE.LDT.DiagonalLine.rebaseAt_rebase {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) (t s : Fq params) : (ℓ.rebaseAt t).rebaseAt s = ℓ.rebaseAt (addCoord t s)

def MIPStarRE.LDT.DiagonalLine.appendAtHeight (params : Parameters) [FieldModel params.q] (ℓ : DiagonalLine params) (x : Fq params) : DiagonalLine params.next

Embed a diagonal line into the slice at height x, keeping the new coordinate fixed.

Equations

• MIPStarRE.LDT.DiagonalLine.appendAtHeight params ℓ x = { base := MIPStarRE.LDT.appendPoint params ℓ.base x, direction := MIPStarRE.LDT.appendPoint params ℓ.direction MIPStarRE.LDT.zeroCoord }

@[simp]

theorem MIPStarRE.LDT.DiagonalLine.appendAtHeight_rebaseAt {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) (t x : Fq params) : appendAtHeight params (ℓ.rebaseAt t) x = (appendAtHeight params ℓ x).rebaseAt t