Strong bounds and literal first ear
Abstract
One shadow-charge path, two prefix strips
For actual old values f and charge q=2f-g, the internal Strong predicate controls every recursive physical prefix by 0<=h<=B-1 and 0<=h+Q<=B. The enlarged height after the literal initial ear is 2h+Q=h+r, so strong_strips supplies both strips on the same word. The positive remaining charge at a proper prefix supplies the strict old ceiling. Under a natural lift by scale M, the pointwise height is M*h+(M-1)Q, the remaining charge is Q, and the shadow height is Mr. lift_bounds proves preservation when the final-negative charge is still present, or at the exact zero endpoint. The whole-word strong_scaled transports Strong under exact source compatibility and nonnegative consumed charge, including a zero-charge endpoint. strong_positive_block controls the prepended low-label block, and strong_append joins it to the inherited word. The complete base chamber endpoint proof remains a separate obligation.