Correctness of raw threshold-circuit fragments

This module exposes an appendable unary dynamic-programming circuit for testing whether at least threshold referenced wires are true. For k references it uses exactly 3 + 2 * k * threshold gates: two Boolean constants, two gates per table cell, and one final output copy.

The core semantic statement uses Mathlib's dependency-light Fin.countP rather than importing the complexity-class counting layer into the circuit library. A majority adapter can rewrite this count to the library's popCount at the higher layer where both APIs are already available.

Main definitions and results

• Threshold.compileRaw: compile an at-least-threshold test over absolute wires.
• Threshold.length_compileRaw: exact gate count.
• Threshold.topologicallyWellFormed_compileRaw: every emitted reference points to the existing prefix or an earlier emitted gate.
• Threshold.evalAux?_compileRaw: exact size, prefix preservation, and semantic correctness of iterative evaluation.

@[simp]

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

Threshold compilation emits two gates per table cell, two constants, and one final copy gate.

theorem Complexity.CircuitCode.Threshold.length_compileRaw_le_quadratic (available threshold : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) (hthreshold : threshold ≤ inputCount) : List.length (compileRaw available threshold refs) ≤ 3 + 2 * inputCount * inputCount

When the requested threshold is at most the input count, the threshold fragment has the advertised quadratic gate bound.

theorem Complexity.CircuitCode.Threshold.outputWire_lt (available threshold : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) : outputWire available inputCount threshold < available + List.length (compileRaw available threshold refs)

The designated output lies inside the newly emitted fragment.

theorem Complexity.CircuitCode.Threshold.le_outputWire (available inputCount threshold : ℕ) : available ≤ outputWire available inputCount threshold

A threshold fragment's designated output is never before its existing-wire prefix.

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

The designated threshold output is the final emitted wire.

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

If every requested input names an existing wire, the threshold fragment only references the existing prefix or earlier gates in the same fragment.

theorem Complexity.CircuitCode.Threshold.evalAux?_compileRaw (available threshold : ℕ) [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 threshold refs).evalAux? wires = some result ∧ result.size = wires.size + (3 + 2 * inputCount * threshold) ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[outputWire available inputCount threshold]? = some (decide (threshold ≤ Fin.countP bits))

Successful threshold evaluation appends its exact gate count, preserves the existing memo array, and returns true exactly when at least threshold of the referenced input values are true.