Counting common-zero-block monomials

For the asymptotic construction it is enough to take field widths that are multiples of the block width. Exponents are then base-2^h digit strings. After transposing the digit matrix, the retained monomials are exactly the strings of digit columns containing an all-zero column. Their cardinality is A^m - (A-1)^m, where A = 2^(dimension*h).

theorem Algebraic.MassProduction.HighRate.cardWordsContaining {Alphabet : Type u_1} [Fintype Alphabet] (letter : Alphabet) (length : ℕ) : Nat.card { word : Fin length → Alphabet // ∃ (index : Fin length), word index = letter } = Fintype.card Alphabet ^ length - (Fintype.card Alphabet - 1) ^ length

Number of words containing a specified letter at least once.

@[reducible, inline]

abbrev Algebraic.MassProduction.HighRate.DigitMatrix (Coordinate : Type u_1) (blockWidth blocks : ℕ) : Type u_1

A matrix with one base-2^h digit per coordinate and per digit block.

Equations

• Algebraic.MassProduction.HighRate.DigitMatrix Coordinate blockWidth blocks = (Fin blocks → Coordinate → Fin (2 ^ blockWidth))

@[reducible, inline]

abbrev Algebraic.MassProduction.HighRate.RetainedDigits (Coordinate : Type u_1) (blockWidth blocks : ℕ) : Type u_1

Retain exactly the digit matrices having a common all-zero block.

Equations

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

def Algebraic.MassProduction.HighRate.digitExponentEquiv (Coordinate : Type u_1) (blockWidth blocks : ℕ) : DigitMatrix Coordinate blockWidth blocks ≃ (Coordinate → Fin ((2 ^ blockWidth) ^ blocks))

Reading each coordinate's digits as a natural exponent is a bijection with all reduced exponent vectors.

Equations

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

def Algebraic.MassProduction.HighRate.digitDegrees {Coordinate : Type u_1} {blockWidth blocks : ℕ} (digits : DigitMatrix Coordinate blockWidth blocks) : Coordinate → ℕ

The natural exponent vector represented by a digit matrix.

Equations

• Algebraic.MassProduction.HighRate.digitDegrees digits coordinate = ↑((Algebraic.MassProduction.HighRate.digitExponentEquiv Coordinate blockWidth blocks) digits coordinate)

theorem Algebraic.MassProduction.HighRate.digitDegrees_lt {Coordinate : Type u_1} {blockWidth blocks : ℕ} (digits : DigitMatrix Coordinate blockWidth blocks) (coordinate : Coordinate) : digitDegrees digits coordinate < 2 ^ (blockWidth * blocks)

Every digit matrix encodes reduced exponents for a field of width blockWidth * blocks.

theorem Algebraic.MassProduction.HighRate.digitDegreesDigit {Coordinate : Type u_1} {blockWidth blocks : ℕ} (digits : DigitMatrix Coordinate blockWidth blocks) (block : Fin blocks) (coordinate : Coordinate) : digitDegrees digits coordinate / 2 ^ (blockWidth * ↑block) % 2 ^ blockWidth = ↑(digits block coordinate)

Extracting one encoded digit returns the original digit.

theorem Algebraic.MassProduction.HighRate.retainedDigitsCommonZeroBlock {Coordinate : Type u_1} {blockWidth blocks : ℕ} (digits : RetainedDigits Coordinate blockWidth blocks) : ∃ (block : Fin blocks), CommonZeroBlock (digitDegrees ↑digits) (blockWidth * ↑block) blockWidth

Every retained matrix supplies a common zero block in its exponent vector. The block starts at blockWidth * block.

theorem Algebraic.MassProduction.HighRate.cardRetainedDigits (Coordinate : Type u_1) [Fintype Coordinate] (blockWidth blocks : ℕ) : Nat.card (RetainedDigits Coordinate blockWidth blocks) = (2 ^ (blockWidth * Fintype.card Coordinate)) ^ blocks - (2 ^ (blockWidth * Fintype.card Coordinate) - 1) ^ blocks

Exact dimension of the chosen monomial family before evaluation.