Explicit finite binary encodings

Routing keys need a logarithmic-width representation of finite group indices and the existing basis-bit representation of affine-space points. These are plain encoding functions with ordinary injectivity hypotheses; no serializer or finite-enumeration instances are introduced.

def Algebraic.MassProduction.finiteIndexBits {count : ℕ} (width : ℕ) (value : Fin count) : Fin width → Bool

Little-endian width-bit representation of a bounded natural index.

Equations

• Algebraic.MassProduction.finiteIndexBits width value bit = (↑value).testBit ↑bit

theorem Algebraic.MassProduction.finiteIndexBits_injective {count width : ℕ} (fits : count ≤ 2 ^ width) : Function.Injective (finiteIndexBits width)

The fixed-width representation is injective whenever its numeric range contains every source index.

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

Row-major fixed-basis bits determine a binary-extension-field vector.

noncomputable def Algebraic.MassProduction.resourceSlotKeyBits {width groups dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (slot : Fin groups × (Fin dimension → BinaryExtension width)) : Fin (groupBitWidth + dimension * width) → Bool

Explicit matching key for a (group, affine point) resource slot.

Equations

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

theorem Algebraic.MassProduction.resourceSlotKeyBits_injective {width groups groupBitWidth dimension : ℕ} (widthPositive : 0 < width) (groupFits : groups ≤ 2 ^ groupBitWidth) : Function.Injective (resourceSlotKeyBits widthPositive groupBitWidth)

Group bits followed by field-coordinate bits form an injective slot key.

def Algebraic.MassProduction.activeRoutingKey {keyWidth : ℕ} (key : Fin keyWidth → Bool) : Fin (keyWidth + 1) → Bool

Reserve a leading marker bit for active routing keys.

Equations

• Algebraic.MassProduction.activeRoutingKey key = Fin.cons false key

def Algebraic.MassProduction.paddingRoutingKey {keyWidth : ℕ} (tail : Fin keyWidth → Bool) : Fin (keyWidth + 1) → Bool

Padding keys live in the disjoint leading-marker half of key space.

Equations

• Algebraic.MassProduction.paddingRoutingKey tail = Fin.cons true tail

theorem Algebraic.MassProduction.activeRoutingKey_injective {keyWidth : ℕ} : Function.Injective activeRoutingKey

theorem Algebraic.MassProduction.paddingRoutingKey_ne_activeRoutingKey {keyWidth : ℕ} (padding active : Fin keyWidth → Bool) : paddingRoutingKey padding ≠ activeRoutingKey active

Canonical lexicographic enumeration of all fixed-width keys

noncomputable def Algebraic.MassProduction.lexBitVectorOrderIso (width : ℕ) : Fin (2 ^ width) ≃o Lex (Fin width → Bool)

The increasing enumeration of all Boolean bit vectors in lexicographic order. This is noncomputable metadata used to assign fixed resource-slot wires; it is not evaluated by the circuit.

Equations

• Algebraic.MassProduction.lexBitVectorOrderIso width = monoEquivOfFin (Lex (Fin width → Bool)) ⋯

noncomputable def Algebraic.MassProduction.lexBitVectorAt {width : ℕ} (position : Fin (2 ^ width)) : Fin width → Bool

Bit vector at one canonical lexicographic position.

Equations

• Algebraic.MassProduction.lexBitVectorAt position = ofLex ((Algebraic.MassProduction.lexBitVectorOrderIso width) position)

noncomputable def Algebraic.MassProduction.lexBitVectorIndex {width : ℕ} (bits : Fin width → Bool) : Fin (2 ^ width)

Canonical lexicographic position of a bit vector.

Equations

• Algebraic.MassProduction.lexBitVectorIndex bits = (Algebraic.MassProduction.lexBitVectorOrderIso width).symm (toLex bits)

@[simp]

theorem Algebraic.MassProduction.lexBitVectorAt_index {width : ℕ} (bits : Fin width → Bool) : lexBitVectorAt (lexBitVectorIndex bits) = bits

@[simp]

theorem Algebraic.MassProduction.lexBitVectorIndex_at {width : ℕ} (position : Fin (2 ^ width)) : lexBitVectorIndex (lexBitVectorAt position) = position

theorem Algebraic.MassProduction.lexBitVectorAt_injective {width : ℕ} : Function.Injective lexBitVectorAt

theorem Algebraic.MassProduction.lexBitVectorAt_strictMono {width : ℕ} : StrictMono fun (position : Fin (2 ^ width)) => toLex (lexBitVectorAt position)