Canonical projective coordinates over binary extension fields

The scheduler ranks forbidden directions by first normalizing a nonzero vector: its first nonzero coordinate is scaled to one. This file establishes the field-level representation and its projective invariance. The following circuit module realizes the same normalization using the explicit polynomial- size field circuits.

noncomputable def Algebraic.MassProduction.binaryExtensionVectorCoordinate {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : BinaryExtension width

Decode one coordinate from a row-major packed field vector.

Equations

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

noncomputable def Algebraic.MassProduction.binaryExtensionVectorBits {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) : Fin (dimension * width) → Bool

Encode a field vector in row-major (coordinate, bit) order.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionVectorCoordinate_vectorBits {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (coordinate : Fin dimension) : binaryExtensionVectorCoordinate widthPositive (binaryExtensionVectorBits widthPositive vector) coordinate = vector coordinate

@[simp]

theorem Algebraic.MassProduction.binaryExtensionVectorBits_vectorCoordinate {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) : binaryExtensionVectorBits widthPositive (binaryExtensionVectorCoordinate widthPositive input) = input

@[simp]

theorem Algebraic.MassProduction.binaryExtensionVectorBits_eq_zero_iff {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) : (binaryExtensionVectorBits widthPositive vector = fun (x : Fin (dimension * width)) => false) ↔ vector = 0

theorem Algebraic.MassProduction.binaryExtensionVectorBits_ne_zero_iff {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) : (binaryExtensionVectorBits widthPositive vector ≠ fun (x : Fin (dimension * width)) => false) ↔ vector ≠ 0

noncomputable def Algebraic.MassProduction.firstNonzeroCoordinate {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) : Option (Fin dimension)

Least nonzero coordinate of a field vector, if one exists.

Equations

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

noncomputable def Algebraic.MassProduction.normalizeBinaryExtensionVector {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) : Fin dimension → BinaryExtension width

Normalize a nonzero vector by its first nonzero coordinate. The zero vector is sent to zero.

Equations

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

theorem Algebraic.MassProduction.firstNonzeroCoordinate_eq_some_iff {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) : firstNonzeroCoordinate vector = some pivot ↔ vector pivot ≠ 0 ∧ ∀ previous < pivot, vector previous = 0

theorem Algebraic.MassProduction.firstNonzeroCoordinate_smul {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (scalar : BinaryExtension width) (scalarNonzero : scalar ≠ 0) (vectorNonzero : ∃ (coordinate : Fin dimension), vector coordinate ≠ 0) : (firstNonzeroCoordinate fun (coordinate : Fin dimension) => scalar * vector coordinate) = firstNonzeroCoordinate vector

theorem Algebraic.MassProduction.normalizeBinaryExtensionVector_smul {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (scalar : BinaryExtension width) (scalarNonzero : scalar ≠ 0) (vectorNonzero : ∃ (coordinate : Fin dimension), vector coordinate ≠ 0) : (normalizeBinaryExtensionVector fun (coordinate : Fin dimension) => scalar * vector coordinate) = normalizeBinaryExtensionVector vector

theorem Algebraic.MassProduction.normalizeBinaryExtensionVector_eq_of_firstNonzeroCoordinate {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) (pivotEquality : firstNonzeroCoordinate vector = some pivot) : normalizeBinaryExtensionVector vector = fun (coordinate : Fin dimension) => (vector pivot)⁻¹ * vector coordinate

theorem Algebraic.MassProduction.normalizeBinaryExtensionVector_ne_zero {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (vectorNonzero : vector ≠ 0) : normalizeBinaryExtensionVector vector ≠ 0

theorem Algebraic.MassProduction.mk_normalizeBinaryExtensionVector {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (vectorNonzero : vector ≠ 0) : Projectivization.mk (BinaryExtension width) (normalizeBinaryExtensionVector vector) ⋯ = Projectivization.mk (BinaryExtension width) vector vectorNonzero

theorem Algebraic.MassProduction.normalizeBinaryExtensionVector_rep_mk {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (vectorNonzero : vector ≠ 0) : normalizeBinaryExtensionVector (Projectivization.mk (BinaryExtension width) vector vectorNonzero).rep = normalizeBinaryExtensionVector vector

noncomputable def Algebraic.MassProduction.projectiveDirectionKey {width dimension : ℕ} (widthPositive : 0 < width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : Fin (dimension * width) → Bool

Packed canonical key of a projective direction.

Equations

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

theorem Algebraic.MassProduction.projectiveDirectionKey_mk {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (vectorNonzero : vector ≠ 0) : projectiveDirectionKey widthPositive (Projectivization.mk (BinaryExtension width) vector vectorNonzero) = binaryExtensionVectorBits widthPositive (normalizeBinaryExtensionVector vector)

theorem Algebraic.MassProduction.projectiveDirectionKey_injective {width dimension : ℕ} (widthPositive : 0 < width) : Function.Injective (projectiveDirectionKey widthPositive)

Canonical packed projective keys are injective.