Packed ranks for projective directions

For a normalized nonzero vector with pivot h, the manuscript's block rank is represented by dimension blocks of width bits:

• every block before h is the unsigned binary digit one;
• block h is the unsigned binary digit zero;
• every later block is the corresponding normalized field-coordinate bits.

With most-significant bits first this is exactly B_h + val_q(tail), but it avoids an addition circuit. This module builds the rank circuit after the existing projective normalizer, proves its exact semantics, and supplies a polynomial cost ledger.

def Algebraic.MassProduction.unsignedOneBits (width : ℕ) : Fin width → Bool

Big-endian width-bit representation of the unsigned integer one.

Equations

• Algebraic.MassProduction.unsignedOneBits width bit = decide (↑bit + 1 = width)

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

Direct first-nonzero flag over packed field-coordinate bits.

Equations

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

@[simp]

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

theorem Algebraic.MassProduction.firstNonzeroDirectExpression_vectorBits_eq_true_iff {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) : DeMorgan.Expression.eval (binaryExtensionVectorBits widthPositive vector) (firstNonzeroDirectExpression dimension width pivot) = true ↔ firstNonzeroCoordinate vector = some pivot

def Algebraic.MassProduction.rankValueExpression (dimension width : ℕ) (coordinate : Fin dimension) (bit : Fin width) (pivot : Fin dimension) : DeMorgan.Expression (dimension * width)

One rank bit selected after the pivot is known.

Equations

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

def Algebraic.MassProduction.projectiveRankBitExpression (dimension width : ℕ) (output : Fin (dimension * width)) : DeMorgan.Expression (dimension * width)

One output bit of the packed projective rank.

Equations

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

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

Pure packed-bit semantics of the rank transformation.

Equations

• Algebraic.MassProduction.projectiveRankPackedBits input output = Algebraic.DeMorgan.Expression.eval input (Algebraic.MassProduction.projectiveRankBitExpression dimension width output)

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

Field-level block-rank representation when the pivot is known.

Equations

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

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

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

Canonical block-rank key of a projective direction.

Equations

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

