claimroutineinferred_dep

Choosing J bits makes enlarged matrix nonsingular

Chooses JJ bits so the enlarged deleted matrix is nonsingular
extends nonsingularity to both supports
Claim·§3.4 One parameter for both twists·inside lemOne squarefree n serving both twists

Statement (paper)

After adding JJ, the deleted matrix on the enlarged support has B,IB,I block equal to M0M_0, and the bits [q0/qj][q_0/q_j] for j∈Jj\in J can be chosen so that this enlarged deleted matrix is nonsingular over F2\F_2. Indeed, varying [q0/qj][q_0/q_j] (together with its reverse) toggles exactly the jj-th JJ-diagonal entry, so the determinant is a multilinear polynomial in these bits with coefficient det⁡M0=1\det M_0=1 on the full product, and hence it does not vanish at every point of the Boolean cube. The chosen bits do not affect the smaller matrix, so the deleted matrices are nonsingular on both supports.

In plain English

On the enlarged support (with JJ added), the deleted matrix has B,IB,I block equal to M0M_0, and the bits [q0/qj][q_0/q_j] for j∈Jj\in J can be chosen so that it is nonsingular over F2\F_2. These choices do not affect the smaller matrix, so the deleted matrices are nonsingular on both supports.

Why it's here

This extends the base case (nonsingular M0M_0 on the smaller support) to the support containing JJ. Flipping the bit [q0/qj][q_0/q_j] toggles only the jj-th JJ-diagonal entry, so the determinant is multilinear in these bits with top coefficient det⁡M0=1\det M_0=1 and cannot vanish on the whole Boolean cube. With nonsingularity on both supports, the earlier reductions give the kernel condition and the matrix target, leaving only the prime-realization step to carry out these choices.
Classified routine:
A direct linear-algebra step over F_2: the determinant is multilinear in the J-diagonal bits with top coefficient det M_0 = 1 (from the previous claim), so it is not identically zero on the Boolean cube. This is a standard argument and not a new idea of the paper.

Uses

claimDeleted matrix on smaller support is nonsingularclaimNonsingular deleted matrix forces kernel lineclaimMatrix target reduces to kernel of K-sharp

Used by

claimRealize prescribed symbols by Dirichlet primes

Sources

PaperOpen
Section
§3.4 One parameter for both twists
Page
—
Label
—
Line
sections/03-parity.tex:674
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Toggling J diagonal makes enlarged matrix nonsingular" rests on claim-par-simultaneous-matrices-6
  • info
    inferred_dep
    outline: "Toggling J diagonal makes enlarged matrix nonsingular" rests on claim-par-simultaneous-matrices-4
  • info
    inferred_dep
    outline: "Toggling J diagonal makes enlarged matrix nonsingular" rests on claim-par-simultaneous-matrices-3