Coffee-Bean Maximality for Width-Normalized Label Systems: A Shift-Lipschitz Induction on Room Multisets

We study width-normalized label systems with positive nondecreasing widths and a single root. If the cumulative count at a terminal depth is at most that of the coffee-bean system (1,k,k,...), cumulative dominance holds at every earlier depth. This yields the breadth-first cost comparison, rigidity, and strictness at intermediate depths for nonidentical systems. Two induction proofs and the correspondence with label sets are formalized in the companion Lean 4 development. Version 0.7 makes the incoming-room depth convention explicit and records the exact root-inclusive translation to the Lean indices. It also retains an exact counterexample to the broader fixed-prefix comparison, which is distinct from the single-root theorem. The counterexample and numerical illustrations are supplied with reproducible exact-integer scripts; their verification is distinguished from the Lean formalization. Included files: manuscript PDF, TeX/BibTeX source archive, and verification archive. The formalization cited by the paper is commit f9cdca894844b19560b4f4558c9687685cb4e688 of https://github.com/ycmath/cbs-lean. The prepared software snapshot bb21bd1b715e96e6e80508152df7022f8743fb11 preserves those Lean sources and repairs CI/documentation handling. No hardware-performance claims are made in this manuscript.