Semantic influence paths in De Morgan programs

When changing one input changes a charged gate, some first charged reader of that input also changes and feeds the gate through the contracted charged graph. This is the semantic cut lemma used by XOR gate elimination.

theorem Algebraic.DeMorgan.InitialChargedGate.gateFunction_eq_binaryEval {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) (input : Fin n → Bool) : program.gateFunction interpretation initial.gate input = initial.op.eval (program.trace interpretation input initial.left) (program.trace interpretation input initial.right)

Evaluate an initial charged gate through its two named argument wires.

theorem Algebraic.DeMorgan.InitialChargedGate.gateFunction_eq_of_origins_eq {n g : ℕ} {program : Program signature n g} (initial : InitialChargedGate program) (left right : Fin n → Bool) (left_eq : ResidualValue.eval program left (origins program initial.left) = ResidualValue.eval program right (origins program initial.left)) (right_eq : ResidualValue.eval program left (origins program initial.right) = ResidualValue.eval program right (origins program initial.right)) : program.gateFunction interpretation initial.gate left = program.gateFunction interpretation initial.gate right

Equal contracted argument values force an initial charged gate to agree.

inductive Algebraic.DeMorgan.DifferingPath {n g : ℕ} (program : Program signature n g) (selected : Fin n) (left right : Fin n → Bool) : Fin g → Prop

A charged path that starts at a direct reader whose value changes between two assignments. The difference proof is stored only at the first gate; later gates are connected structurally.

• direct {n g : ℕ} {program : Program signature n g} {selected : Fin n} {left right : Fin n → Bool} {gate : Fin g} : ReadsInput program gate selected → program.gateFunction interpretation gate left ≠ program.gateFunction interpretation gate right → DifferingPath program selected left right gate
• step {n g : ℕ} {program : Program signature n g} {selected : Fin n} {left right : Fin n → Bool} {source target : Fin g} : DifferingPath program selected left right source → UsesGate program source target → DifferingPath program selected left right target

theorem Algebraic.DeMorgan.DifferingPath.castSucc {n g : ℕ} {program : Program signature n g} {selected : Fin n} {left right : Fin n → Bool} {gate : Fin g} (path : DifferingPath program selected left right gate) (line : Line signature n g) : DifferingPath (program.gate line) selected left right gate.castSucc

Extend a differing path through an appended program gate.

theorem Algebraic.DeMorgan.DifferingPath.exists_first {n g : ℕ} {program : Program signature n g} {selected : Fin n} {left right : Fin n → Bool} {endpoint : Fin g} (path : DifferingPath program selected left right endpoint) : ∃ (first : Fin g), ReadsInput program first selected ∧ program.gateFunction interpretation first left ≠ program.gateFunction interpretation first right ∧ (first = endpoint ∨ ∃ (next : Fin g), UsesGate program first next)

Expose the first differing direct reader on a differing path.

theorem Algebraic.DeMorgan.differingPath_of_gate_ne {n g : ℕ} (program : Program signature n g) (selected : Fin n) (left right : Fin n → Bool) (agree : ∀ (input : Fin n), input ≠ selected → left input = right input) (gate : Fin g) : ChargedGate program gate → program.gateFunction interpretation gate left ≠ program.gateFunction interpretation gate right → DifferingPath program selected left right gate

If two assignments differ only at selected and a charged gate distinguishes them, there is a differing path from a direct reader of selected to that gate.