Rejecting decoded positive-family execution

This file lifts the rejecting counted gate loop through a successfully decoded positive-family header. It shares the successful branch's named budgets while retaining a well-formed counter remainder and an explicit zero verdict.

theorem Complexity.CircuitCode.Machine.Internal.positiveFamily_run_none (gateCount : ℕ) (gateCode inputRest : List Bool) (input code wires counter output : Tape) (inputBit : Bool) (hstream : gateStream? gateCount gateCode (inputBit :: inputRest) none = none) (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) (finalUsed : ℕ), 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') ∧ counter'.HasCounterRemainder finalUsed gateCount ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.zero

A positive-family tag whose decoded counted gate stream rejects runs through counter construction and the failing gate loop within the named quadratic budget.

theorem Complexity.CircuitCode.Machine.Internal.positiveFamily_fromFrontiers_run_none (gateCount : ℕ) (gateCode inputRest : List Bool) (input code wires counter output : Tape) (inputBit : Bool) (hstream : gateStream? gateCount gateCode (inputBit :: inputRest) none = none) (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) (finalUsed : ℕ), 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') ∧ counter'.HasCounterRemainder finalUsed gateCount ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.zero

From the staging append frontiers, a rejecting decoded positive-family stream reaches a zero verdict within the full quadratic core budget.