Documentation

Complexitylib.Algebraic.Basis.DeMorgan.Origin

Charged origins in De Morgan programs #

origins follows zero-cost constants, identities, and negations, but stops at an input or an AND/OR gate. It is the structural view used by gate elimination: zero-cost chains disappear without changing the underlying Program/Circuit representation.

source
def Algebraic.DeMorgan.lineOrigin {n g h : ℕ} (line : Line signature n g) (values : Wire n g → ResidualValue n h) (fresh : Wire n h) :
ResidualValue n h

Evaluate one source line symbolically from already-computed origins. fresh names the line's own output and is used exactly for charged binary operations.

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.DeMorgan.lineOrigin_not {n g h : ℕ} (wires : Fin 1 → Wire n g) (values : Wire n g → ResidualValue n h) (fresh : Wire n h) :
    lineOrigin { op := Op.not, wires := wires } values fresh = (values (wires 0)).negate
    source
    def Algebraic.DeMorgan.gateOrigins {n g : ℕ} (program : Program signature n g) :
    Fin g → ResidualValue n g

    The charged origin of each internal gate output.

    Equations
    Instances For
      source
      def Algebraic.DeMorgan.origins {n g : ℕ} (program : Program signature n g) :
      Wire n g → ResidualValue n g

      The charged origin of every wire: a constant, a signed input, or a signed AND/OR-gate output. Free internal gates are followed transitively.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Algebraic.DeMorgan.origins_input {n g : ℕ} (program : Program signature n g) (input : Fin n) :
        origins program (Wire.input input) = ResidualValue.wire false (Wire.input input)
        source
        @[simp]
        theorem Algebraic.DeMorgan.origins_gateWire {n g : ℕ} (program : Program signature n g) (gate : Fin g) :
        origins program (Wire.gate gate) = gateOrigins program gate
        source
        @[simp]
        theorem Algebraic.DeMorgan.liftedOrigins_apply {n g : ℕ} (program : Program signature n g) (wire : Wire n g) :
        Wire.elim (fun (input : Fin n) => ResidualValue.wire false (Wire.input input)) (fun (oldGate : Fin g) => ResidualValue.mapWires Wire.Renaming.castSucc.apply (gateOrigins program oldGate)) wire = ResidualValue.mapWires Wire.Renaming.castSucc.apply (origins program wire)

        The origin map lifted through one appended gate.

        source
        @[simp]
        theorem Algebraic.DeMorgan.gateOrigins_gate_castSucc {n g : ℕ} (program : Program signature n g) (line : Line signature n g) (gate : Fin g) :
        gateOrigins (program.gate line) gate.castSucc = ResidualValue.mapWires Wire.Renaming.castSucc.apply (gateOrigins program gate)
        source
        @[simp]
        theorem Algebraic.DeMorgan.gateOrigins_gate_last {n g : ℕ} (program : Program signature n g) (line : Line signature n g) :
        gateOrigins (program.gate line) (Fin.last g) = lineOrigin line (Wire.elim (fun (input : Fin n) => ResidualValue.wire false (Wire.input input)) fun (oldGate : Fin g) => ResidualValue.mapWires Wire.Renaming.castSucc.apply (gateOrigins program oldGate)) (Wire.gate (Fin.last g))
        source
        @[simp]
        theorem Algebraic.DeMorgan.origins_gate_castSucc {n g : ℕ} (program : Program signature n g) (line : Line signature n g) (wire : Wire n g) :
        origins (program.gate line) wire.castSucc = ResidualValue.mapWires Wire.Renaming.castSucc.apply (origins program wire)
        source
        theorem Algebraic.DeMorgan.origins_gate_last {n g : ℕ} (program : Program signature n g) (line : Line signature n g) :
        origins (program.gate line) (Wire.gate (Fin.last g)) = lineOrigin line (Wire.elim (fun (input : Fin n) => ResidualValue.wire false (Wire.input input)) fun (oldGate : Fin g) => ResidualValue.mapWires Wire.Renaming.castSucc.apply (gateOrigins program oldGate)) (Wire.gate (Fin.last g))
        source
        theorem Algebraic.DeMorgan.origins_gateWire_last_of_charged {n g : ℕ} (program : Program signature n g) (line : Line signature n g) (charged : binaryCost line.op = 1) :
        origins (program.gate line) (Wire.gate (Fin.last g)) = ResidualValue.wire false (Wire.gate (Fin.last g))

        A charged newly-appended gate is its own origin.

        source
        theorem Algebraic.DeMorgan.origins_last_of_charged {n g : ℕ} (program : Program signature n g) (line : Line signature n g) (charged : binaryCost line.op = 1) :
        origins (program.gate line) (Wire.gate (Fin.last g)) = ResidualValue.wire false (Wire.gate (Fin.last g))

        Last-wire spelling of origins_gateWire_last_of_charged. With inductive wires the last wire is Wire.gate (Fin.last g), so the two statements agree.

        source
        theorem Algebraic.DeMorgan.origins_gateWire_last_false {n g : ℕ} (program : Program signature n g) (wires : Fin 0 → Wire n g) :
        origins (program.gate { op := Op.false, wires := wires }) (Wire.gate (Fin.last g)) = ResidualValue.constant false
        source
        theorem Algebraic.DeMorgan.origins_gateWire_last_true {n g : ℕ} (program : Program signature n g) (wires : Fin 0 → Wire n g) :
        origins (program.gate { op := Op.true, wires := wires }) (Wire.gate (Fin.last g)) = ResidualValue.constant true
        source
        theorem Algebraic.DeMorgan.origins_gateWire_last_id {n g : ℕ} (program : Program signature n g) (wires : Fin 1 → Wire n g) :
        origins (program.gate { op := Op.id, wires := wires }) (Wire.gate (Fin.last g)) = ResidualValue.mapWires Wire.Renaming.castSucc.apply (origins program (wires 0))
        source
        theorem Algebraic.DeMorgan.origins_gateWire_last_not {n g : ℕ} (program : Program signature n g) (wires : Fin 1 → Wire n g) :
        origins (program.gate { op := Op.not, wires := wires }) (Wire.gate (Fin.last g)) = (ResidualValue.mapWires Wire.Renaming.castSucc.apply (origins program (wires 0))).negate
        source
        def Algebraic.DeMorgan.originSupport {n g : ℕ} (program : Program signature n g) :
        ResidualValue n g → Finset (Fin n)

        A residual value's structural input support.

        Equations
        Instances For
          source
          @[simp]
          theorem Algebraic.DeMorgan.originSupport_constant {n g : ℕ} (program : Program signature n g) (value : Bool) :
          originSupport program (ResidualValue.constant value) = ∅
          source
          @[simp]
          theorem Algebraic.DeMorgan.originSupport_wire {n g : ℕ} (program : Program signature n g) (negated : Bool) (wire : Wire n g) :
          originSupport program (ResidualValue.wire negated wire) = program.wireSupport wire
          source
          @[simp]
          theorem Algebraic.DeMorgan.originSupport_negate {n g : ℕ} (value : ResidualValue n g) (program : Program signature n g) :
          originSupport program value.negate = originSupport program value
          source
          @[simp]
          theorem Algebraic.DeMorgan.originSupport_map_castSucc {n g : ℕ} (value : ResidualValue n g) (program : Program signature n g) (line : Line signature n g) :
          originSupport (program.gate line) (ResidualValue.mapWires Wire.Renaming.castSucc.apply value) = originSupport program value
          source
          @[simp]
          theorem Algebraic.DeMorgan.eval_map_castSucc {n g : ℕ} (value : ResidualValue n g) (program : Program signature n g) (line : Line signature n g) (input : Fin n → Bool) :
          ResidualValue.eval (program.gate line) input (ResidualValue.mapWires Wire.Renaming.castSucc.apply value) = ResidualValue.eval program input value
          source
          theorem Algebraic.DeMorgan.origins_support {n g : ℕ} (program : Program signature n g) (wire : Wire n g) :
          originSupport program (origins program wire) = program.wireSupport wire

          Following free gates preserves structural input support exactly.

          source
          def Algebraic.DeMorgan.ValidOrigin {n g : ℕ} (program : Program signature n g) :
          ResidualValue n g → Prop

          An origin is an input or the output of a charged internal gate.

          Equations
          Instances For
            source
            theorem Algebraic.DeMorgan.validOrigin_negate {n g : ℕ} {program : Program signature n g} {value : ResidualValue n g} (valid : ValidOrigin program value) :
            ValidOrigin program value.negate
            source
            theorem Algebraic.DeMorgan.validOrigin_map_castSucc {n g : ℕ} {program : Program signature n g} (line : Line signature n g) {value : ResidualValue n g} (valid : ValidOrigin program value) :
            ValidOrigin (program.gate line) (ResidualValue.mapWires Wire.Renaming.castSucc.apply value)
            source
            theorem Algebraic.DeMorgan.origins_valid {n g : ℕ} (program : Program signature n g) (wire : Wire n g) :
            ValidOrigin program (origins program wire)

            Every value returned by Program.origins is a valid charged origin.

            source
            theorem Algebraic.DeMorgan.origins_eval {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) (wire : Wire n g) :
            ResidualValue.eval program input (origins program wire) = program.trace interpretation input wire

            Origins evaluate to the values of the source wires they summarize.