Polynomial-size projective normalization circuits

This file realizes first-nonzero projective normalization as an explicit shared De Morgan circuit. It first computes one nonzero flag per field coordinate, selects the first nonzero coordinate once, applies the shared binary-field inverse circuit once, and then multiplies every coordinate by that inverse in parallel.

def Algebraic.MassProduction.vectorCoordinateNonzeroExpression (dimension width : ℕ) (coordinate : Fin dimension) : DeMorgan.Expression (dimension * width)

Direct OR expression testing whether one packed field coordinate has a true bit.

Equations

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

def Algebraic.MassProduction.vectorCoordinateNonzeroFlags {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : Fin dimension → Bool

Semantic nonzero flags for every coordinate of a packed field vector.

Equations

• Algebraic.MassProduction.vectorCoordinateNonzeroFlags input coordinate = Algebraic.DeMorgan.Expression.finOrValue width fun (bit : Fin width) => input (finProdFinEquiv (coordinate, bit))

@[simp]

theorem Algebraic.MassProduction.vectorCoordinateNonzeroExpression_eval {dimension width : ℕ} (coordinate : Fin dimension) (input : Fin (dimension * width) → Bool) : DeMorgan.Expression.eval input (vectorCoordinateNonzeroExpression dimension width coordinate) = vectorCoordinateNonzeroFlags input coordinate

theorem Algebraic.MassProduction.vectorCoordinateNonzeroFlags_eq_true_iff {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : vectorCoordinateNonzeroFlags input coordinate = true ↔ binaryExtensionVectorCoordinate widthPositive input coordinate ≠ 0

@[simp]

theorem Algebraic.MassProduction.vectorCoordinateNonzeroExpression_standardCost {dimension width : ℕ} (coordinate : Fin dimension) : (vectorCoordinateNonzeroExpression dimension width coordinate).standardCost = width

@[reducible]

def Algebraic.MassProduction.vectorCoordinateNonzeroGateCount (dimension width : ℕ) (coordinate : Fin dimension) : ℕ

Gate count of one compiled coordinate nonzero test.

Equations

• Algebraic.MassProduction.vectorCoordinateNonzeroGateCount dimension width coordinate = (Algebraic.MassProduction.vectorCoordinateNonzeroExpression dimension width coordinate).gateCount

def Algebraic.MassProduction.vectorCoordinateNonzeroCircuit (dimension width : ℕ) : Circuit DeMorgan.signature (dimension * width) dimension

Compute and share all coordinate nonzero flags.

Equations

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

@[simp]

theorem Algebraic.MassProduction.vectorCoordinateNonzeroCircuit_size (dimension width : ℕ) : (vectorCoordinateNonzeroCircuit dimension width).size = ∑ coordinate : Fin dimension, vectorCoordinateNonzeroGateCount dimension width coordinate

@[simp]

theorem Algebraic.MassProduction.vectorCoordinateNonzeroCircuit_eval {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : (vectorCoordinateNonzeroCircuit dimension width).eval DeMorgan.interpretation input = vectorCoordinateNonzeroFlags input

@[simp]

theorem Algebraic.MassProduction.vectorCoordinateNonzeroCircuit_cost {dimension width : ℕ} : (vectorCoordinateNonzeroCircuit dimension width).cost DeMorgan.standardCost = dimension * width

All coordinate nonzero tests together cost exactly dimension * width.

def Algebraic.MassProduction.normalizationFlaggedBits {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : Fin (dimension * width + dimension) → Bool

Original packed vector followed by its shared coordinate nonzero flags.

Equations

• Algebraic.MassProduction.normalizationFlaggedBits input = Fin.append input (Algebraic.MassProduction.vectorCoordinateNonzeroFlags input)

def Algebraic.MassProduction.normalizationFlaggedCircuit (dimension width : ℕ) : Circuit DeMorgan.signature (dimension * width) (dimension * width + dimension)

Circuit retaining the original vector and appending all nonzero flags.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationFlaggedCircuit_size (dimension width : ℕ) : (normalizationFlaggedCircuit dimension width).size = ∑ coordinate : Fin dimension, vectorCoordinateNonzeroGateCount dimension width coordinate

The exact gate count of normalizationFlaggedCircuit.

@[simp]

theorem Algebraic.MassProduction.normalizationFlaggedCircuit_eval {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : (normalizationFlaggedCircuit dimension width).eval DeMorgan.interpretation input = normalizationFlaggedBits input

@[simp]

theorem Algebraic.MassProduction.normalizationFlaggedCircuit_cost {dimension width : ℕ} : (normalizationFlaggedCircuit dimension width).cost DeMorgan.standardCost = dimension * width

def Algebraic.MassProduction.normalizationVectorBitIndex {dimension width : ℕ} (index : Fin (dimension * width)) : Fin (dimension * width + dimension)

Index of an original vector bit in the flagged intermediate layout.

Equations

• Algebraic.MassProduction.normalizationVectorBitIndex index = Fin.castAdd dimension index

def Algebraic.MassProduction.normalizationFlagIndex {dimension width : ℕ} (coordinate : Fin dimension) : Fin (dimension * width + dimension)

Index of one nonzero flag in the flagged intermediate layout.

Equations

• Algebraic.MassProduction.normalizationFlagIndex coordinate = Fin.natAdd (dimension * width) coordinate

@[simp]

theorem Algebraic.MassProduction.normalizationFlaggedBits_vectorBit {dimension width : ℕ} (input : Fin (dimension * width) → Bool) (index : Fin (dimension * width)) : normalizationFlaggedBits input (normalizationVectorBitIndex index) = input index

@[simp]

theorem Algebraic.MassProduction.normalizationFlaggedBits_flag {dimension width : ℕ} (input : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : normalizationFlaggedBits input (normalizationFlagIndex coordinate) = vectorCoordinateNonzeroFlags input coordinate

def Algebraic.MassProduction.firstNonzeroFlag {dimension : ℕ} (flags : Fin dimension → Bool) (pivot : Fin dimension) : Bool

Whether a coordinate is the first asserted nonzero flag.

Equations

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

def Algebraic.MassProduction.firstNonzeroFlagExpression (dimension width : ℕ) (pivot : Fin dimension) : DeMorgan.Expression (dimension * width + dimension)

Expression computing one first-nonzero one-hot flag from the shared coordinate flags.

Equations

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

@[simp]

theorem Algebraic.MassProduction.firstNonzeroFlagExpression_eval_flagged {dimension width : ℕ} (input : Fin (dimension * width) → Bool) (pivot : Fin dimension) : DeMorgan.Expression.eval (normalizationFlaggedBits input) (firstNonzeroFlagExpression dimension width pivot) = firstNonzeroFlag (vectorCoordinateNonzeroFlags input) pivot

theorem Algebraic.MassProduction.firstNonzeroFlag_vectorBits_eq_true_iff {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) : firstNonzeroFlag (vectorCoordinateNonzeroFlags (binaryExtensionVectorBits widthPositive vector)) pivot = true ↔ firstNonzeroCoordinate vector = some pivot

def Algebraic.MassProduction.normalizationPivotBits {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : Fin width → Bool

The selected pivot bits computed from the flagged layout.

Equations

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

def Algebraic.MassProduction.normalizationPivotBitExpression (dimension width : ℕ) (bit : Fin width) : DeMorgan.Expression (dimension * width + dimension)

Expression for one bit of the selected first nonzero coordinate.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationPivotBitExpression_eval_flagged {dimension width : ℕ} (input : Fin (dimension * width) → Bool) (bit : Fin width) : DeMorgan.Expression.eval (normalizationFlaggedBits input) (normalizationPivotBitExpression dimension width bit) = normalizationPivotBits input bit

@[reducible]

def Algebraic.MassProduction.normalizationPivotBitGateCount (dimension width : ℕ) (bit : Fin width) : ℕ

Gate count of one compiled pivot-output expression.

Equations

• Algebraic.MassProduction.normalizationPivotBitGateCount dimension width bit = (Algebraic.MassProduction.normalizationPivotBitExpression dimension width bit).gateCount

def Algebraic.MassProduction.normalizationPivotFromFlaggedCircuit (dimension width : ℕ) : Circuit DeMorgan.signature (dimension * width + dimension) width

Select the first nonzero field coordinate from a flagged vector.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationPivotFromFlaggedCircuit_size (dimension width : ℕ) : (normalizationPivotFromFlaggedCircuit dimension width).size = ∑ bit : Fin width, normalizationPivotBitGateCount dimension width bit

def Algebraic.MassProduction.normalizationPivotCircuit (dimension width : ℕ) : Circuit DeMorgan.signature (dimension * width) width

Select the first nonzero coordinate directly from a packed vector.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationPivotCircuit_size (dimension width : ℕ) : (normalizationPivotCircuit dimension width).size = (normalizationFlaggedCircuit dimension width).size + ∑ bit : Fin width, normalizationPivotBitGateCount dimension width bit

The exact gate count of normalizationPivotCircuit.

@[simp]

theorem Algebraic.MassProduction.normalizationPivotCircuit_eval {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : (normalizationPivotCircuit dimension width).eval DeMorgan.interpretation input = normalizationPivotBits input

theorem Algebraic.MassProduction.normalizationPivotBits_vectorBits {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) (pivotEquality : firstNonzeroCoordinate vector = some pivot) : normalizationPivotBits (binaryExtensionVectorBits widthPositive vector) = decodeBinaryExtension widthPositive (vector pivot)

On a nonzero field vector, pivot selection returns the encoding of its least nonzero coordinate.

def Algebraic.MassProduction.normalizationVectorAndPivotBits {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : Fin (dimension * width + width) → Bool

Preserve the packed vector while appending its selected pivot.

Equations

• Algebraic.MassProduction.normalizationVectorAndPivotBits input = Fin.append input (Algebraic.MassProduction.normalizationPivotBits input)

def Algebraic.MassProduction.normalizationVectorAndPivotCircuit (dimension width : ℕ) : Circuit DeMorgan.signature (dimension * width) (dimension * width + width)

Shared vector-and-pivot circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationVectorAndPivotCircuit_size (dimension width : ℕ) : (normalizationVectorAndPivotCircuit dimension width).size = (normalizationPivotCircuit dimension width).size

normalizationVectorAndPivotCircuit has exactly the gates of normalizationPivotCircuit; the surrounding wiring adds none.

@[simp]

theorem Algebraic.MassProduction.normalizationVectorAndPivotCircuit_eval {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : (normalizationVectorAndPivotCircuit dimension width).eval DeMorgan.interpretation input = normalizationVectorAndPivotBits input

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

Preserve the vector block and replace the pivot block by the output of the shared inverse circuit.

Equations

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

noncomputable def Algebraic.MassProduction.normalizationInversePreparationCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : Circuit DeMorgan.signature (dimension * width + width) (dimension * width + width)

Apply one shared pivot inversion while retaining the original vector.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationInversePreparationCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (normalizationInversePreparationCircuit dimension widthPositive).size = (binaryExtensionInverseCircuit widthPositive).size

normalizationInversePreparationCircuit has exactly the gates of binaryExtensionInverseCircuit; the surrounding wiring adds none.

@[simp]

theorem Algebraic.MassProduction.normalizationInversePreparationCircuit_eval {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width + width) → Bool) : (normalizationInversePreparationCircuit dimension widthPositive).eval DeMorgan.interpretation input = normalizationInversePreparationBits widthPositive input

noncomputable def Algebraic.MassProduction.normalizationVectorAndInverseCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : Circuit DeMorgan.signature (dimension * width) (dimension * width + width)

Vector together with the inverse of its selected pivot.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationVectorAndInverseCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (normalizationVectorAndInverseCircuit dimension widthPositive).size = (normalizationVectorAndPivotCircuit dimension width).size + (normalizationInversePreparationCircuit dimension widthPositive).size

The exact gate count of normalizationVectorAndInverseCircuit.

@[simp]

theorem Algebraic.MassProduction.normalizationVectorAndInverseCircuit_eval {width dimension : ℕ} (widthPositive : 0 < width) (input : Fin (dimension * width) → Bool) : (normalizationVectorAndInverseCircuit dimension widthPositive).eval DeMorgan.interpretation input = normalizationInversePreparationBits widthPositive (normalizationVectorAndPivotBits input)

def Algebraic.MassProduction.normalizationCoordinateMultiplicationInput (dimension width : ℕ) (coordinate : Fin dimension) : Fin (2 * width) → Fin (dimension * width + width)

Wiring from one vector coordinate and the shared inverse block into a binary-field multiplication circuit.

Equations

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

noncomputable def Algebraic.MassProduction.normalizationCoordinateMultiplicationCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (coordinate : Fin dimension) : Circuit DeMorgan.signature (dimension * width + width) width

One coordinate times the shared inverse pivot.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationCoordinateMultiplicationCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (coordinate : Fin dimension) : (normalizationCoordinateMultiplicationCircuit dimension widthPositive coordinate).size = ∑ output : Fin width, multiplicationCoordinateGateCount widthPositive output

The exact gate count of normalizationCoordinateMultiplicationCircuit.

theorem Algebraic.MassProduction.normalizationCoordinateMultiplicationCircuit_eval {width dimension : ℕ} (widthPositive : 0 < width) (coordinate : Fin dimension) (vector : Fin (dimension * width) → Bool) (inverse : Fin width → Bool) : (normalizationCoordinateMultiplicationCircuit dimension widthPositive coordinate).eval DeMorgan.interpretation (Fin.append vector inverse) = binaryExtensionMulBits widthPositive (binaryExtensionPairBits (fun (bit : Fin width) => vector (finProdFinEquiv (coordinate, bit))) inverse)

@[reducible]

noncomputable def Algebraic.MassProduction.normalizationCoordinateMultiplicationGateCount {width : ℕ} (widthPositive : 0 < width) : ℕ

Gate count of one coordinate multiplication.

Equations

• Algebraic.MassProduction.normalizationCoordinateMultiplicationGateCount widthPositive = ∑ output : Fin width, Algebraic.MassProduction.multiplicationCoordinateGateCount widthPositive output

noncomputable def Algebraic.MassProduction.normalizationMultiplicationCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : Circuit DeMorgan.signature (dimension * width + width) (dimension * width)

Multiply every vector coordinate by the same shared inverse pivot.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizationMultiplicationCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (normalizationMultiplicationCircuit dimension widthPositive).size = ∑ x : Fin dimension, normalizationCoordinateMultiplicationGateCount widthPositive

@[simp]

theorem Algebraic.MassProduction.normalizationMultiplicationCircuit_eval {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin (dimension * width) → Bool) (inverse : Fin width → Bool) (coordinate : Fin dimension) (bit : Fin width) : (normalizationMultiplicationCircuit dimension widthPositive).eval DeMorgan.interpretation (Fin.append vector inverse) (finProdFinEquiv (coordinate, bit)) = binaryExtensionMulBits widthPositive (binaryExtensionPairBits (fun (localBit : Fin width) => vector (finProdFinEquiv (coordinate, localBit))) inverse) bit

noncomputable def Algebraic.MassProduction.normalizeBinaryExtensionVectorCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : Circuit DeMorgan.signature (dimension * width) (dimension * width)

Complete shared circuit for canonical projective normalization.

Equations

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

@[simp]

theorem Algebraic.MassProduction.normalizeBinaryExtensionVectorCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (normalizeBinaryExtensionVectorCircuit dimension widthPositive).size = (normalizationVectorAndInverseCircuit dimension widthPositive).size + dimension * normalizationCoordinateMultiplicationGateCount widthPositive

The exact gate count of normalizeBinaryExtensionVectorCircuit.

theorem Algebraic.MassProduction.normalizationVectorAndInverseCircuit_eval_vectorBits {width dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) (pivotEquality : firstNonzeroCoordinate vector = some pivot) : (normalizationVectorAndInverseCircuit dimension widthPositive).eval DeMorgan.interpretation (binaryExtensionVectorBits widthPositive vector) = Fin.append (binaryExtensionVectorBits widthPositive vector) (decodeBinaryExtension widthPositive (vector pivot)⁻¹)

On an encoded nonzero vector, the shared inverse stage preserves the vector and appends the encoding of the inverse pivot.

theorem Algebraic.MassProduction.normalizeBinaryExtensionVectorCircuit_eval_vectorBits {width dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (vector : Fin dimension → BinaryExtension width) (vectorNonzero : vector ≠ 0) : (normalizeBinaryExtensionVectorCircuit dimension widthPositive).eval DeMorgan.interpretation (binaryExtensionVectorBits widthPositive vector) = binaryExtensionVectorBits widthPositive (normalizeBinaryExtensionVector vector)

The explicit normalization circuit computes the packed canonical normalization of every nonzero field vector.

theorem Algebraic.MassProduction.normalizeBinaryExtensionVectorCircuit_eval_projective {width dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : (normalizeBinaryExtensionVectorCircuit dimension widthPositive).eval DeMorgan.interpretation (binaryExtensionVectorBits widthPositive direction.rep) = projectiveDirectionKey widthPositive direction

Consequently the normalization circuit computes the canonical key of any supplied projective representative.

theorem Algebraic.MassProduction.firstNonzeroFlagExpression_standardCost_le {dimension width : ℕ} (pivot : Fin dimension) : (firstNonzeroFlagExpression dimension width pivot).standardCost ≤ 2 * dimension + 1

A first-nonzero flag expression has quadratic-free, linear cost in the number of field coordinates.

theorem Algebraic.MassProduction.normalizationPivotBitExpression_standardCost_le {width dimension : ℕ} (bit : Fin width) : (normalizationPivotBitExpression dimension width bit).standardCost ≤ dimension * (2 * dimension + 3)

One selected-pivot output bit has quadratic cost in the vector dimension.

theorem Algebraic.MassProduction.normalizationPivotFromFlaggedCircuit_cost_le {dimension width : ℕ} : (normalizationPivotFromFlaggedCircuit dimension width).cost DeMorgan.standardCost ≤ width * (dimension * (2 * dimension + 3))

Cost bound for selecting one shared pivot after the coordinate flags have been computed.

theorem Algebraic.MassProduction.normalizationPivotCircuit_cost_le {dimension width : ℕ} : (normalizationPivotCircuit dimension width).cost DeMorgan.standardCost ≤ dimension * width + width * (dimension * (2 * dimension + 3))

Full pivot selection includes the linear coordinate-zero tests.

@[simp]

theorem Algebraic.MassProduction.normalizationCoordinateMultiplicationCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) (coordinate : Fin dimension) : (normalizationCoordinateMultiplicationCircuit dimension widthPositive coordinate).cost DeMorgan.standardCost = width * (6 * (width * width))

@[simp]

theorem Algebraic.MassProduction.normalizationMultiplicationCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) : (normalizationMultiplicationCircuit dimension widthPositive).cost DeMorgan.standardCost = dimension * (width * (6 * (width * width)))

The final coordinatewise scaling performs one field multiplication per coordinate.

@[simp]

theorem Algebraic.MassProduction.normalizationInversePreparationCircuit_cost {width dimension : ℕ} (widthPositive : 0 < width) : (normalizationInversePreparationCircuit dimension widthPositive).cost DeMorgan.standardCost = (binaryExtensionInverseCircuit widthPositive).cost DeMorgan.standardCost

def Algebraic.MassProduction.projectiveNormalizationCircuitBound (dimension width : ℕ) : ℕ

A concrete polynomial ledger for the complete projective normalizer.

Equations

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

theorem Algebraic.MassProduction.normalizeBinaryExtensionVectorCircuit_cost_le {width dimension : ℕ} (widthPositive : 0 < width) : (normalizeBinaryExtensionVectorCircuit dimension widthPositive).cost DeMorgan.standardCost ≤ projectiveNormalizationCircuitBound dimension width

The complete canonical-normalization circuit satisfies the displayed polynomial bound.