Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Evaluation.Sequence

Sequential fixed-width gate evaluation #

This module exposes the exact length and topological correctness of the raw fragment that computes every fixed-width gate slot in sequence.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_stepCircuit {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
List.length (stepCircuit inputWidth gateBound slot) = GateFormula.gateSize inputWidth gateBound slot

A compiled gate step emits exactly its advertised formula size.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_stepCircuitAt (inputWidth gateBound index : ℕ) :
List.length (stepCircuitAt inputWidth gateBound index) = EvaluationLayout.sizeAt inputWidth gateBound index

The total natural-index step builder agrees with the numeric size oracle.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_prefixCircuit (inputWidth gateBound count : ℕ) :
List.length (prefixCircuit inputWidth gateBound count) = EvaluationLayout.prefixSize inputWidth gateBound count

A prefix circuit emits exactly its corresponding formula-size prefix.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_circuit (inputWidth gateBound : ℕ) :
List.length (circuit inputWidth gateBound) = EvaluationLayout.prefixSize inputWidth gateBound gateBound

The complete gate sequence has the full bounded formula-size prefix.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.topologicallyWellFormed_stepCircuit {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
RawCircuit.TopologicallyWellFormed (EvaluationLayout.stepAvailable inputWidth gateBound slot) (stepCircuit inputWidth gateBound slot)

Every compiled gate step references only its entry prefix or gates emitted earlier in that formula fragment.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.topologicallyWellFormed_prefixCircuit (inputWidth gateBound count : ℕ) (hcount : count ≤ gateBound) :
RawCircuit.TopologicallyWellFormed (EvaluationLayout.baseWireCount inputWidth gateBound) (prefixCircuit inputWidth gateBound count)

Every in-range sequential prefix is topologically well formed from the description-and-sample input block.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.topologicallyWellFormed_circuit (inputWidth gateBound : ℕ) :
RawCircuit.TopologicallyWellFormed (EvaluationLayout.baseWireCount inputWidth gateBound) (circuit inputWidth gateBound)

The complete bounded gate sequence is topologically well formed.