Strategies

1. Create scratch/coupled_syndromes.py implementing an exact parity-check matrix H for the promoted encoder, including the correct dual weights. For an error support E, test the condition that every column of S1 + gamma*S2 lies in the span of H_E; this is the concrete replacement for rational interpolation. 2. Restrict the construction to two interleaved channels and adjacent exponent residue blocks modulo the fibre size. Search pencils whose second channel is a cyclic shift of the first plus a rank-one boundary correction. Start with small power-of-two domains and compute locator recurrences and their exact elimination matrices, rather than searching arbitrary words. 3. Seek a family-wide identity making the fifteenth locator condition a consequence of the other fourteen and the existing cyclic product key. Simultaneously check that the shift coupling is not removable by an invertible channel transformation, that winning challenges are not restricted to the base field, and that no omitted equation reappears as a polynomial-degree or endpoint condition. Save either the explicit identity or the exact obstruction in scratch/coupled_syndromes.md. 4. Add ProximityPrize/SubmissionUpper/SyndromePencil.lean with reusable lemmas equating support-constrained errors to parity-check span membership, including the interleaved version. Formalize the successful boundary identity before constructing the full words; these lemmas remain useful if the initial coupling fails. 5. Lift a successful identity to the 512-fibre parameters. Establish the common agreement support, valid degree bounds for both channels, a violating dot-product instance, and the exact challenge-cardinality inequality. Only then combine with the promoted suffix certificate, obtain a strictly smaller score using score_for_claim, and run the benchmark gate.

1. Create scratch/pade_slack.py to work symbolically with V_U(Y)=Y^273+u1*Y^272+... and auxiliary factors H_U(Y) of degree one or two. Derive the complete coefficient equations for a numerator H_U*V_U to represent a fixed affine pencil modulo a codeword of the allowed degree. Include monicity, denominator clearing if used, and the functional equation determining gamma. 2. Eliminate the auxiliary-factor coefficients explicitly. Record the resulting Padé minors or recurrence invariants as the actual key; count every remaining base-field coordinate and every discrete endpoint key. Generic dimension counting gives no gain, so reject any design that merely trades auxiliary variables for equally many new constraints. 3. Test structural rank defects specific to the 512-label root-of-unity domain, using Newton identities and the identity V_U*V_complement=Y^512-1. Require an algebraic identity valid for the entire restricted family, rather than numerical rank evidence or an assumed unusually large fibre. 4. Before writing a full attack, certify an exact family-count/key-count inequality giving more than |F|/2^128 distinct challenges at agreement at least 273*512 plus the justified core. Also establish how many auxiliary-factor solutions can produce the same codeword or challenge. 5. Save a reusable Lean lemma in scratch/PadeLocator.lean: if the derived coefficient equations and divisibility conditions hold, the resulting polynomial has degree below 131072 and agrees with the affine word on every selected column. This is a useful first-stage deliverable even if the entropy test fails. 6. Cap symbolic exploration at one-third of the session. Proceed to a gate-ready submission only after the rank identity, exact count, and challenge-separation argument all pass; reuse the promoted suffix certificate and scoring proof rather than rebuilding them.

1. In scratch/equivariant_1024.py, check the exact inequality C(255,136) > p^6 * 256 * ceil(2^59/16), using integer arithmetic. Treat this only as a prospective entropy budget, not a certificate. 2. Construct the core as one 1024-point domain coset minus one 16-point subcoset. Its vanishing polynomial R is invariant under multiplication by the order-16 subgroup; verify deg(R)=1008 and deg(R*Q(X^1024)) <= 131056 whenever deg(Q)<=127. 3. In scratch/EquivariantPencil.lean, first prove a general equivariance lemma: a domain permutation preserving the encoder, the fixed pair of words, and the claimed functional induces an explicit Möbius action on winning challenges. The lemma must preserve violation as well as agreement. 4. Start with character eigenvectors under x -> zeta*x and invariant denominators. Do not assume that symmetry of the core alone changes gamma. 5. Prove a disjoint-orbit or transversal bound for the generated challenges; multiplying a fibre size by 16 without controlling overlaps is forbidden. If the invariant word space or orbit bound fails, stop and leave the general equivariance lemma and search script reusable. 6. If both checks succeed, instantiate the promoted OrbitPencil counting route with 136 labels and six prescribed top coefficients.

1. Implement scratch/dihedral_pencil.py for d in {64, 128, 256, 512}. Represent a regular quotient fibre by X^(2d) - s*X^d + 1, with s = z + z^-1, and record the two exceptional fibres z = ±1 separately. 2. Construct subset products of these fibre factors. Derive their reciprocal coefficient identities, the actual polynomial degree after clearing negative powers, and admissible common-core factors. Explicitly charge every clearing factor against the degree bound 131071. 3. Test rational-pencil denominators at the branch values and at an extension-field parameter. Derive the complete collision key, including any required endpoint evaluations; reject any profile that silently treats these evaluations as subgroup-sized keys. 4. Produce exact family and bad-set bounds. Continue to Lean only if the resulting agreement is greater than 139775 and the distinct-challenge count satisfies 2^128 * K > p^6. Otherwise leave the symbolic degree ledger and exclusion results as reusable artifacts. 5. Formalize a surviving construction in DihedralPencil.lean, prove agreement including the exceptional fibres, and join it to the promoted suffix proof before checking the exact score.

1. Read the promoted OrbitPencil.lean and extract its exact degree, divisibility, projection and exceptional-alpha requirements; do not start from the rejected 273-column submission. Write scratch/mixed_blocks.py using Y = X^256, where a paired block has factor Y^2 - z^2 and a single block has factor Y - z. 2. Enumerate bounded profiles of paired blocks, singleton blocks and fixed core roots. Symbolically determine which high coefficients are independent, which low coefficients are automatically zero, and the degree remaining after the rational-pencil division. Count each family exactly, accounting for excluded and overlapping columns. 3. Search only profiles whose guaranteed agreement exceeds 139775 and whose rigorously bounded key count leaves K with 2^128 * K > p^6. Do not count a coefficient as free merely because it is determined after conditioning on another uncounted parameter. 4. Save the profile tables and degree identities even if the search fails. For a surviving profile, implement MixedBlocks.lean with factorization, coefficient-profile, fibre-cardinality and agreement lemmas. 5. Reuse the promoted prescribed-top suffix certificate, prove the new lower-radius segment separately, and run score_for_claim and the complete upper benchmark.