Direct-unrolling generator program

This module exposes the fixed work-vector layout and verified tagged/header prefix of the direct-unrolling generator. A later module supplies the positive tableau body and discharges its value-level entry condition.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble_sound {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (positivePreamble tm q).Sound

The positive polynomial-counter and tagged-header prefix is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble_space_bigO_log {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (positivePreamble tm q).SpaceBoundInLogAt TM.binaryLengthSpace (BinaryRoutine.inputLengthValues Work.inputLength)

The positive polynomial/header prefix uses logarithmic all-prefix space after the unary input length has been loaded in binary.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveMember_sound {k : ℕ} (tm : TM k) (q : Polynomial ℕ) {body : BinaryRoutine WorkCount} (hbody : body.Sound) : (positiveMember tm q body).Sound

A sound positive tableau body composes with the verified header prefix.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveMember_space_bigO_log {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (body : BinaryRoutine WorkCount) (hbody : body.SpaceBoundInLogAt TM.binaryLengthSpace fun (inputLength : ℕ) => preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength inputLength)) : (positiveMember tm q body).SpaceBoundInLogAt TM.binaryLengthSpace (BinaryRoutine.inputLengthValues Work.inputLength)

A logarithmic-space positive body remains logarithmic after the verified polynomial/header prefix.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.zeroMember_sound {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (zeroMember tm q).Sound

The hardwired zero-length family member is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.program_sound {k : ℕ} (tm : TM k) (q : Polynomial ℕ) {positiveBody : BinaryRoutine WorkCount} (hbody : positiveBody.Sound) : (program tm q positiveBody).Sound

A sound positive tableau body yields a sound complete zero/positive generator skeleton.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.program_space_bigO_log {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (positiveBody : BinaryRoutine WorkCount) (hbody : positiveBody.SpaceBoundInLogAt TM.binaryLengthSpace fun (inputLength : ℕ) => preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength inputLength)) : (program tm q positiveBody).SpaceBoundInLogAt TM.binaryLengthSpace (BinaryRoutine.inputLengthValues Work.inputLength)

A logarithmic-space positive body yields a logarithmic-space complete zero/positive generator skeleton.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble_requires_inputLengthValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (length : ℕ) : (positivePreamble tm q).requires (BinaryRoutine.inputLengthValues Work.inputLength length)

The positive prefix's arithmetic/scratch obligations hold from the canonical input-length work vector.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.program_requires_inputLengthValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (positiveBody : BinaryRoutine WorkCount) (hbody : ∀ (length : ℕ), 0 < length → positiveBody.requires (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength length))) (length : ℕ) : (program tm q positiveBody).requires (BinaryRoutine.inputLengthValues Work.inputLength length)

A positive body's entry obligation for every nonzero length is exactly what the complete zero/positive generator needs at fresh-input entry.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble_effect {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (values : BinaryValues WorkCount) : (positivePreamble tm q).effect values = preambleValues tm q values

Exact pure work-vector endpoint of the positive prefix.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble_emitted {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (values : BinaryValues WorkCount) : (positivePreamble tm q).emitted values = true :: CircuitCode.NatCode.encode (Polynomial.eval (values Work.inputLength) (tm.directSerializerGateCountPolynomial q))

Exact tag and gate-count header emitted by the positive prefix.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.zeroMember_emitted {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (values : BinaryValues WorkCount) : (zeroMember tm q).emitted values = [false, boundedAcceptanceBit tm.toNTM (Polynomial.eval 0 (TM.directSerializerHorizonPolynomial q)) (fun (index : Fin 0) => index.elim0) fun (x : Fin (Polynomial.eval 0 (TM.directSerializerHorizonPolynomial q))) => false]

Exact tagged code emitted on length zero.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.program_emitted {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (positiveBody : BinaryRoutine WorkCount) (values : BinaryValues WorkCount) : (program tm q positiveBody).emitted values = if values Work.inputLength = 0 then [false, boundedAcceptanceBit tm.toNTM (Polynomial.eval 0 (TM.directSerializerHorizonPolynomial q)) (fun (index : Fin 0) => index.elim0) fun (x : Fin (Polynomial.eval 0 (TM.directSerializerHorizonPolynomial q))) => false] else true :: (CircuitCode.NatCode.encode (Polynomial.eval (values Work.inputLength) (tm.directSerializerGateCountPolynomial q)) ++ positiveBody.emitted (preambleValues tm q values))

Exact zero/positive word emitted by the generator skeleton.