Exact indexing and keys for the high-rate resource bank

The bank contains exactly one Boolean function per code copy, field point, and basis bit. Only routing keys use ceiling-logarithm index widths; neither copy nor bit-index padding enlarges the bank's leading cost.

def Algebraic.MassProduction.HighRate.ResourceLayout.count (copies dimension width : ℕ) : ℕ

Exact number of Boolean resource functions.

Equations

• Algebraic.MassProduction.HighRate.ResourceLayout.count copies dimension width = copies * (2 ^ (dimension * width) * width)

def Algebraic.MassProduction.HighRate.ResourceLayout.index {copies dimension width : ℕ} (copy : Fin copies) (point : Fin (2 ^ (dimension * width))) (bit : Fin width) : Fin (count copies dimension width)

Exact row-major index of a code-copy, encoded-point, basis-bit triple.

Equations

• Algebraic.MassProduction.HighRate.ResourceLayout.index copy point bit = finProdFinEquiv (copy, finProdFinEquiv (point, bit))

def Algebraic.MassProduction.HighRate.ResourceLayout.atIndex {copies dimension width : ℕ} (resource : Fin (count copies dimension width)) : Fin copies × Fin (2 ^ (dimension * width)) × Fin width

Decode the exact bank index into its three finite coordinates.

Equations

• Algebraic.MassProduction.HighRate.ResourceLayout.atIndex resource = ((finProdFinEquiv.symm resource).1, finProdFinEquiv.symm (finProdFinEquiv.symm resource).2)

theorem Algebraic.MassProduction.HighRate.ResourceLayout.atIndex_index {copies dimension width : ℕ} (copy : Fin copies) (point : Fin (2 ^ (dimension * width))) (bit : Fin width) : atIndex (index copy point bit) = (copy, point, bit)

Index construction and coordinate decoding cancel exactly.

theorem Algebraic.MassProduction.HighRate.ResourceLayout.index_atIndex {copies dimension width : ℕ} (resource : Fin (count copies dimension width)) : index (atIndex resource).1 (atIndex resource).2.1 (atIndex resource).2.2 = resource

Every index is recovered from its decoded coordinates.

def Algebraic.MassProduction.HighRate.ResourceLayout.keyWidth (copyBits dimension width selectorBits : ℕ) : ℕ

Routing key width, with exact point bits and logarithmic finite indices.

Equations

• Algebraic.MassProduction.HighRate.ResourceLayout.keyWidth copyBits dimension width selectorBits = copyBits + (dimension * width + selectorBits)

noncomputable def Algebraic.MassProduction.HighRate.ResourceLayout.key {copies dimension width : ℕ} (copyBits selectorBits : ℕ) (resource : Fin (count copies dimension width)) : Fin (keyWidth copyBits dimension width selectorBits) → Bool

Fixed resource keys contain copy, point, and basis-bit coordinates.

Equations

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

theorem Algebraic.MassProduction.HighRate.ResourceLayout.key_injective {copies copyBits width selectorBits dimension : ℕ} (copyFits : copies ≤ 2 ^ copyBits) (selectorFits : width ≤ 2 ^ selectorBits) : Function.Injective (key copyBits selectorBits)

Adequate finite-index widths make the fixed resource keys distinct.

noncomputable def Algebraic.MassProduction.HighRate.ResourceLayout.position {width copies dimension : ℕ} (positive : 0 < width) (copy : Fin copies) (point : Fin dimension → BinaryExtension width) (bit : Fin width) : Fin (count copies dimension width)

Bank position of a geometric point and its selected field-basis bit.

Equations

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

theorem Algebraic.MassProduction.HighRate.ResourceLayout.key_position {width copies dimension : ℕ} (positive : 0 < width) (copyBits selectorBits : ℕ) (copy : Fin copies) (point : Fin dimension → BinaryExtension width) (bit : Fin width) : key copyBits selectorBits (position positive copy point bit) = Fin.append (finiteIndexBits copyBits copy) (Fin.append (binaryExtensionVectorBits positive point) (finiteIndexBits selectorBits bit))

The key at a geometric position is its expected concatenated encoding.

noncomputable def Algebraic.MassProduction.HighRate.ResourceLayout.pointAt {width copies dimension : ℕ} (positive : 0 < width) (resource : Fin (count copies dimension width)) : Fin dimension → BinaryExtension width

Decode a bank index's affine point using the fixed binary basis.

Equations

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

theorem Algebraic.MassProduction.HighRate.ResourceLayout.pointAt_position {width copies dimension : ℕ} (positive : 0 < width) (copy : Fin copies) (point : Fin dimension → BinaryExtension width) (bit : Fin width) : pointAt positive (position positive copy point bit) = point

Geometric indexing followed by point decoding recovers the same point.

noncomputable def Algebraic.MassProduction.HighRate.ResourceLayout.function {width dimension copies : ℕ} {Source : Type u_1} {Suffix : Type u_2} (positive : 0 < width) (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ InformationBit code copies) (original : Source → Suffix → Bool) (resource : Fin (count copies dimension width)) (suffix : Suffix) : Bool

The Boolean function at each exact bank position.

Equations

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

theorem Algebraic.MassProduction.HighRate.ResourceLayout.function_position {width dimension copies : ℕ} {Source : Type u_1} {Suffix : Type u_2} (positive : 0 < width) (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ InformationBit code copies) (original : Source → Suffix → Bool) (copy : Fin copies) (point : Fin dimension → BinaryExtension width) (bit : Fin width) (suffix : Suffix) : function positive code placement original (position positive copy point bit) suffix = booleanResource positive code placement original copy point bit suffix

A selected bank function is exactly the high-rate recovery resource.