Kernel-checked packet ceilings for all active and aligned scalar rows

Let $k$ select one of the 64 registered rows in GoldbachActiveRoundedData: all 63 active packet rows and the aligned scalar row from the v4 release at https://goldbach-nine.vercel.app/ . Write its integer cap sequences as $a_i,b_i$, budgets as $U,V$, base-energy numerator as $B$, and $D=10^{12}$.

For any real number $q$ and real sequences $r_i,t_i$ satisfying

and every bounded partial-mass constraint

the quadratic series converges and

The proof retains the supplied base-energy upper bound as an explicit premise. It proves the known countable aligned cap-and-mass inequality, reduces its greedy extremum to a finite prefix, and checks every cap ordering, budget cover, and integer energy comparison using decide +kernel. It imports only the data definition and Mathlib, with no open theorem or solution imports.

The registered data conservatively enlarges all corresponding frozen witness constraints, as checked separately by exact Python arithmetic. This is a closed optimization theorem conditional on those constraints. It does not establish that analytic zero sums satisfy them, the paper's exceptional-set estimate, or strong Goldbach. The optimization principle is attributed to Theorem 17 of https://lorenzoschiavone.com/writing/goldbach-exceptional-set-bound/ . No mathematical novelty is claimed.