def Algebraic.MassProduction.projectiveRankBlock {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : Fin width → Bool

One width-bit block of a packed rank.

Equations

• Algebraic.MassProduction.projectiveRankBlock rank coordinate bit = rank (finProdFinEquiv (coordinate, bit))

noncomputable def Algebraic.MassProduction.firstNonOneRankBlock {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) : Option (Fin dimension)

First rank block different from the unsigned digit one. Valid ranks have one-blocks before the pivot and a zero-block at the pivot.

Equations

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

theorem Algebraic.MassProduction.firstNonOneRankBlock_eq_some_iff {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) (pivot : Fin dimension) : firstNonOneRankBlock rank = some pivot ↔ projectiveRankBlock rank pivot ≠ unsignedOneBits width ∧ ∀ previous < pivot, projectiveRankBlock rank previous = unsignedOneBits width

@[simp]

theorem Algebraic.MassProduction.projectiveRankBlock_normalized_before {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot coordinate : Fin dimension) (before : coordinate < pivot) : projectiveRankBlock (normalizedVectorRankBits widthPositive vector pivot) coordinate = unsignedOneBits width

@[simp]

theorem Algebraic.MassProduction.projectiveRankBlock_normalized_pivot {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) : projectiveRankBlock (normalizedVectorRankBits widthPositive vector pivot) pivot = fun (x : Fin width) => false

theorem Algebraic.MassProduction.falseBits_ne_unsignedOneBits {width : ℕ} (widthPositive : 0 < width) : (fun (x : Fin width) => false) ≠ unsignedOneBits width

theorem Algebraic.MassProduction.firstNonOneRankBlock_normalizedVectorRankBits {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) : firstNonOneRankBlock (normalizedVectorRankBits widthPositive vector pivot) = some pivot

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

Semantic inverse of the packed rank on valid ranks. The first non-one block identifies the pivot; earlier field coordinates are zero, the pivot is field one, and later coordinates are copied from the rank tail.

Equations

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

theorem Algebraic.MassProduction.projectiveUnrankPackedBits_rank_of_pivot {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) (pivotEquality : firstNonzeroCoordinate vector = some pivot) (pivotOne : vector pivot = 1) : projectiveUnrankPackedBits widthPositive (projectiveRankPackedBits (binaryExtensionVectorBits widthPositive vector)) = binaryExtensionVectorBits widthPositive vector

Unranking inverts ranking for any vector already normalized at its first nonzero coordinate.

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

Projective normalization keeps the first nonzero coordinate.

theorem Algebraic.MassProduction.normalizeBinaryExtensionVector_pivot {dimension width : ℕ} (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) (pivotEquality : firstNonzeroCoordinate vector = some pivot) : normalizeBinaryExtensionVector vector pivot = 1

The pivot coordinate of a normalized vector is field one.

theorem Algebraic.MassProduction.projectiveUnrankPackedBits_directionRank {width dimension : ℕ} (widthPositive : 0 < width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : projectiveUnrankPackedBits widthPositive (projectiveDirectionRankBits widthPositive direction) = projectiveDirectionKey widthPositive direction

Semantic unranking recovers the canonical normalized key of every projective direction.

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

The packed block rank is injective on projective directions.

The exact initial interval of valid projective ranks

def Algebraic.MassProduction.projectiveRankSentinel (dimension width : ℕ) : Fin (dimension * width) → Bool

First invalid packed projective rank: one field digit in every block.

Equations

• Algebraic.MassProduction.projectiveRankSentinel dimension width output = Algebraic.MassProduction.unsignedOneBits width (finProdFinEquiv.symm output).2

@[simp]

theorem Algebraic.MassProduction.projectiveRankSentinel_block {dimension width : ℕ} (coordinate : Fin dimension) : projectiveRankBlock (projectiveRankSentinel dimension width) coordinate = unsignedOneBits width

theorem Algebraic.MassProduction.normalizedVectorRankBits_lt_sentinel {width dimension : ℕ} (widthPositive : 0 < width) (vector : Fin dimension → BinaryExtension width) (pivot : Fin dimension) : toLex (normalizedVectorRankBits widthPositive vector pivot) < toLex (projectiveRankSentinel dimension width)

A normalized block rank is strictly below the all-one-digit sentinel.

theorem Algebraic.MassProduction.rank_lt_sentinel_has_zero_pivot {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (rankLt : toLex rank < toLex (projectiveRankSentinel dimension width)) : ∃ (pivot : Fin dimension), (projectiveRankBlock rank pivot = fun (x : Fin width) => false) ∧ ∀ previous < pivot, projectiveRankBlock rank previous = unsignedOneBits width

Any rank below the sentinel has a first non-one block, and that block is the all-zero pivot block. All preceding blocks are unsigned one.

theorem Algebraic.MassProduction.firstNonOneRankBlock_of_lt_sentinel {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (rankLt : toLex rank < toLex (projectiveRankSentinel dimension width)) : ∃ (pivot : Fin dimension), firstNonOneRankBlock rank = some pivot ∧ projectiveRankBlock rank pivot = fun (x : Fin width) => false

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

Field vector decoded from the semantic projective unranker.

Equations

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

@[simp]

theorem Algebraic.MassProduction.projectiveUnrankVector_before {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (pivot previous : Fin dimension) (pivotEquality : firstNonOneRankBlock rank = some pivot) (previousBefore : previous < pivot) : projectiveUnrankVector widthPositive rank previous = 0

@[simp]

theorem Algebraic.MassProduction.projectiveUnrankVector_pivot {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (pivot : Fin dimension) (pivotEquality : firstNonOneRankBlock rank = some pivot) : projectiveUnrankVector widthPositive rank pivot = 1

theorem Algebraic.MassProduction.firstNonzeroCoordinate_projectiveUnrankVector {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (pivot : Fin dimension) (pivotEquality : firstNonOneRankBlock rank = some pivot) : firstNonzeroCoordinate (projectiveUnrankVector widthPositive rank) = some pivot

theorem Algebraic.MassProduction.normalize_projectiveUnrankVector {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (pivot : Fin dimension) (pivotEquality : firstNonOneRankBlock rank = some pivot) : normalizeBinaryExtensionVector (projectiveUnrankVector widthPositive rank) = projectiveUnrankVector widthPositive rank

theorem Algebraic.MassProduction.projectiveUnrankPackedBits_eq_vectorBits {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) : projectiveUnrankPackedBits widthPositive rank = binaryExtensionVectorBits widthPositive (projectiveUnrankVector widthPositive rank)

theorem Algebraic.MassProduction.normalizedVectorRankBits_projectiveUnrankVector {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (pivot : Fin dimension) (pivotEquality : firstNonOneRankBlock rank = some pivot) (pivotZero : projectiveRankBlock rank pivot = fun (x : Fin width) => false) : normalizedVectorRankBits widthPositive (projectiveUnrankVector widthPositive rank) pivot = rank

theorem Algebraic.MassProduction.projectiveRankPackedBits_unrank_of_lt_sentinel {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (rankLt : toLex rank < toLex (projectiveRankSentinel dimension width)) : projectiveRankPackedBits (projectiveUnrankPackedBits widthPositive rank) = rank

Ranking after semantic unranking is the identity on the valid initial interval.

theorem Algebraic.MassProduction.projectiveDirectionRankBits_lt_sentinel {width dimension : ℕ} (widthPositive : 0 < width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : toLex (projectiveDirectionRankBits widthPositive direction) < toLex (projectiveRankSentinel dimension width)

theorem Algebraic.MassProduction.exists_projectiveDirectionRankBits_eq_of_lt_sentinel {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (rankLt : toLex rank < toLex (projectiveRankSentinel dimension width)) : ∃ (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), projectiveDirectionRankBits widthPositive direction = rank

noncomputable def Algebraic.MassProduction.projectiveDirectionOfRank {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (rankLt : toLex rank < toLex (projectiveRankSentinel dimension width)) : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)

The projective direction represented by a packed rank below the sentinel.

Equations

• Algebraic.MassProduction.projectiveDirectionOfRank widthPositive rank rankLt = Classical.choose ⋯

@[simp]

theorem Algebraic.MassProduction.projectiveDirectionRankBits_directionOfRank {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (rankLt : toLex rank < toLex (projectiveRankSentinel dimension width)) : projectiveDirectionRankBits widthPositive (projectiveDirectionOfRank widthPositive rank rankLt) = rank

noncomputable def Algebraic.MassProduction.projectiveDirectionRankEquivIio {width dimension : ℕ} (widthPositive : 0 < width) : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width) ≃ { rank : Lex (Fin (dimension * width) → Bool) // rank < toLex (projectiveRankSentinel dimension width) }

Packed projective ranks are exactly the strict initial lexicographic interval below the all-one-digit sentinel.

Equations

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

theorem Algebraic.MassProduction.card_projectiveRankInterval {width dimension : ℕ} (widthPositive : 0 < width) : Nat.card { rank : Lex (Fin (dimension * width) → Bool) // rank < toLex (projectiveRankSentinel dimension width) } = Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))

def Algebraic.MassProduction.rankBitEqualsConstantExpression {n : ℕ} (expected : Bool) (input : Fin n) : DeMorgan.Expression n

Test a selected input bit against one hardwired rank bit.

Equations

• Algebraic.MassProduction.rankBitEqualsConstantExpression expected input = if expected = true then Algebraic.DeMorgan.Expression.input input else (Algebraic.DeMorgan.Expression.input input).not

@[simp]

theorem Algebraic.MassProduction.rankBitEqualsConstantExpression_eval_eq_true_iff {n : ℕ} (expected : Bool) (index : Fin n) (input : Fin n → Bool) : DeMorgan.Expression.eval input (rankBitEqualsConstantExpression expected index) = true ↔ input index = expected

theorem Algebraic.MassProduction.rankBitEqualsConstantExpression_standardCost_le {n : ℕ} (expected : Bool) (index : Fin n) : (rankBitEqualsConstantExpression expected index).standardCost ≤ 1

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

Equality of one rank block with the big-endian unsigned digit one.

Equations

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

def Algebraic.MassProduction.rankBlockOneFlag {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : Bool

Boolean flag computed by rankBlockOneExpression.

Equations

• Algebraic.MassProduction.rankBlockOneFlag rank coordinate = Algebraic.DeMorgan.Expression.eval rank (Algebraic.MassProduction.rankBlockOneExpression dimension width coordinate)

theorem Algebraic.MassProduction.rankBlockOneFlag_eq_true_iff {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : rankBlockOneFlag rank coordinate = true ↔ projectiveRankBlock rank coordinate = unsignedOneBits width

theorem Algebraic.MassProduction.rankBlockOneFlag_eq_false_iff {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) (coordinate : Fin dimension) : rankBlockOneFlag rank coordinate = false ↔ projectiveRankBlock rank coordinate ≠ unsignedOneBits width

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

One-hot flag for the first rank block that is not unsigned one.

Equations

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

@[simp]

theorem Algebraic.MassProduction.firstNonOneRankExpression_eval {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) (pivot : Fin dimension) : DeMorgan.Expression.eval rank (firstNonOneRankExpression dimension width pivot) = (!rankBlockOneFlag rank pivot && DeMorgan.Expression.finAndValue dimension fun (previous : Fin dimension) => if previous < pivot then rankBlockOneFlag rank previous else true)

theorem Algebraic.MassProduction.firstNonOneRankExpression_eval_eq_true_iff {dimension width : ℕ} (rank : Fin (dimension * width) → Bool) (pivot : Fin dimension) : DeMorgan.Expression.eval rank (firstNonOneRankExpression dimension width pivot) = true ↔ firstNonOneRankBlock rank = some pivot

noncomputable def Algebraic.MassProduction.unrankValueExpression {width dimension : ℕ} (widthPositive : 0 < width) (coordinate : Fin dimension) (bit : Fin width) (pivot : Fin dimension) : DeMorgan.Expression (dimension * width)

One output value selected by a candidate unrank pivot.

Equations

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

noncomputable def Algebraic.MassProduction.projectiveUnrankBitExpression {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (output : Fin (dimension * width)) : DeMorgan.Expression (dimension * width)

One output bit of the projective unrank circuit.

Equations

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

theorem Algebraic.MassProduction.projectiveUnrankBitExpression_eval {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) (output : Fin (dimension * width)) : DeMorgan.Expression.eval rank (projectiveUnrankBitExpression dimension widthPositive output) = projectiveUnrankPackedBits widthPositive rank output

@[reducible]

noncomputable def Algebraic.MassProduction.projectiveUnrankBitGateCount {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (output : Fin (dimension * width)) : ℕ

Gate count of one independently compiled unrank output.

Equations

• Algebraic.MassProduction.projectiveUnrankBitGateCount dimension widthPositive output = (Algebraic.MassProduction.projectiveUnrankBitExpression dimension widthPositive output).gateCount

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

Explicit circuit reconstructing the canonical normalized vector from a valid packed projective rank.

Equations

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

@[simp]

theorem Algebraic.MassProduction.projectiveUnrankPackedCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (projectiveUnrankPackedCircuit dimension widthPositive).size = ∑ output : Fin (dimension * width), projectiveUnrankBitGateCount dimension widthPositive output

@[simp]

theorem Algebraic.MassProduction.projectiveUnrankPackedCircuit_eval {width dimension : ℕ} (widthPositive : 0 < width) (rank : Fin (dimension * width) → Bool) : (projectiveUnrankPackedCircuit dimension widthPositive).eval DeMorgan.interpretation rank = projectiveUnrankPackedBits widthPositive rank

theorem Algebraic.MassProduction.projectiveUnrankPackedCircuit_eval_directionRank {width dimension : ℕ} (widthPositive : 0 < width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : (projectiveUnrankPackedCircuit dimension widthPositive).eval DeMorgan.interpretation (projectiveDirectionRankBits widthPositive direction) = projectiveDirectionKey widthPositive direction

Circuit-level rank/unrank correctness on every projective direction.

theorem Algebraic.MassProduction.rankBlockOneExpression_standardCost_le {dimension width : ℕ} (coordinate : Fin dimension) : (rankBlockOneExpression dimension width coordinate).standardCost ≤ 2 * width

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

theorem Algebraic.MassProduction.projectiveUnrankBitExpression_standardCost_le {width dimension : ℕ} (widthPositive : 0 < width) (output : Fin (dimension * width)) : (projectiveUnrankBitExpression dimension widthPositive output).standardCost ≤ dimension * (2 * width + 2 + dimension * (2 * width + 1) + 2)

theorem Algebraic.MassProduction.projectiveUnrankPackedCircuit_cost_le {width dimension : ℕ} (widthPositive : 0 < width) : (projectiveUnrankPackedCircuit dimension widthPositive).cost DeMorgan.standardCost ≤ dimension * width * (dimension * (2 * width + 2 + dimension * (2 * width + 1) + 2))

Polynomial gate ledger for projective unranking.

@[reducible]

def Algebraic.MassProduction.projectiveRankBitGateCount (dimension width : ℕ) (output : Fin (dimension * width)) : ℕ

Gate count of the independently compiled rank outputs.

Equations

• Algebraic.MassProduction.projectiveRankBitGateCount dimension width output = (Algebraic.MassProduction.projectiveRankBitExpression dimension width output).gateCount

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

Explicit circuit converting a normalized nonzero vector to its block rank.

Equations

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

@[simp]

theorem Algebraic.MassProduction.projectiveRankPackedCircuit_size (dimension width : ℕ) : (projectiveRankPackedCircuit dimension width).size = ∑ output : Fin (dimension * width), projectiveRankBitGateCount dimension width output

@[simp]

theorem Algebraic.MassProduction.projectiveRankPackedCircuit_eval {dimension width : ℕ} (input : Fin (dimension * width) → Bool) : (projectiveRankPackedCircuit dimension width).eval DeMorgan.interpretation input = projectiveRankPackedBits input

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

Normalize a projective representative and then emit its block rank.

Equations

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

@[simp]

theorem Algebraic.MassProduction.projectiveDirectionRankCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) : (projectiveDirectionRankCircuit dimension widthPositive).size = (normalizeBinaryExtensionVectorCircuit dimension widthPositive).size + ∑ output : Fin (dimension * width), projectiveRankBitGateCount dimension width output

The exact gate count of projectiveDirectionRankCircuit.

@[simp]

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

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

theorem Algebraic.MassProduction.projectiveRankBitExpression_standardCost_le {dimension width : ℕ} (output : Fin (dimension * width)) : (projectiveRankBitExpression dimension width output).standardCost ≤ dimension * (width + 1 + dimension * (width + 2) + 2)

theorem Algebraic.MassProduction.projectiveRankPackedCircuit_cost_le {dimension width : ℕ} : (projectiveRankPackedCircuit dimension width).cost DeMorgan.standardCost ≤ dimension * width * (dimension * (width + 1 + dimension * (width + 2) + 2))

Polynomial gate ledger for the packed rank transformation.

theorem Algebraic.MassProduction.projectiveDirectionRankCircuit_cost_le {width dimension : ℕ} (widthPositive : 0 < width) : (projectiveDirectionRankCircuit dimension widthPositive).cost DeMorgan.standardCost ≤ projectiveNormalizationCircuitBound dimension width + dimension * width * (dimension * (width + 1 + dimension * (width + 2) + 2))

The complete normalizer-plus-ranker remains polynomial in the extension width for fixed projective dimension.