Packing Boolean data into evaluation-code resource functions

For a fixed suffix, the manuscript packs requested Boolean values into basis coordinates of the tensor-code information symbols. This module states that packing through an explicit embedding and proves that punctured-line recovery returns the original Boolean coordinate.

The placement embedding is data, not a serialization typeclass. A later front-end circuit may implement any concrete placement satisfying the same interface without changing the algebraic recovery proof. Packing capacities use Nat.card, so their public types do not capture a field enumeration.

@[reducible, inline]

abbrev Algebraic.MassProduction.PackedBitPosition (dimension width : ℕ) : Type

One Boolean information position consists of a tensor-grid symbol and a basis coordinate inside that binary-extension-field symbol.

Equations

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

noncomputable def Algebraic.MassProduction.binaryResourceNodes {width : ℕ} (widthPositive : 0 < width) (dimension : ℕ) : Fin (resourceGridWidth (Nat.card (BinaryExtension width)) dimension) → BinaryExtension width

Concrete interpolation nodes: a grid index is represented by its little-endian width-bit integer and encoded in the fixed field basis. This choice connects the semantic evaluation code to the runtime packing circuit.

Equations

• Algebraic.MassProduction.binaryResourceNodes widthPositive dimension point = Algebraic.MassProduction.encodeBinaryExtension widthPositive (Algebraic.MassProduction.finiteIndexBits width point)

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

noncomputable def Algebraic.MassProduction.packedBit {Prefix : Type u} {dimension width : ℕ} (placement : Prefix ↪ PackedBitPosition dimension width) (values : Prefix → Bool) (position : PackedBitPosition dimension width) : Bool

Read the source bit assigned to a packed position, using false for an unused information coordinate. Classical choice is local to this semantic definition and does not create a global decidability instance.

Equations

• Algebraic.MassProduction.packedBit placement values position = if occupied : ∃ (source : Prefix), placement source = position then values (Classical.choose occupied) else false

theorem Algebraic.MassProduction.packedBit_at_placement {Prefix : Type u} {dimension width : ℕ} (placement : Prefix ↪ PackedBitPosition dimension width) (values : Prefix → Bool) (source : Prefix) : packedBit placement values (placement source) = values source

A placement embedding makes the lookup at every occupied coordinate exact.

noncomputable def Algebraic.MassProduction.packedMessage {Prefix : Type u} {width dimension : ℕ} (widthPositive : 0 < width) (placement : Prefix ↪ PackedBitPosition dimension width) (values : Prefix → Bool) : (Fin dimension → Fin (resourceGridWidth (Nat.card (BinaryExtension width)) dimension)) → BinaryExtension width

Pack Boolean information coordinates into one field-valued message on the tensor grid.

Equations

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

theorem Algebraic.MassProduction.decode_packedMessage_at_placement {Prefix : Type u} {width dimension : ℕ} (widthPositive : 0 < width) (placement : Prefix ↪ PackedBitPosition dimension width) (values : Prefix → Bool) (source : Prefix) : decodeBinaryExtension widthPositive (packedMessage widthPositive placement values (placement source).1) (placement source).2 = values source

Decoding an occupied coordinate of the packed message recovers its source Boolean value.

theorem Algebraic.MassProduction.decodeBinaryExtension_add {width : ℕ} (widthPositive : 0 < width) (left right : BinaryExtension width) : decodeBinaryExtension widthPositive (left + right) = decodeBinaryExtension widthPositive left + decodeBinaryExtension widthPositive right

Decoding is additive in the fixed binary basis.

theorem Algebraic.MassProduction.decodeBinaryExtension_finset_sum {width : ℕ} {Index : Type u_1} (widthPositive : 0 < width) (set : Finset Index) (values : Index → BinaryExtension width) : decodeBinaryExtension widthPositive (∑ index ∈ set, values index) = ∑ index ∈ set, decodeBinaryExtension widthPositive (values index)

Decoding commutes with a finite sum of binary-extension-field values.

noncomputable def Algebraic.MassProduction.packedEvaluationResource {Prefix : Type u} {width dimension : ℕ} {Suffix : Sort u_1} (widthPositive : 0 < width) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → Suffix → Bool) (point : Fin dimension → BinaryExtension width) (suffix : Suffix) : BinaryExtension width

Field-valued resource function induced by one packed Boolean family. The Suffix argument is the shorter input on which recursive evaluation will operate.

Equations

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

noncomputable def Algebraic.MassProduction.packedTargetPoint {Prefix : Type u} {width dimension : ℕ} (widthPositive : 0 < width) (placement : Prefix ↪ PackedBitPosition dimension width) (source : Prefix) : Fin dimension → BinaryExtension width

Tensor-grid point containing the bit assigned to one source prefix.

Equations

• Algebraic.MassProduction.packedTargetPoint widthPositive placement source = Algebraic.MassProduction.binaryResourceNodes widthPositive dimension ∘ (placement source).1

theorem Algebraic.MassProduction.packedEvaluationResource_at_target {Prefix : Type u} {width dimension : ℕ} {Suffix : Sort u_1} (widthPositive : 0 < width) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → Suffix → Bool) (source : Prefix) (suffix : Suffix) : decodeBinaryExtension widthPositive (packedEvaluationResource widthPositive placement function (packedTargetPoint widthPositive placement source) suffix) (placement source).2 = function source suffix

The packed target is systematic: its assigned basis coordinate is the original Boolean function value.

theorem Algebraic.MassProduction.packedEvaluationResource_sum_puncturedLine {Prefix : Type u} {width dimension : ℕ} {Suffix : Sort u_1} (widthPositive : 0 < width) (dimensionPositive : 0 < dimension) (placement : Prefix ↪ PackedBitPosition dimension width) (function : Prefix → Suffix → Bool) (source : Prefix) (suffix : Suffix) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : ∑ point ∈ puncturedLine (packedTargetPoint widthPositive placement source) direction, decodeBinaryExtension widthPositive (packedEvaluationResource widthPositive placement function point suffix) (placement source).2 = function source suffix

Exact Boolean-coordinate recovery from any projective punctured line through the packed information point.

theorem Algebraic.MassProduction.packedEvaluationResource_count {width dimension : ℕ} (widthPositive : 0 < width) : Nat.card (Fin dimension → BinaryExtension width) * width = (2 ^ width) ^ dimension * width

The number of Boolean resource functions is the number of ambient code points times the extension-field bit width.

theorem Algebraic.MassProduction.nonempty_packedBitPlacement_of_card_le {Prefix : Type u} {width dimension : ℕ} [Fintype Prefix] (capacity : Fintype.card Prefix ≤ resourceGridWidth (Nat.card (BinaryExtension width)) dimension ^ dimension * width) : Nonempty (Prefix ↪ PackedBitPosition dimension width)

A semantic placement exists whenever the information-bit count fits in the tensor-grid symbol capacity. This is deliberately separate from the later polynomial-size placement circuit.