Structural properties of packed one-step circuit fragments

This internal module connects the canonical configuration-atom ordering to the formula batch compiler. It records the exact formula and gate counts, formula lookup order, and arithmetic addresses of packed successor atoms.

theorem Complexity.CircuitUnrolling.length_stepFormulas_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : (stepFormulas tm T configBase choiceWire).length = configWidth tm T

Internal exact length of the canonical next-formula ordering.

theorem Complexity.CircuitUnrolling.getElem_stepFormulas_configIndex_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) (atom : ConfigAtom tm T) : (stepFormulas tm T configBase choiceWire)[configIndex tm T atom] = nextFormula tm T configBase choiceWire atom

Internal lookup law connecting atom indices to next-configuration formulas.

theorem Complexity.CircuitUnrolling.length_stepFragment_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : List.length (stepFragment tm T configBase choiceWire available) = stepFragmentSize tm T configBase choiceWire

Internal exact gate count of a packed one-step fragment.

theorem Complexity.CircuitUnrolling.stepOutputBase_eq_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : stepOutputBase tm T configBase choiceWire available = available + (List.map BoolFormula.size (stepFormulas tm T configBase choiceWire)).sum

Internal arithmetic description of the packed successor-block base.

theorem Complexity.CircuitUnrolling.stepOutputAddress_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (atom : ConfigAtom tm T) : stepOutputBase tm T configBase choiceWire available + configIndex tm T atom = available + (List.map BoolFormula.size (stepFormulas tm T configBase choiceWire)).sum + configIndex tm T atom

Internal absolute address of a packed successor-configuration atom.

theorem Complexity.CircuitUnrolling.configWire_stepOutputBase_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (atom : ConfigAtom tm T) : configWire tm T (stepOutputBase tm T configBase choiceWire available) atom = stepOutputBase tm T configBase choiceWire available + configIndex tm T atom

Internal bridge from packed output addresses to configuration-wire addresses.

theorem Complexity.CircuitUnrolling.stepOutputEnd_eq_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : stepOutputBase tm T configBase choiceWire available + configWidth tm T = available + stepFragmentSize tm T configBase choiceWire

Internal end address of the packed successor-configuration block.