Routing repeated input reads through their preceding copies

Circuit.WellFormed bounds gate fan-out, but permits arbitrarily many gates to read the same external input. For bounded-degree consistency polynomials, the first such gate reads the external variable and each later one reads the preceding input gate's variable. This changes neither the variables nor the Boolean gate values. Each variable supplies at most one of these copy links.

def MIPRE.SAT.Circuit.inputOwner (C : Circuit) : ℕ → ℕ → ℕ

One plus the last gate reading input i before gate k, or zero if none.

Equations

• C.inputOwner 0 x✝ = 0
• C.inputOwner k.succ x✝ = if C.gates.getD k (MIPRE.SAT.Gate.const false) = MIPRE.SAT.Gate.input x✝ then k + 1 else C.inputOwner k x✝

theorem MIPRE.SAT.Circuit.inputOwner_le (C : Circuit) (k i : ℕ) : C.inputOwner k i ≤ k

theorem MIPRE.SAT.Circuit.inputOwner_mono (C : Circuit) (i : ℕ) : Monotone fun (k : ℕ) => C.inputOwner k i

theorem MIPRE.SAT.Circuit.inputOwner_spec (C : Circuit) (k i : ℕ) (h : C.inputOwner k i ≠ 0) : C.gates.getD (C.inputOwner k i - 1) (Gate.const false) = Gate.input i

theorem MIPRE.SAT.Circuit.inputOwner_after (C : Circuit) {a b i : ℕ} (hab : a < b) (ha : C.gates.getD a (Gate.const false) = Gate.input i) : a + 1 ≤ C.inputOwner b i

def MIPRE.SAT.Circuit.inputRef (C : Circuit) (k i : ℕ) : ℕ ⊕ ℕ

The input-copy link: external input on the first read, previous gate thereafter.

Equations

• C.inputRef k i = if C.inputOwner k i = 0 then Sum.inl i else Sum.inr (C.inputOwner k i - 1)

theorem MIPRE.SAT.Circuit.inputRef_ne_of_lt (C : Circuit) {a b i j : ℕ} (hab : a < b) (ha : C.gates.getD a (Gate.const false) = Gate.input i) (he : C.inputRef a i = C.inputRef b j) : False

theorem MIPRE.SAT.Circuit.inputRef_injective (C : Circuit) {a b i j : ℕ} (ha : C.gates.getD a (Gate.const false) = Gate.input i) (hb : C.gates.getD b (Gate.const false) = Gate.input j) (he : C.inputRef a i = C.inputRef b j) : a = b

Each external input or previous input gate is used by at most one copy link.

theorem MIPRE.SAT.Circuit.inputRef_cases (C : Circuit) (k i : ℕ) : C.inputRef k i = Sum.inl i ∨ ∃ u < k, C.inputRef k i = Sum.inr u ∧ C.gates.getD u (Gate.const false) = Gate.input i

A copy link points to an input variable or to a strictly earlier gate.

def MIPRE.SAT.Circuit.RoutedConsistent (C : Circuit) (x w : ℕ → Bool) : Prop

Consistency equations after replacing repeated external reads by copy links.

Equations

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

theorem MIPRE.SAT.Circuit.inputRef_value (C : Circuit) (x w : ℕ → Bool) (k i : ℕ) (hw : ∀ u < k, w u = C.valueAt x u) : Sum.elim x w (C.inputRef k i) = x i

theorem MIPRE.SAT.Circuit.routedConsistent_iff (C : Circuit) (x w : ℕ → Bool) : C.RoutedConsistent x w ↔ ∀ k < C.size, w k = C.valueAt x k

Routing imposes exactly the original gate values on all the same variables.

theorem MIPRE.SAT.Circuit.eval_iff_routedConsistent (C : Circuit) (hne : C.gates ≠ []) (x : ℕ → Bool) : C.eval x = true ↔ ∃ (w : ℕ → Bool), C.RoutedConsistent x w ∧ w (C.size - 1) = true

The routed consistency equations and the output literal characterize acceptance, using exactly the original input and gate variables.