Restricting one-output De Morgan circuits

The source program is restricted directly, and its designated output wire is then materialized in the residual program when necessary. Deleted charged gates are indexed by Fin source.size, the original source-gate type. The exact cost identity is exposed as a standard Circuit.Reduction certificate.

structure Algebraic.DeMorgan.CircuitRestriction {n : ℕ} (source : Circuit signature (n + 1) 1) (selected : Fin (n + 1)) (fixedValue : Bool) : Type

Restriction of a one-output De Morgan circuit, with the exact set of deleted charged source gates.

• result : Circuit signature n 1

  Residual circuit on the remaining inputs.

• deleted : Finset (Fin source.size)

  Deleted charged gates in the original source program.

• eval_eq (input : Fin n → Bool) : self.result.eval interpretation input = source.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input)

  Pointwise semantics under the chosen input restriction.

• cost_eq : self.deleted.card + self.result.cost binaryCost = source.cost binaryCost

  The deletion set accounts exactly for the charged-cost decrease.

@[reducible, inline]

abbrev Algebraic.DeMorgan.CircuitRestriction.gateCount {n : ℕ} {source : Circuit signature (n + 1) 1} {selected : Fin (n + 1)} {fixedValue : Bool} (restriction : CircuitRestriction source selected fixedValue) : ℕ

Number of internal gates in the residual circuit.

Equations

• restriction.gateCount = restriction.result.size

def Algebraic.DeMorgan.CircuitRestriction.ofProgram {n : ℕ} {source : Circuit signature (n + 1) 1} {selected : Fin (n + 1)} {fixedValue : Bool} (program : ProgramRestriction source.program selected fixedValue) : CircuitRestriction source selected fixedValue

Materialize the residual value of the designated source output, using at most one free gate for a constant or a negation.

Equations

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

def Algebraic.DeMorgan.CircuitRestriction.toReduction {n : ℕ} {source : Circuit signature (n + 1) 1} {selected : Fin (n + 1)} {fixedValue : Bool} (restriction : CircuitRestriction source selected fixedValue) : Circuit.Reduction binaryCost source interpretation (InputSubstitution.fix selected fixedValue)

View an exact circuit restriction as a generic certified reduction.

Equations

• restriction.toReduction = { result := restriction.result, eval_eq := ⋯, saving := restriction.deleted.card, saving_le := ⋯ }

noncomputable def Algebraic.DeMorgan.restrictCircuit {n : ℕ} (source : Circuit signature (n + 1) 1) (selected : Fin (n + 1)) (fixedValue : Bool) : CircuitRestriction source selected fixedValue

Partial-evaluate a one-output circuit after fixing one input.

Equations

• Algebraic.DeMorgan.restrictCircuit source selected fixedValue = Algebraic.DeMorgan.CircuitRestriction.ofProgram (Algebraic.DeMorgan.restrictProgram selected fixedValue source.program)

@[simp]

theorem Algebraic.DeMorgan.restrictCircuit_deleted {n : ℕ} (source : Circuit signature (n + 1) 1) (selected : Fin (n + 1)) (fixedValue : Bool) : (restrictCircuit source selected fixedValue).deleted = (restrictProgram selected fixedValue source.program).deleted

Circuit restriction exposes exactly the source program's deletion set.