Regularly padded deterministic unrolling families

For positive input length n, the direct tableau is padded to its closed cubic gate bound and followed by one copy of its original acceptance wire. Thus the raw gate count is known before serialization, while evaluation remains exactly the deterministic bounded-run answer. The zero-length member retains the library's explicit answer-bit convention.

Main results

• TM.paddedDirectUnrollingRawCircuit_length gives the exact closed gate count.
• TM.paddedDirectUnrollingRawCircuit_wellFormed validates the padded syntax.
• TM.paddedDirectUnrollingCircuitFamily_encodeAt identifies the exact code map.
• TM.DecidesInTime.paddedDirectUnrollingCircuitFamily_decides proves correctness.
• TM.paddedDirectUnrollingCircuitFamily_size_bigO retains the cubic size bound.

theorem Complexity.TM.directUnrollingRawCircuit_length_le_gateBound {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : List.length (tm.directUnrollingRawCircuit f n) ≤ tm.directUnrollingGateBound f n

The unpadded positive tableau fits within its closed padding budget.

@[simp]

theorem Complexity.TM.paddedDirectUnrollingRawCircuit_length {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : List.length (tm.paddedDirectUnrollingRawCircuit f n) = tm.directUnrollingGateBound f n + 1

Every positive padded member has exactly the closed tableau bound plus its terminal output-copy gate.

theorem Complexity.TM.paddedDirectUnrollingRawCircuit_wellFormed {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : CircuitCode.RawCircuit.WellFormed n (tm.paddedDirectUnrollingRawCircuit f n)

The padded gate stream is nonempty and every reference points strictly backward. In particular, the final gate may safely copy the original last gate through the dead padding.

theorem Complexity.TM.paddedDirectUnrollingRawCircuit_eval? {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] (x : BitString n) : (tm.paddedDirectUnrollingRawCircuit f n).eval? x.toList = some (CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f n) x fun (x : Fin (f n)) => false)

Raw evaluation of a padded positive member is exactly deterministic bounded acceptance.

noncomputable def Complexity.TM.paddedDirectUnrollingCircuit {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : Circuit Basis.andOr2 n 1 (List.length (tm.paddedDirectUnrollingRawCircuit f n) - 1)

Reconstruct a positive padded raw member as a typed single-output circuit.

Equations

• tm.paddedDirectUnrollingCircuit f n = Complexity.CircuitCode.RawCircuit.toCircuit n (tm.paddedDirectUnrollingRawCircuit f n) ⋯

noncomputable def Complexity.TM.paddedDirectUnrollingCircuitFamily {k : ℕ} (tm : TM k) (f : ℕ → ℕ) : CircuitFamily Basis.andOr2

Total family of regularly padded direct-unrolling circuits.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.paddedDirectUnrollingCircuit_eval {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] (x : BitString n) : (tm.paddedDirectUnrollingCircuit f n).eval x 0 = CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f n) x fun (x : Fin (f n)) => false

The reconstructed positive circuit computes deterministic bounded acceptance.

theorem Complexity.TM.paddedDirectUnrollingCircuitFamily_function {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) (x : BitString n) : (tm.paddedDirectUnrollingCircuitFamily f).function n x = CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f n) x fun (x : Fin (f n)) => false

The total padded family computes the same bounded deterministic trace bit at every input length.

theorem Complexity.TM.paddedDirectUnrollingCircuitFamily_encodeAt_zero {k : ℕ} (tm : TM k) (f : ℕ → ℕ) : (tm.paddedDirectUnrollingCircuitFamily f).encodeAt 0 = [false, CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f 0) (fun (i : Fin 0) => i.elim0) fun (x : Fin (f 0)) => false]

The zero-length code is the same explicit tagged bounded-run answer as for the direct family.

theorem Complexity.TM.paddedDirectUnrollingCircuitFamily_encodeAt_succ {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : (tm.paddedDirectUnrollingCircuitFamily f).encodeAt (n + 1) = true :: (tm.paddedDirectUnrollingRawCircuit f (n + 1)).encode

A positive family member serializes to exactly the padded raw gate stream.

theorem Complexity.TM.paddedDirectUnrollingCircuitFamily_encodeAt {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : (tm.paddedDirectUnrollingCircuitFamily f).encodeAt n = tm.paddedDirectUnrollingCode f n

The family codec agrees at every length with the explicit padded code map.

theorem Complexity.TM.DecidesInTime.paddedDirectUnrollingCircuitFamily_decides {k : ℕ} {tm : TM k} {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInTime L f) : (tm.paddedDirectUnrollingCircuitFamily f).Decides L

A deterministic decider's padded direct family decides the same language.

theorem Complexity.TM.paddedDirectUnrollingCircuitFamily_size_succ {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : (tm.paddedDirectUnrollingCircuitFamily f).size (n + 1) = tm.directUnrollingGateBound f (n + 1) + 1

At positive length, the padded family size is exactly its closed tableau bound plus one terminal copy.

theorem Complexity.TM.paddedDirectUnrollingCircuitFamily_size_bigO {k : ℕ} (tm : TM k) {f : ℕ → ℕ} {d : ℕ} (hf : BigO f fun (x : ℕ) => x ^ d) : BigO (tm.paddedDirectUnrollingCircuitFamily f).size fun (x : ℕ) => x ^ (3 * d)

A horizon in O(n^d) gives padded family size O(n^(3d)).

theorem Complexity.TM.paddedDirectUnrollingCircuitFamily_polynomialSize {k : ℕ} (tm : TM k) {f : ℕ → ℕ} {d : ℕ} (hf : BigO f fun (x : ℕ) => x ^ d) : (tm.paddedDirectUnrollingCircuitFamily f).PolynomialSize

Polynomially bounded horizons yield a polynomial-size padded family.