Polynomial overhead bounds for the finite Uhlig layer

This module bounds the routing and decoding overhead of the complete finite Uhlig layer. The result is an explicit polynomial bound used by the quantitative recursion; no asymptotic claim is hidden in this module.

Polynomial overhead bounds for the shared layer

theorem Algebraic.MassProduction.UhligCircuit.sourceIndicatorExpression_standardCost_le {prefixWidth suffixWidth : ℕ} (side : Fin 2) (source : Fin (prefixLast prefixWidth + 1)) : (sourceIndicatorExpression side source).standardCost ≤ 2 * prefixWidth

Prefix-equality testing costs at most two gates per tested bit.

theorem Algebraic.MassProduction.UhligCircuit.stateSourceIndicatorExpression_standardCost_le {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (source : Fin (prefixLast prefixWidth + 1)) : (stateSourceIndicatorExpression pair side source).standardCost ≤ 2 * prefixWidth

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.fixedRoutedSuffixExpression_standardCost {prefixWidth suffixWidth : ℕ} (first second : Fin (prefixLast prefixWidth + 1)) (resource : Fin (prefixLast prefixWidth + 2)) (bit : Fin suffixWidth) : (fixedRoutedSuffixExpression first second resource bit).standardCost = 0

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.resourceRouterCircuit_cost {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) : (resourceRouterCircuit resource).cost DeMorgan.standardCost = ∑ bit : Fin suffixWidth, (routedSuffixExpression resource bit).standardCost

def Algebraic.MassProduction.UhligCircuit.routedSuffixCostBound (prefixWidth : ℕ) : ℕ

A direct polynomial bound for one routed suffix bit.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.routedSuffixExpression_standardCost_le {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) (bit : Fin suffixWidth) : (routedSuffixExpression resource bit).standardCost ≤ routedSuffixCostBound prefixWidth

theorem Algebraic.MassProduction.UhligCircuit.resourceRouterCircuit_cost_le {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) : (resourceRouterCircuit resource).cost DeMorgan.standardCost ≤ suffixWidth * routedSuffixCostBound prefixWidth

theorem Algebraic.MassProduction.UhligCircuit.candidatePostprocessExpression_cost : candidatePostprocessExpression.circuit.cost DeMorgan.standardCost = 2

def Algebraic.MassProduction.UhligCircuit.candidateDecodedCostBound (prefixWidth : ℕ) : ℕ

Uniform charged cost bound for one hardwired source-pair candidate.

Equations

• Algebraic.MassProduction.UhligCircuit.candidateDecodedCostBound prefixWidth = 4 * prefixWidth + 4 * (Algebraic.MassProduction.UhligCircuit.prefixLast prefixWidth + 2) + 2

theorem Algebraic.MassProduction.UhligCircuit.candidateDecodedCircuit_cost_le {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : (candidateDecodedCircuit pair side first second).cost DeMorgan.standardCost ≤ candidateDecodedCostBound prefixWidth

def Algebraic.MassProduction.UhligCircuit.candidateRowCostBound (prefixWidth : ℕ) : ℕ

Uniform row cost after OR-ing over the second source.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.candidateRowCircuit_cost_le {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first : Fin (prefixLast prefixWidth + 1)) : (candidateRowCircuit pair side first).cost DeMorgan.standardCost ≤ candidateRowCostBound prefixWidth

def Algebraic.MassProduction.UhligCircuit.sharedDecodedCostBound (prefixWidth : ℕ) : ℕ

Uniform charged cost bound for one requested-output decoder.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.sharedDecodedCircuit_cost_le {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) : (sharedDecodedCircuit pair side).cost DeMorgan.standardCost ≤ sharedDecodedCostBound prefixWidth

theorem Algebraic.MassProduction.UhligCircuit.sharedDecoderCircuit_cost_le (prefixWidth suffixWidth pairs : ℕ) : (sharedDecoderCircuit prefixWidth suffixWidth pairs).cost DeMorgan.standardCost ≤ 2 * pairs * sharedDecodedCostBound prefixWidth

theorem Algebraic.MassProduction.UhligCircuit.resourceRoutingBankCost_le (prefixWidth suffixWidth pairs : ℕ) : ∑ resource : Fin (prefixLast prefixWidth + 2), ∑ _pair : Fin pairs, (resourceRouterCircuit resource).cost DeMorgan.standardCost ≤ (prefixLast prefixWidth + 2) * (pairs * (suffixWidth * routedSuffixCostBound prefixWidth))

Uniform routing cost across all resources and request pairs.

def Algebraic.MassProduction.UhligCircuit.sharedLayerOverheadBound (prefixWidth suffixWidth pairs : ℕ) : ℕ

Polynomial overhead added by one shared Uhlig layer.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.sharedUhligLayerCircuit_cost_le_resource_sum_add_overhead {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (sharedUhligLayerCircuit pairs resourceCircuits).cost DeMorgan.standardCost ≤ ∑ resource : Fin (prefixLast prefixWidth + 2), (resourceCircuits resource).cost DeMorgan.standardCost + sharedLayerOverheadBound prefixWidth suffixWidth pairs

The shared finite layer costs the sum of its recursive resource circuits plus an explicit polynomial overhead.