Fixed-width binary circuit descriptions -- proof internals

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

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

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

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

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

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

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

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

@[simp]

theorem Complexity.CircuitCode.FixedWidth.Description.getElem_toRawCircuit_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (index : Fin (List.length description.toRawCircuit)) : description.toRawCircuit[↑index] = (description.activeSlot ⟨↑index, ⋯⟩).toRawGate

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

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