Executable line-versus-point arithmetic

The program finds the first nonzero direction coordinate, checks membership in the affine line, and evaluates the supplied polynomial at that parameter. The zero direction denotes a singleton line and has parameter zero.

theorem MIPRE.Introspection.FieldLineCheck.firstPair_zero {F : Type u_1} [Zero F] [DecidableEq F] (l : List (F × F)) (h : ∀ p ∈ l, p.2 = 0) : LineProgram.firstPair l = (0, 0)

def MIPRE.Introspection.FieldLineCheck.parameter {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (origin direction point : Fin m → F) : F

The canonical scalar parameter, including singleton lines.

Equations

• MIPRE.Introspection.FieldLineCheck.parameter origin direction point = MIPRE.Introspection.LineProgram.coefficient (List.ofFn fun (i : Fin m) => (point i - origin i, direction i))

theorem MIPRE.Introspection.FieldLineCheck.parameter_eq {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (origin direction point : Fin m → F) : parameter origin direction point = if h : ∃ (j : Fin m), direction j ≠ 0 then (point (Fin.find (fun (j : Fin m) => direction j ≠ 0) h) - origin (Fin.find (fun (j : Fin m) => direction j ≠ 0) h)) / direction (Fin.find (fun (j : Fin m) => direction j ≠ 0) h) else 0

theorem MIPRE.Introspection.FieldLineCheck.membership_iff {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (origin direction point : Fin m → F) : point = origin + parameter origin direction point • direction ↔ ∃ (t : F), point = origin + t • direction

noncomputable def MIPRE.Introspection.FieldLineCheck.subtractProg : Cost.PolyTimeFun (List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

Equations

• MIPRE.Introspection.FieldLineCheck.subtractProg = MIPRE.LowDegree.BinaryPolynomial.xorBitsProg.map.comp MIPRE.Cost.PolyTimeFun.zip

theorem MIPRE.Introspection.FieldLineCheck.subtractProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (x y : Fin m → (SAT.shoupBinField k hk).carrier) : subtractProg.toFun ((SAT.shoupBinField k hk).vecBits x, (SAT.shoupBinField k hk).vecBits y) = (SAT.shoupBinField k hk).vecBits (x - y)

noncomputable def MIPRE.Introspection.FieldLineCheck.parameterProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × List Cost.BitStr × List Cost.BitStr) Cost.BitStr

Width, origin, direction, and point.

Equations

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

theorem MIPRE.Introspection.FieldLineCheck.parameterProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (origin direction point : Fin m → (SAT.shoupBinField k hk).carrier) : parameterProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).vecBits origin, (SAT.shoupBinField k hk).vecBits direction, (SAT.shoupBinField k hk).vecBits point) = (SAT.shoupBinField k hk).toBits (parameter origin direction point)

noncomputable def MIPRE.Introspection.FieldLineCheck.affineEntryProg : Cost.PolyTimeFun ((Cost.BitStr × Cost.BitStr) × Cost.Unary × Cost.BitStr) Cost.BitStr

Equations

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

noncomputable def MIPRE.Introspection.FieldLineCheck.affineProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr × List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

Equations

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

theorem MIPRE.Introspection.FieldLineCheck.affineProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (t : (SAT.shoupBinField k hk).carrier) (origin direction : Fin m → (SAT.shoupBinField k hk).carrier) : affineProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits t, (SAT.shoupBinField k hk).vecBits origin, (SAT.shoupBinField k hk).vecBits direction) = (SAT.shoupBinField k hk).vecBits (origin + t • direction)

theorem MIPRE.Introspection.FieldLineCheck.vecBits_injective {k m : ℕ} (E : SAT.BinField k) : Function.Injective E.vecBits

noncomputable def MIPRE.Introspection.FieldLineCheck.memberProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × List Cost.BitStr × List Cost.BitStr) Bool

Equations

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

theorem MIPRE.Introspection.FieldLineCheck.memberProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (origin direction point : Fin m → (SAT.shoupBinField k hk).carrier) : memberProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).vecBits origin, (SAT.shoupBinField k hk).vecBits direction, (SAT.shoupBinField k hk).vecBits point) = true ↔ ∃ (t : (SAT.shoupBinField k hk).carrier), point = origin + t • direction

noncomputable def MIPRE.Introspection.FieldLineCheck.lineCheckProg : Cost.PolyTimeFun ((Cost.Unary × List Cost.BitStr × List Cost.BitStr × List Cost.BitStr) × List Cost.BitStr × Cost.BitStr) Bool

The geometric line input, polynomial coefficients, and claimed point value.

Equations

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

theorem MIPRE.Introspection.FieldLineCheck.lineCheckProg_correct (k : ℕ) (hk : 1 ≤ k) {m n : ℕ} (origin direction point : Fin m → (SAT.shoupBinField k hk).carrier) (f : Fin n → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) : lineCheckProg.toFun ((Cost.unary k, (SAT.shoupBinField k hk).vecBits origin, (SAT.shoupBinField k hk).vecBits direction, (SAT.shoupBinField k hk).vecBits point), (SAT.shoupBinField k hk).vecBits f, (SAT.shoupBinField k hk).toBits a) = true ↔ (∃ (t : (SAT.shoupBinField k hk).carrier), point = origin + t • direction) ∧ ∑ i : Fin n, f i * parameter origin direction point ^ ↑i = a