Original labels and exact unbounded domain
Abstract
Native masses and a literal conditional ear
The bank schedule uses the original terminal order U,V,W,X. If Rp<0, insert the sole fresh label k immediately before the V terminal, after banks U and V; otherwise insert it immediately before the X terminal, after all four positive banks. The exact natural cut is the length of the corresponding original prefix, and is strictly less than k.
The proof supplies both a PacketNormalForm data certificate and legality of the specific increasing-decoder word. Native chain identities determine old and new bank masses and terminal values. The endpoint windows imply every individual prefix bound using positivity within banks and negativity of each terminal. The original finite-set engine is reused without replacing the literal word by a Finset enumeration.
The identity blocksWord(withEar(…))=insertAt(k,word,freshCut) retains the original labels and the early or late insertion exactly. SourceCertificate consumes Banks and Arithmetic and is consumed by Allocation. Its numerical window hypotheses are internal obligations discharged there.