Splitting an arbitrary Boolean function into prefix and suffix inputs

The finite composition theorem accepts a function indexed by a numeric prefixWidth-bit prefix and an ordinary Boolean suffix. The headline theorem instead quantifies over an arbitrary Boolean function on the concatenated input block. This module proves that the runtime prefix encoding used by the circuit is exactly inverse to the corresponding semantic split.

All transports are explicit functions or equalities; no instances are introduced.

def Algebraic.MassProduction.InputSplit.sourceBits {prefixWidth : ℕ} (source : Fin (2 ^ prefixWidth)) : Fin prefixWidth → Bool

Decode a bounded numeric prefix into the same little-endian Boolean bits used by RuntimePacking.source.

Equations

• Algebraic.MassProduction.InputSplit.sourceBits source bit = finTwoEquiv (finFunctionFinEquiv.symm source bit)

@[simp]

theorem Algebraic.MassProduction.InputSplit.sourceBits_runtimeSource {prefixWidth : ℕ} (bits : Fin prefixWidth → Bool) : sourceBits (RuntimePacking.source bits) = bits

@[simp]

theorem Algebraic.MassProduction.InputSplit.runtimeSource_sourceBits {prefixWidth : ℕ} (source : Fin (2 ^ prefixWidth)) : RuntimePacking.source (sourceBits source) = source

Encoding the decoded bits of a bounded source returns that source.

def Algebraic.MassProduction.InputSplit.joinedInput {prefixWidth suffixWidth : ℕ} (source : Fin (2 ^ prefixWidth)) (suffix : Fin suffixWidth → Bool) : Fin (prefixWidth + suffixWidth) → Bool

Concatenate the decoded prefix and the ordinary suffix.

Equations

• Algebraic.MassProduction.InputSplit.joinedInput source suffix = Fin.append (Algebraic.MassProduction.InputSplit.sourceBits source) suffix

