Proof-carrying binary stream routines -- proof internals

The common proof layer converts canonical value vectors into literal tape frames, lifts frame-oriented arithmetic contracts through an arbitrary output accumulator, and composes routines across the parked seqTM phase boundary.

theorem Complexity.BinaryRoutine.natTape_hasBinaryNat_internal (value : ℕ) : (natTape value).HasBinaryNat value

theorem Complexity.BinaryRoutine.natTape_parked_internal (value : ℕ) : TM.Parked (natTape value)

theorem Complexity.BinaryRoutine.workTapes_parked_internal {n : ℕ} (values : BinaryValues n) (i : Fin n) : TM.Parked (workTapes values i)

theorem Complexity.BinaryRoutine.workTapes_hasBinaryNat_internal {n : ℕ} (values : BinaryValues n) (i : Fin n) : (workTapes values i).HasBinaryNat (values i)

theorem Complexity.BinaryRoutine.workTapes_update_internal {n : ℕ} (values : BinaryValues n) (idx : Fin n) (value : ℕ) : workTapes (Function.update values idx value) = Function.update (workTapes values) idx (natTape value)

theorem Complexity.BinaryRoutine.Sound.seq_internal {n : ℕ} {first second : BinaryRoutine n} (hfirst : first.Sound) (hsecond : second.Sound) : (first.seq second).Sound

theorem Complexity.BinaryRoutine.Sound.restrict_internal {n : ℕ} {routine : BinaryRoutine n} (hsound : routine.Sound) (requires : BinaryValues n → Prop) (hrequires : ∀ (values : BinaryValues n), requires values → routine.requires values) : (routine.restrict requires).Sound

theorem Complexity.BinaryRoutine.emitBits_sound_internal {n : ℕ} (word : List Bool) : (emitBits word).Sound

theorem Complexity.BinaryRoutine.identity_sound_internal {n : ℕ} : identity.Sound

theorem Complexity.BinaryRoutine.binarySucc_sound_internal {n : ℕ} (idx : Fin n) : (binarySucc idx).Sound

theorem Complexity.BinaryRoutine.binaryPred_sound_internal {n : ℕ} (idx : Fin n) : (binaryPred idx).Sound

theorem Complexity.BinaryRoutine.binaryCopy_sound_internal {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : (binaryCopy srcIdx dstIdx counterIdx).Sound

theorem Complexity.BinaryRoutine.emitRawGateStep_sound_internal {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) : (emitRawGateStep op negated₀ negated₁ emitCounterIdx availableIdx input₀Idx input₁Idx).Sound