Documentation

Complexitylib.Circuits.Encoding.Machine.Core.Internal.Execution.Gate.Loop

Successful gate-stream execution #

This file lifts the pure one-gate bridge to every successful counted gate stream. The loop invariant tracks the code suffix, exact memo frontier, consumed unary counter, last-value/output correspondence, and a fixed maximum memo length. The resulting budget is quadratic once the maximum memo length is bounded by input length plus gate count.

source
def Complexity.CircuitCode.Machine.Internal.gateLoopBudget (remaining maxWireLength : ℕ) :
ℕ

Uniform budget for a successful suffix of the gate loop.

Equations
Instances For
    source
    def Complexity.CircuitCode.Machine.Internal.positiveGateRunBudget (gateCount inputLength : ℕ) :
    ℕ

    Budget from a positive-family tag through unary-count setup and a successful gate loop.

    Equations
    Instances For
      source
      def Complexity.CircuitCode.Machine.Internal.positiveCoreRunBudget (gateCount codeLength inputLength : ℕ) :
      ℕ

      Budget from the staging append frontiers through a successful positive family evaluation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.CircuitCode.Machine.Internal.positiveCoreRunBudget_le_quadratic {gateCount codeLength inputLength : ℕ} (hcount : gateCount ≤ codeLength) :
        positiveCoreRunBudget gateCount codeLength inputLength ≤ 20 * (codeLength + inputLength + 1) ^ 2

        The successful positive-core budget is quadratically bounded by the serialized code and input lengths once the unary gate count fits in the code.

        source
        theorem Complexity.CircuitCode.Machine.Internal.gateLoop_run_some (remaining maxWireLength : ℕ) (sawGate : Bool) (last : Option Bool) (answer : Bool) {codeBits wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hstream : gateStream? remaining codeBits wireBits last = some answer) (hsaw : sawGate = last.isSome) (hposition : position = if sawGate = true then wireBits.length else 0) (hcode : code.HasBinarySuffix codeBits) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder used total) (hcount : used + remaining = total) (hmax : wireBits.length + remaining ≤ maxWireLength) (hinput : input.read ≠ Γ.start) (houtputHead : output.head = 1) (houtputInv : output.StartInvariant) (hlast : ∀ (value : Bool), last = some value → output.cells 1 = Γ.ofBool value) :
        ∃ (t : ℕ) (code' : Tape) (wires' : Tape) (counter' : Tape) (output' : Tape) (finalWireBits : List Bool), t ≤ gateLoopBudget remaining maxWireLength ∧ evalFamilyCoreTM.reachesIn t (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg CorePhase.done input code' wires' counter' output') ∧ code'.HasBinarySuffix [] ∧ BinaryCursor wires' finalWireBits finalWireBits.length ∧ counter'.HasCounterRemainder total total ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.ofBool answer

        Every successful pure counted gate stream has a matching machine run to the halted controller. The final code is exhausted, the counter is fully consumed, the wire memo remains at its append frontier, and output cell one contains the pure answer.

        source
        theorem Complexity.CircuitCode.Machine.Internal.positiveFamily_run_some (gateCount : ℕ) (gateCode inputRest : List Bool) (input code wires counter output : Tape) (inputBit answer : Bool) (hstream : gateStream? gateCount gateCode (inputBit :: inputRest) none = some answer) (hcode : BinaryCursor code (true :: (NatCode.encode gateCount ++ gateCode)) 0) (hwires : BinaryCursor wires (inputBit :: inputRest) 0) (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) (finalWireBits : List Bool), t ≤ positiveGateRunBudget gateCount (inputBit :: inputRest).length ∧ evalFamilyCoreTM.reachesIn t (coreCfg CorePhase.familyTag input code wires counter output) (coreCfg CorePhase.done input code' wires' counter' output') ∧ code'.HasBinarySuffix [] ∧ BinaryCursor wires' finalWireBits finalWireBits.length ∧ counter'.HasCounterRemainder gateCount gateCount ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.ofBool answer

        A positive-family tag whose counted pure stream succeeds runs through counter construction, every gate, and the exhausted-counter check within the named quadratic budget.

        source
        theorem Complexity.CircuitCode.Machine.Internal.positiveFamily_fromFrontiers_run_some (gateCount : ℕ) (gateCode inputRest : List Bool) (input code wires counter output : Tape) (inputBit answer : Bool) (hstream : gateStream? gateCount gateCode (inputBit :: inputRest) none = some answer) (hcode : BinaryCursor code (true :: (NatCode.encode gateCount ++ gateCode)) (true :: (NatCode.encode gateCount ++ gateCode)).length) (hwires : BinaryCursor wires (inputBit :: inputRest) (inputBit :: inputRest).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) (finalWireBits : List Bool), t ≤ positiveCoreRunBudget gateCount (true :: (NatCode.encode gateCount ++ gateCode)).length (inputBit :: inputRest).length ∧ evalFamilyCoreTM.reachesIn t (coreCfg CorePhase.rewindCode input code wires counter output) (coreCfg CorePhase.done input code' wires' counter' output') ∧ code'.HasBinarySuffix [] ∧ BinaryCursor wires' finalWireBits finalWireBits.length ∧ counter'.HasCounterRemainder gateCount gateCount ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.ofBool answer

        From the staging append frontiers, a successful positive-family stream reaches its exact verdict within the full quadratic core budget.