A Collision-Safe 21-Polynomial Gram Reduction for Defect-Three Collatz Kernels

A low-defect approach to hypothetical Collatz cycles leads, on the boundary branch h3 = s, to a cyclic operator with a seven-term Laurent kernel. After imposing η^−s = 2/3, two cyclic coincidences reduce this kernel to six atoms. Its Gram autocorrelation therefore contains 36 ordered-pair contributions. We prove that these contributions admit an exact grouping into 21 symbolic shift classes and, crucially, that the grouping remains valid when different symbolic classes collide in Z/sZ. Each class mass is then identified with an explicit low-degree polynomial in η, u1 = η^−h1 and u2 = η^−h2. The 21 polynomials are further identified with the 18-monomial integer coefficient table used by an existing compressed certificate checker: after multiplication by 9, their coefficients agree exactly with the stored Kronecker encodings. We also prove injectivity of that signed Kronecker packing for length-18 coefficient rows under the bounds used by the checker. The central algebraic statements are machine-checked in Lean 4.28.0 with Mathlib 4.28.0; the archived proof leaves contain no sorry, admit, or project-specific axioms. An independent exact Python replay gives 378/378 ordinary coefficient matches. This note is deliberately limited in scope. It does not prove the Collatz conjecture, and it does not complete the defect-three exclusion. The remaining step is to connect the per-class compressed transformed-diagonal certificates to the corresponding real cyclic Gram entries and then instantiate the final local determinant capstone.