Raw threshold-fragment internals #

This module proves the structural and semantic invariants of the unary dynamic program defined in Complexitylib.Circuits.Encoding.Threshold.Defs. Public statements are re-exported by Complexitylib.Circuits.Encoding.Threshold.

Exact structural accounting #

theorem Complexity.CircuitCode.Threshold.length_cellGates_internal (available threshold inputRow thresholdColumn input : ℕ) :

List.length (cellGates available threshold inputRow thresholdColumn input) = 2

Internal exact size of a two-gate table cell.

theorem Complexity.CircuitCode.Threshold.length_rowPrefix_internal (available threshold inputRow input columnCount : ℕ) :

List.length (rowPrefix available threshold inputRow input columnCount) = 2 * columnCount

Internal exact size of a row prefix.

theorem Complexity.CircuitCode.Threshold.length_rows_internal (available threshold inputRow inputCount : ℕ) (refs : Fin inputCount → ℕ) :

List.length (rows available threshold inputRow inputCount refs) = 2 * inputCount * threshold

Internal exact size of a sequence of table rows.

theorem Complexity.CircuitCode.Threshold.length_compileRaw_internal (available threshold : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) :

List.length (compileRaw available threshold refs) = 3 + 2 * inputCount * threshold

Internal exact gate count for threshold compilation.

theorem Complexity.CircuitCode.Threshold.outputWire_eq_internal (available threshold : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) :

outputWire available inputCount threshold = available + List.length (compileRaw available threshold refs) - 1

Internal equation identifying the final emitted wire.

theorem Complexity.CircuitCode.Threshold.evalAux?_compileRaw_internal (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))

Internal semantic correctness theorem for raw threshold fragments.

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

Internal topological correctness theorem for raw threshold fragments.