Raw parity-circuit fragments

The compiler in this module emits one false initializer and three shared gates per selected existing wire. It exposes exact size, topological well-formedness, and iterative evaluation theorems for use in larger raw-circuit builders.

theorem Complexity.CircuitCode.Parity.foldXor_eq_sum (count : ℕ) (bits : Fin count → Bool) : foldXor count bits = ∑ i : Fin count, bits i

The iterative XOR agrees with finite addition in the Boolean ring.

@[simp]

theorem Complexity.CircuitCode.Parity.length_compileRaw (available : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) : List.length (compileRaw available refs) = 1 + 3 * inputCount

Parity compilation emits exactly one initializer and three gates per selected wire.

theorem Complexity.CircuitCode.Parity.outputWire_eq (available : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) : outputWire available inputCount = available + List.length (compileRaw available refs) - 1

The last gate emitted by parity compilation carries its result.

theorem Complexity.CircuitCode.Parity.topologicallyWellFormed_compileRaw (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (hrefs : ∀ (i : Fin inputCount), refs i < available) : RawCircuit.TopologicallyWellFormed available (compileRaw available refs)

The parity fragment is topologically ordered whenever every selected reference names a pre-existing wire.

theorem Complexity.CircuitCode.Parity.compileRaw_wellFormed (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (hrefs : ∀ (i : Fin inputCount), refs i < available) : RawCircuit.WellFormed available (compileRaw available refs)

The parity fragment is a valid nonempty raw circuit whenever its selected references name pre-existing wires.

theorem Complexity.CircuitCode.Parity.eval?_compileRaw (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (hrefs : ∀ (i : Fin inputCount), refs i < available) (input : BitString available) : (compileRaw available refs).eval? input.toList = some (foldXor inputCount fun (i : Fin inputCount) => input ⟨refs i, ⋯⟩)

Iterative evaluation of the parity fragment returns the XOR of the selected input bits.

theorem Complexity.CircuitCode.Parity.evalAux?_compileRaw (available : ℕ) [NeZero available] {inputCount : ℕ} (refs : Fin inputCount → ℕ) (bits : Fin inputCount → Bool) (wires : Array Bool) (hsize : wires.size = available) (hrefs : ∀ (i : Fin inputCount), refs i < available) (hinputs : ∀ (i : Fin inputCount), wires[refs i]? = some (bits i)) : ∃ (result : Array Bool), (compileRaw available refs).evalAux? wires = some result ∧ result.size = wires.size + (1 + 3 * inputCount) ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[outputWire available inputCount]? = some (foldXor inputCount bits)

Fragment evaluation appends the parity value while preserving every pre-existing memo wire.