Streamable deterministic unrolling arithmetic — proof internals

This module proves that absolute wire bases do not affect transition-formula tree sizes, then solves the deterministic trace-prefix recurrences using the resulting constant packed-layer size.

theorem Complexity.CircuitUnrolling.size_nextFormula_eq_directStepFormulaSize_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) (atom : ConfigAtom tm T) : (nextFormula tm T configBase choiceWire atom).size = directStepFormulaSize tm T atom

theorem Complexity.CircuitUnrolling.stepFragmentSize_eq_directStepSize_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : stepFragmentSize tm T configBase choiceWire = directStepSize tm T

theorem Complexity.TM.directPrefixTraceBuild_configBase_internal {k : ℕ} (tm : TM k) (T n i : ℕ) [NeZero n] (hi : i ≤ T) : (tm.directPrefixTraceBuild T n i).configBase = n + i * CircuitUnrolling.directStepSize tm.toNTM T

theorem Complexity.TM.directPrefixTraceBuild_available_internal {k : ℕ} (tm : TM k) (T n i : ℕ) [NeZero n] (hi : i ≤ T) : (tm.directPrefixTraceBuild T n i).available = n + CircuitUnrolling.configWidth tm.toNTM T + i * CircuitUnrolling.directStepSize tm.toNTM T

theorem Complexity.TM.directPrefixTraceBuild_size_internal {k : ℕ} (tm : TM k) (T n i : ℕ) [NeZero n] (hi : i ≤ T) : (tm.directPrefixTraceBuild T n i).size = CircuitUnrolling.configWidth tm.toNTM T + i * CircuitUnrolling.directStepSize tm.toNTM T

theorem Complexity.TM.directPrefixTraceBuild_circuit_internal {k : ℕ} (tm : TM k) (T n i : ℕ) [NeZero n] (hi : i ≤ T) : (tm.directPrefixTraceBuild T n i).circuit = CircuitUnrolling.initFragment tm.toNTM T n n (CircuitUnrolling.deterministicInputWires T n) ++ List.flatMap (tm.directStepFragment T n) (List.take i (List.finRange T))

theorem Complexity.TM.directTraceFragment_eq_init_append_steps_internal {k : ℕ} (tm : TM k) (T n : ℕ) [NeZero n] : CircuitUnrolling.traceFragment tm.toNTM T n n (CircuitUnrolling.deterministicInputWires T n) = CircuitUnrolling.initFragment tm.toNTM T n n (CircuitUnrolling.deterministicInputWires T n) ++ List.flatMap (tm.directStepFragment T n) (List.finRange T)

theorem Complexity.TM.directTraceOutputBase_internal {k : ℕ} (tm : TM k) (T n : ℕ) [NeZero n] : CircuitUnrolling.traceOutputBase tm.toNTM T n n (CircuitUnrolling.deterministicInputWires T n) = n + T * CircuitUnrolling.directStepSize tm.toNTM T

theorem Complexity.TM.directUnrollingRawCircuit_eq_init_append_steps_internal {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : tm.directUnrollingRawCircuit f n = CircuitUnrolling.initFragment tm.toNTM (f n) n n (CircuitUnrolling.deterministicInputWires (f n) n) ++ List.flatMap (tm.directStepFragment (f n) n) (List.finRange (f n)) ++ [CircuitUnrolling.acceptanceGate tm.toNTM (f n) (n + f n * CircuitUnrolling.directStepSize tm.toNTM (f n))]