Canonical Boolean-prefix packing

This module formalizes the manuscript's exact placement

s(a) = I(a) / width, j(a) = I(a) % width,

followed by the dimension base-gridWidth digits of s(a). The explicit finFunctionFinEquiv is the base-conversion bijection, so injectivity is a composition of finite embeddings rather than a cardinality-choice argument.

@[reducible]

noncomputable def Algebraic.MassProduction.CanonicalPacking.gridWidth (dimension width : ℕ) : ℕ

Number of interpolation nodes available in each tensor coordinate.

Equations

• Algebraic.MassProduction.CanonicalPacking.gridWidth dimension width = Algebraic.MassProduction.resourceGridWidth (Nat.card (Algebraic.MassProduction.BinaryExtension width)) dimension

theorem Algebraic.MassProduction.CanonicalPacking.gridWidth_eq {width dimension : ℕ} (widthPositive : 0 < width) : gridWidth dimension width = resourceGridWidth (2 ^ width) dimension

noncomputable def Algebraic.MassProduction.CanonicalPacking.flatPosition {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : Fin (gridWidth dimension width ^ dimension * width)

The canonical flat information-bit position for one prefix index.

Equations

• Algebraic.MassProduction.CanonicalPacking.flatPosition packingFits source = Fin.castLE packingFits source

noncomputable def Algebraic.MassProduction.CanonicalPacking.symbolAndBit {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : Fin (gridWidth dimension width ^ dimension) × Fin width

Split a flat packed position into its tensor-symbol rank and basis bit.

Equations

• Algebraic.MassProduction.CanonicalPacking.symbolAndBit packingFits source = finProdFinEquiv.symm (Algebraic.MassProduction.CanonicalPacking.flatPosition packingFits source)

noncomputable def Algebraic.MassProduction.CanonicalPacking.symbolIndex {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : Fin (gridWidth dimension width ^ dimension)

Canonical tensor-symbol rank s(a) = I(a) / width.

Equations

• Algebraic.MassProduction.CanonicalPacking.symbolIndex packingFits source = (Algebraic.MassProduction.CanonicalPacking.symbolAndBit packingFits source).1

noncomputable def Algebraic.MassProduction.CanonicalPacking.bitIndex {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : Fin width

Canonical basis coordinate j(a) = I(a) % width.

Equations

• Algebraic.MassProduction.CanonicalPacking.bitIndex packingFits source = (Algebraic.MassProduction.CanonicalPacking.symbolAndBit packingFits source).2

noncomputable def Algebraic.MassProduction.CanonicalPacking.symbolDigits {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : Fin dimension → Fin (gridWidth dimension width)

The dimension little-endian base-gridWidth digits of s(a).

Equations

• Algebraic.MassProduction.CanonicalPacking.symbolDigits packingFits source = finFunctionFinEquiv.symm (Algebraic.MassProduction.CanonicalPacking.symbolIndex packingFits source)

noncomputable def Algebraic.MassProduction.CanonicalPacking.placement {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) : Fin (2 ^ prefixWidth) ↪ (Fin dimension → Fin (gridWidth dimension width)) × Fin width

Manuscript-canonical embedding of all Boolean prefixes into information symbol coordinates and field-basis coordinates.

Equations

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

@[simp]

theorem Algebraic.MassProduction.CanonicalPacking.placement_first {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : ((placement packingFits) source).1 = symbolDigits packingFits source

@[simp]

theorem Algebraic.MassProduction.CanonicalPacking.placement_second {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : ((placement packingFits) source).2 = bitIndex packingFits source

noncomputable def Algebraic.MassProduction.CanonicalPacking.packedPlacement {width prefixWidth dimension : ℕ} (_widthPositive : 0 < width) (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) : Fin (2 ^ prefixWidth) ↪ PackedBitPosition dimension width

Under the verified binary-field cardinality, the canonical placement has exactly the PackedBitPosition type used by resource packing.

Equations

• Algebraic.MassProduction.CanonicalPacking.packedPlacement _widthPositive packingFits = Algebraic.MassProduction.CanonicalPacking.placement packingFits

@[simp]

theorem Algebraic.MassProduction.CanonicalPacking.packedPlacement_first {width prefixWidth dimension : ℕ} (widthPositive : 0 < width) (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : ((packedPlacement widthPositive packingFits) source).1 = symbolDigits packingFits source

@[simp]

theorem Algebraic.MassProduction.CanonicalPacking.packedPlacement_second {width prefixWidth dimension : ℕ} (widthPositive : 0 < width) (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : ((packedPlacement widthPositive packingFits) source).2 = bitIndex packingFits source

theorem Algebraic.MassProduction.CanonicalPacking.packedTargetPoint_bits {width prefixWidth dimension : ℕ} (widthPositive : 0 < width) (packingFits : 2 ^ prefixWidth ≤ gridWidth dimension width ^ dimension * width) (source : Fin (2 ^ prefixWidth)) : binaryExtensionVectorBits widthPositive (packedTargetPoint widthPositive (packedPlacement widthPositive packingFits) source) = fun (flat : Fin (dimension * width)) => have coordinateAndBit := finProdFinEquiv.symm flat; finiteIndexBits width (symbolDigits packingFits source coordinateAndBit.1) coordinateAndBit.2

The packed target's field-basis bits are precisely the fixed-width binary encodings of the base-conversion digits.