Serialized circuit-evaluator machine

This module exposes the audited front end for a deterministic evaluator of serialized circuit families. It validates the outer self-delimiting pair, stages its code and input components on separate appendable work tapes, and exposes the verified quadratic-time memoized evaluator from raw input through its final verdict.

Main results

• pair_mem_circuitEvalLanguage_iff identifies the target language on canonical paired inputs.
• pairStageTM_hoareTime gives the total staged-input contract in linear time.
• Machine.evalFamilyCoreTM_hoareTime gives the total staged-core contract in concrete quadratic time.
• Machine.evalFamilyTM_decidesInTime proves the complete evaluator decides circuitEvalLanguage, and Machine.evalFamilyTime_bigO_quadratic gives its polynomial bound.
• Machine.emitNatCodeTM_hoareTimeSpace emits terminated-unary natural codes from binary work tapes with reusable scratch and an all-prefix space bound.
• Machine.emitRawGateTM_hoareTimeSpace emits complete raw-gate codes from two preserved binary wire references.
• Machine.emitRawGateStepTM_hoareTimeSpace additionally advances the first-unused-wire counter after one emitted gate.

@[simp]

theorem Complexity.CircuitCode.mem_circuitEvalLanguage_iff (z : List Bool) : z ∈ circuitEvalLanguage ↔ evalFamilyPair? z = some true

Membership in the evaluator language is successful Boolean evaluation.

theorem Complexity.CircuitCode.pair_mem_circuitEvalLanguage_iff (code input : List Bool) : pair code input ∈ circuitEvalLanguage ↔ evalFamilyCode code input = some true

A canonical outer pair belongs to the evaluator language exactly when its tagged circuit code evaluates to true on the paired input.

theorem Complexity.CircuitCode.encodeAt_pair_mem_circuitEvalLanguage_iff (F : CircuitFamily Basis.andOr2) (input : List Bool) : pair (F.encodeAt input.length) input ∈ circuitEvalLanguage ↔ F.evalList input = true

Pairing a family's canonical member code with an input recognizes exactly the language decided by that family.

theorem Complexity.CircuitCode.Machine.PairStagePost.outputReady {bits : List Bool} {inp : Tape} {work : Fin workTapeCount → Tape} {out : Tape} (h : PairStagePost bits inp work out) : out.StartInvariant ∧ out.head = 1

Every staged endpoint leaves the output at cell one with the canonical left-marker invariant, ready for the evaluator core to overwrite its verdict.

theorem Complexity.CircuitCode.Machine.pairStageTM_hoareTime (bits : List Bool) : pairStageTM.HoareTime (PairStagePre bits) (PairStagePost bits) (pairStageTime bits.length)

The pair-staging machine validates every outer input and, in linear time, either rejects it without dirtying work tapes or exposes appendable code and input prefixes for the evaluator core.