Successful streaming endpoints

This proof-only module exposes the exact final transducer state reached on a typed CNF token stream. The endpoint is recovered from the public transformFrom?_tokens_internal result, so the token-level execution proof in Internal.Streaming remains the single source of truth.

theorem Complexity.SAT.ThreeSAT.Streaming.run_tokens_endpoint_internal (phi : CNF) (next : ℕ) : run (initial next) phi.tokens = some { next := (CNF.to3Aux next phi).2, pending := Pending.zero, scan := Scan.boundary, emitted := (CNF.to3Aux next phi).1.tokens }

Running a typed CNF token stream reaches the exact state described by CNF.to3Aux, before the final finish projection is applied.

theorem Complexity.SAT.ThreeSAT.Streaming.run_tokens_bitLengthStart_internal (phi : CNF) : run (initial (phi.encode.length + 1)) phi.tokens = some { next := (CNF.to3Aux (phi.encode.length + 1) phi).2, pending := Pending.zero, scan := Scan.boundary, emitted := (CNF.to3Aux (phi.encode.length + 1) phi).1.tokens }

Exact successful endpoint when the fresh-variable counter starts one past the concrete source bit length.