Axis-parallel lines for the low individual degree test

Axis-parallel line geometry on top of the core parameter infrastructure: AxisParallelLine records a base point and a coordinate direction, with canonical parameterization, rebasing, and slice-embedding operations.

References

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

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

A genuinely axis-parallel affine line in F_q^m.

• base : Point params
• direction : Fin params.m

@[instance_reducible]

instance MIPStarRE.LDT.instDecidableEqAxisParallelLine {params✝ : Parameters} : DecidableEq (AxisParallelLine params✝)

Equations

• MIPStarRE.LDT.instDecidableEqAxisParallelLine = MIPStarRE.LDT.instDecidableEqAxisParallelLine.decEq

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

Equations

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

@[instance_reducible]

instance MIPStarRE.LDT.instInhabitedAxisParallelLine {a✝ : Parameters} : Inhabited (AxisParallelLine a✝)

Equations

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

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

The canonical affine parameterization t ↦ base + t e_i.

Equations

• ℓ.pointAt t i = if i = ℓ.direction then MIPStarRE.LDT.addCoord (ℓ.base i) t else ℓ.base i

def MIPStarRE.LDT.AxisParallelLine.throughPoint {params : Parameters} [FieldModel params.q] (u : Point params) (i : Fin params.m) : AxisParallelLine params

Canonical geometric axis-parallel line through u in direction i.

The representative stores zero in the moving coordinate, so all points on the same geometric line map to the same AxisParallelLine.

Equations

• MIPStarRE.LDT.AxisParallelLine.throughPoint u i = { base := fun (j : Fin params.m) => if j = i then MIPStarRE.LDT.zeroCoord else u j, direction := i }

def MIPStarRE.LDT.AxisParallelLine.sampleParameter {params : Parameters} [FieldModel params.q] (u : Point params) (i : Fin params.m) : Fq params

Affine parameter of the sampled point on the canonical axis-parallel line through u in direction i.

Equations

• MIPStarRE.LDT.AxisParallelLine.sampleParameter u i = u i

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

Rebase an axis-parallel 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.AxisParallelLine.rebaseAt_pointAt_zero {params : Parameters} [FieldModel params.q] (ℓ : AxisParallelLine params) (t : Fq params) : (ℓ.rebaseAt t).pointAt zeroCoord = ℓ.pointAt t

@[simp]

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

@[simp]

theorem MIPStarRE.LDT.AxisParallelLine.rebaseAt_direction {params : Parameters} [FieldModel params.q] (ℓ : AxisParallelLine params) (t : Fq params) : (ℓ.rebaseAt t).direction = ℓ.direction

@[simp]

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

The canonical affine parameterization of throughPoint u i at parameter sampleParameter u i = u i returns the original point u.

@[simp]

theorem MIPStarRE.LDT.AxisParallelLine.rebaseAt_throughPoint_sampleParameter {params : Parameters} [FieldModel params.q] (u : Point params) (i : Fin params.m) : (throughPoint u i).rebaseAt (sampleParameter u i) = { base := u, direction := i }

Rebasing the canonical line throughPoint u i at its sample parameter yields the axis-parallel line with base u and direction i.

def MIPStarRE.LDT.AxisParallelLine.appendAtHeight (params : Parameters) (ℓ : AxisParallelLine params) (x : Fq params) : AxisParallelLine params.next

Embed an axis-parallel line into the slice at height x.

Equations

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

@[simp]

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