def Algebraic.MassProduction.InputSplit.splitFunction {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool

Semantic split of an arbitrary function on a concatenated input block.

Equations

• Algebraic.MassProduction.InputSplit.splitFunction function source suffix = function (Algebraic.MassProduction.InputSplit.joinedInput source suffix)

@[simp]

theorem Algebraic.MassProduction.InputSplit.requestFunction_splitFunction {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) : RuntimePipeline.requestFunction (splitFunction function) = function

Splitting a function and passing it through the runtime request interface recovers the original function exactly.

theorem Algebraic.MassProduction.InputSplit.booleanMassComplexity_requestFunction_splitFunction {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (copies : ℕ) : booleanMassComplexity (RuntimePipeline.requestFunction (splitFunction function)) copies = booleanMassComplexity function copies

The finite composition theorem therefore bounds the ordinary mass complexity of every function on prefixWidth + suffixWidth inputs.

Zero-cost input transport

def Algebraic.MassProduction.InputSplit.batchedInputMap {sourceWidth targetWidth : ℕ} (copies : ℕ) (inputMap : Fin sourceWidth → Fin targetWidth) : Fin (copies * sourceWidth) → Fin (copies * targetWidth)

Apply one input-index map independently in every row-major request block.

Equations

• Algebraic.MassProduction.InputSplit.batchedInputMap copies inputMap input = finProdFinEquiv ((finProdFinEquiv.symm input).1, inputMap (finProdFinEquiv.symm input).2)

theorem Algebraic.MassProduction.InputSplit.directProductInput_batchedInputMap {sourceWidth targetWidth : ℕ} {U : Sort u_1} (copies : ℕ) (inputMap : Fin sourceWidth → Fin targetWidth) (input : Fin (copies * targetWidth) → U) (copy : Fin copies) (index : Fin sourceWidth) : directProductInput (input ∘ batchedInputMap copies inputMap) copy index = directProductInput input copy (inputMap index)

theorem Algebraic.MassProduction.InputSplit.directProduct_batchedInputMap {U : Type u_1} {sourceWidth targetWidth : ℕ} (function : ScalarFunction U sourceWidth) (copies : ℕ) (inputMap : Fin sourceWidth → Fin targetWidth) (input : Fin (copies * targetWidth) → U) : directProduct function copies (input ∘ batchedInputMap copies inputMap) = directProduct (fun (block : Fin targetWidth → U) => function (block ∘ inputMap)) copies input

Reindexing the inputs of every copy commutes with direct product.

theorem Algebraic.MassProduction.InputSplit.costComplexity_reindexInputs_le {σ : Signature} {U : Type u_2} {sourceWidth outputs targetWidth : ℕ} (interpretation : Interpretation σ U) (operationCost : OperationCost σ) (target : Target U sourceWidth outputs) (inputMap : Fin sourceWidth → Fin targetWidth) : (Circuit.costComplexity interpretation operationCost fun (input : Fin targetWidth → U) (output : Fin outputs) => target (input ∘ inputMap) output) ≤ Circuit.costComplexity interpretation operationCost target

Rewiring source inputs cannot increase minimum circuit complexity.

theorem Algebraic.MassProduction.InputSplit.booleanMassComplexity_reindexInputs_le {sourceWidth targetWidth : ℕ} (function : ScalarFunction Bool sourceWidth) (copies : ℕ) (inputMap : Fin sourceWidth → Fin targetWidth) : booleanMassComplexity (fun (input : Fin targetWidth → Bool) => function (input ∘ inputMap)) copies ≤ booleanMassComplexity function copies

The scalar direct-product specialization of zero-cost input rewiring.

Padding to a convenient larger block length

def Algebraic.MassProduction.InputSplit.paddingRetraction {sourceWidth targetWidth : ℕ} (sourcePositive : 0 < sourceWidth) : Fin targetWidth → Fin sourceWidth

Retraction from a padded input block to a nonempty original block. Only its behavior on the initial embedded block matters.

Equations

• Algebraic.MassProduction.InputSplit.paddingRetraction sourcePositive input = if inside : ↑input < sourceWidth then ⟨↑input, inside⟩ else ⟨0, sourcePositive⟩

@[simp]

theorem Algebraic.MassProduction.InputSplit.paddingRetraction_castLE {sourceWidth targetWidth : ℕ} (sourcePositive : 0 < sourceWidth) (fits : sourceWidth ≤ targetWidth) (input : Fin sourceWidth) : paddingRetraction sourcePositive (Fin.castLE fits input) = input

def Algebraic.MassProduction.InputSplit.paddedFunction {sourceWidth targetWidth : ℕ} {U : Type u_1} (fits : sourceWidth ≤ targetWidth) (function : ScalarFunction U sourceWidth) : ScalarFunction U targetWidth

Extend a function to a larger input block by ignoring the padded tail.

Equations

• Algebraic.MassProduction.InputSplit.paddedFunction fits function input = function (input ∘ Fin.castLE fits)

@[simp]

theorem Algebraic.MassProduction.InputSplit.paddedFunction_retract {sourceWidth targetWidth : ℕ} {U : Type u_1} (sourcePositive : 0 < sourceWidth) (fits : sourceWidth ≤ targetWidth) (function : ScalarFunction U sourceWidth) (input : Fin sourceWidth → U) : paddedFunction fits function (input ∘ paddingRetraction sourcePositive) = function input

theorem Algebraic.MassProduction.InputSplit.booleanMassComplexity_le_paddedFunction {sourceWidth targetWidth : ℕ} (sourcePositive : 0 < sourceWidth) (fits : sourceWidth ≤ targetWidth) (function : ScalarFunction Bool sourceWidth) (copies : ℕ) : booleanMassComplexity function copies ≤ booleanMassComplexity (paddedFunction fits function) copies

Padding unused tail variables cannot make the original Boolean direct product cheaper: a circuit for the padded function rewires back at zero cost.