Structural analysis of one-output De Morgan circuits

The contracted origin of the circuit's designated output wire lies in the original program. For a function depending on at least two inputs, this origin must be a charged gate rather than a constant or a single literal.

structure Algebraic.DeMorgan.OutputRoot {n : ℕ} (circuit : Circuit signature n 1) : Type

The charged origin of a one-output circuit's terminal value.

• gate : Fin circuit.size

  Charged gate carrying the output, after contracting free gates.

• negated : Bool

  Whether the terminal free chain negates the charged gate.

• origin_eq : origins circuit.program (circuit.outputs 0) = ResidualValue.wire self.negated (Wire.gate self.gate)

  Exact contracted-origin equation for the output wire.

• charged : ChargedGate circuit.program self.gate

  The selected origin is charged.

theorem Algebraic.DeMorgan.OutputRoot.output_eq_of_gate_eq {n : ℕ} {circuit : Circuit signature n 1} (root : OutputRoot circuit) (left right : Fin n → Bool) (gate_eq : circuit.program.gateFunction interpretation root.gate left = circuit.program.gateFunction interpretation root.gate right) : circuit.eval interpretation left 0 = circuit.eval interpretation right 0

Equality at the charged root implies equality of the circuit output.

theorem Algebraic.DeMorgan.OutputRoot.gate_ne_of_output_ne {n : ℕ} {circuit : Circuit signature n 1} (root : OutputRoot circuit) (left right : Fin n → Bool) (different : circuit.eval interpretation left 0 ≠ circuit.eval interpretation right 0) : circuit.program.gateFunction interpretation root.gate left ≠ circuit.program.gateFunction interpretation root.gate right

A changed circuit output forces its charged root to change.

theorem Algebraic.DeMorgan.exists_outputRoot {n : ℕ} (circuit : Circuit signature (n + 1) 1) (positive : 0 < n) (allSupported : ∀ (input : Fin (n + 1)), input ∈ circuit.inputSupport) : Nonempty (OutputRoot circuit)

A one-output circuit structurally supported by every one of at least two inputs has a charged output root.