Fixed-width binary circuit descriptions

Bounded descriptions use one fixed-width gate array. Reference words have a positive ceiling-logarithmic width, active gates are topologically ordered, and inactive slots are canonically zero. This gives the approximate-counting relation a finite, parser-free syntax while retaining RawCircuit semantics.

theorem Complexity.CircuitCode.FixedWidth.one_le_referenceWidth (inputWidth gateBound : ℕ) : 1 ≤ referenceWidth inputWidth gateBound

Reference words always have positive width.

theorem Complexity.CircuitCode.FixedWidth.one_le_gateCountWidth (gateBound : ℕ) : 1 ≤ gateCountWidth gateBound

Gate-count words always have positive width.

theorem Complexity.CircuitCode.FixedWidth.inputWidth_add_gateBound_le_two_pow_referenceWidth (inputWidth gateBound : ℕ) : inputWidth + gateBound ≤ 2 ^ referenceWidth inputWidth gateBound

The reference width represents every primary or bounded gate wire.

theorem Complexity.CircuitCode.FixedWidth.gateBound_lt_two_pow_gateCountWidth (gateBound : ℕ) : gateBound < 2 ^ gateCountWidth gateBound

Every allowed positive gate count fits in the count word.

theorem Complexity.CircuitCode.FixedWidth.card_gateSlot (width : ℕ) : Fintype.card (GateSlot width) = 2 ^ (3 + 2 * width)

A gate slot has exactly as many values as its advertised bit width.

theorem Complexity.CircuitCode.FixedWidth.card_description (inputWidth gateBound : ℕ) : Fintype.card (Description inputWidth gateBound) = (gateBound + 1) * 2 ^ (gateBound * gateSlotWidth inputWidth gateBound)

Exact number of bounded descriptions before imposing validity.

theorem Complexity.CircuitCode.FixedWidth.Description.gateCountNat_le_gateBound {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : description.gateCountNat ≤ gateBound

The active count is within the fixed gate array.

@[simp]

theorem Complexity.CircuitCode.FixedWidth.Description.length_toRawCircuit {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : List.length description.toRawCircuit = description.gateCountNat

Converting active slots to raw syntax preserves the exact gate count.

theorem Complexity.CircuitCode.FixedWidth.Description.topologicallyWellFormed_toRawCircuit_iff {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : RawCircuit.TopologicallyWellFormed inputWidth description.toRawCircuit ↔ description.TopologicallyWellFormed

Fixed-slot and raw-list topological validity agree exactly.

theorem Complexity.CircuitCode.FixedWidth.Description.wellFormed_toRawCircuit {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) : RawCircuit.WellFormed inputWidth description.toRawCircuit

A valid fixed-width description produces a valid raw circuit.