Gate-elimination lower-bound framework

The framework separates three concerns:

• a circuit basis supplies certified reductions;
• a target family identifies how substitutions move between problems; and
• a well-founded rank and claimed bound turn local cost savings into a global lower bound.

No normalization strategy or algebraic law is assumed here. Those belong to the basis-specific construction of Circuit.Reduction certificates.

structure Algebraic.GateElimination.Problem (U : Type u) (m : ℕ) : Type u

One target-computation problem with a fixed number of outputs.

• inputCount : ℕ

  Number of inputs to the target.

• target : Target U self.inputCount m

  Target function to be computed.

structure Algebraic.GateElimination.Problem.Restriction {U : Type u_1} {m : ℕ} (source target : Problem U m) : Type u_1

A substitution under which one target problem becomes another.

• substitution : InputSubstitution U source.inputCount target.inputCount

  Express every source input using the target inputs.

• target_eq : source.target.substitute self.substitution = target.target

  The restricted source target is exactly the new target.

structure Algebraic.GateElimination.Step {σ : Signature} {U : Type u_2} {m : ℕ} {State : Type s} (operationCost : OperationCost σ) (interpretation : Interpretation σ U) (problem : State → Problem U m) (rank bound : State → ℕ) (state : State) (circuit : Circuit σ (problem state).inputCount m) : Type (max (max s u_1) u_2)

One certified gate-elimination step between states in a target family.

• next : State

  State reached after the restriction.

• rank_lt : rank self.next < rank state

  Gate elimination makes well-founded progress.

• restriction : (problem state).Restriction (problem self.next)

  The target family is preserved by the chosen restriction.

• reduction : Circuit.Reduction operationCost circuit interpretation self.restriction.substitution

  Basis-specific residual circuit and its certified cost saving.

• progress : bound state ≤ self.reduction.saving + bound self.next

  The local saving pays for the decrease in the claimed lower bound.

theorem Algebraic.GateElimination.Step.result_computes {σ✝ : Signature} {operationCost : OperationCost σ✝} {Carrier✝ : Type u_2} {interpretation : Interpretation σ✝ Carrier✝} {State✝ : Type u_3} {m✝ : ℕ} {problem : State✝ → Problem Carrier✝ m✝} {rank bound : State✝ → ℕ} {state : State✝} {circuit : Circuit σ✝ (problem state).inputCount m✝} (step : Step operationCost interpretation problem rank bound state circuit) (computes : circuit.ComputesWith interpretation (problem state).target) : step.reduction.result.ComputesWith interpretation (problem step.next).target

The residual circuit in a step computes the next target problem.

structure Algebraic.GateElimination.Framework {σ : Signature} {U : Type u_2} {State : Type s} (operationCost : OperationCost σ) (interpretation : Interpretation σ U) (m : ℕ) : Type (max (max s u_1) u_2)

A gate-elimination scheme for a state-indexed family of target problems.

• problem : State → Problem U m

  Target problem represented by each state.

• rank : State → ℕ

  Well-founded measure used by the elimination induction.

• bound : State → ℕ

  Claimed circuit-cost lower bound at each state.

• reduce (state : State) : 0 < self.bound state → (circuit : Circuit σ (self.problem state).inputCount m) → circuit.ComputesWith interpretation (self.problem state).target → Step operationCost interpretation self.problem self.rank self.bound state circuit

  Every positive-bound computation admits a paying elimination step.

structure Algebraic.GateElimination.OptimalFramework {σ : Signature} {U : Type u_2} {State : Type s} (operationCost : OperationCost σ) (interpretation : Interpretation σ U) (m : ℕ) : Type (max (max s u_1) u_2)

A gate-elimination scheme whose local argument only needs to handle minimum-cost circuits. This matches the usual form of structural elimination proofs while still yielding a theorem about every circuit.

• problem : State → Problem U m

  Target problem represented by each state.

• rank : State → ℕ

  Well-founded measure used by the elimination induction.

• bound : State → ℕ

  Claimed circuit-cost lower bound at each state.

• reduce (state : State) : 0 < self.bound state → (circuit : Circuit σ (self.problem state).inputCount m) → circuit.ComputesWith interpretation (self.problem state).target → Circuit.CostSizeMinimal operationCost circuit interpretation (self.problem state).target → Step operationCost interpretation self.problem self.rank self.bound state circuit

  Every positive-bound, minimum-cost computation admits a paying step.

theorem Algebraic.GateElimination.Framework.lowerBound {σ : Signature} {U : Type u} {State : Type s} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {m : ℕ} (framework : Framework operationCost interpretation m) (state : State) (circuit : Circuit σ (framework.problem state).inputCount m) : circuit.ComputesWith interpretation (framework.problem state).target → framework.bound state ≤ circuit.cost operationCost

Local certified reductions telescope to the claimed lower bound.

noncomputable def Algebraic.GateElimination.OptimalFramework.toFramework {σ : Signature} {U : Type u_2} {State : Type s} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {m : ℕ} (optimalFramework : OptimalFramework operationCost interpretation m) : Framework operationCost interpretation m

Choose a minimum-cost representative before applying each optimal-circuit step, and rebase the resulting reduction onto the caller's circuit. This is a proof-level construction using the classical choice made by Circuit.minimum.

Equations

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

theorem Algebraic.GateElimination.OptimalFramework.lowerBound {σ : Signature} {U : Type u_2} {State : Type s} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {m : ℕ} (optimalFramework : OptimalFramework operationCost interpretation m) (state : State) (circuit : Circuit σ (optimalFramework.problem state).inputCount m) : circuit.ComputesWith interpretation (optimalFramework.problem state).target → optimalFramework.bound state ≤ circuit.cost operationCost

An optimal-circuit gate-elimination scheme proves its bound for all circuits.