Documentation

Complexitylib.Circuits.Encoding.Machine.Core.Internal.Execution.Family

Total tagged-family core execution #

This file assembles the empty-family, positive-family, tag-mismatch, malformed count, and counted gate-loop branches. The output is the defaulted pure verdict: successful Boolean results are preserved and every malformed stream writes zero.

source
theorem Complexity.CircuitCode.Machine.Internal.familyCore_fromFrontiers_run_stream (codeBits inputBits : List Bool) (input code wires counter output : Tape) (hcode : BinaryCursor code codeBits codeBits.length) (hwires : BinaryCursor wires inputBits inputBits.length) (hcounter : counter.HasUnaryPrefix 0) (hcounter0 : counter.cells 0 = Γ.start) (hinput : input.read ≠ Γ.start) (houtputHead : output.head = 1) (houtputInv : output.StartInvariant) :
∃ (t : ℕ) (code' : Tape) (wires' : Tape) (counter' : Tape) (output' : Tape), t ≤ evalFamilyCoreTime codeBits.length inputBits.length ∧ evalFamilyCoreTM.reachesIn t (coreCfg CorePhase.rewindCode input code wires counter output) (coreCfg CorePhase.done input code' wires' counter' output') ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.ofBool ((familyStream? codeBits inputBits).getD false)

Every staged tagged-family stream has a matching halted machine run under the uniform quadratic core budget. Option.none is represented by the explicit zero verdict used for rejection.

source
theorem Complexity.CircuitCode.Machine.Internal.familyCore_fromFrontiers_run (codeBits inputBits : List Bool) (input code wires counter output : Tape) (hcode : BinaryCursor code codeBits codeBits.length) (hwires : BinaryCursor wires inputBits inputBits.length) (hcounter : counter.HasUnaryPrefix 0) (hcounter0 : counter.cells 0 = Γ.start) (hinput : input.read ≠ Γ.start) (houtputHead : output.head = 1) (houtputInv : output.StartInvariant) :
∃ (t : ℕ) (code' : Tape) (wires' : Tape) (counter' : Tape) (output' : Tape), t ≤ evalFamilyCoreTime codeBits.length inputBits.length ∧ evalFamilyCoreTM.reachesIn t (coreCfg CorePhase.rewindCode input code wires counter output) (coreCfg CorePhase.done input code' wires' counter' output') ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.ofBool ((evalFamilyCode codeBits inputBits).getD false)

Total core execution agrees with the public tagged-family evaluator after defaulting malformed encodings to the machine's zero verdict.