Direct-unrolling generator program -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble_spaceBoundByWidth_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : ∃ (p : Polynomial ℕ), (positivePreamble tm q).SpaceBoundByWidthAt TM.binaryLengthSpace (BinaryRoutine.inputLengthValues Work.inputLength) fun (x : ℕ) => Polynomial.eval x p

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

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

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

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

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

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

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveMember_space_bigO_log_internal {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)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.program_space_bigO_log_internal {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)

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.program_requires_inputLengthValues_internal {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)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble_emitted_internal {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))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.zeroMember_emitted_internal {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]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.program_emitted_internal {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))