claimroutineinferred_dep

Deleted matrix on smaller support is nonsingular

Shows deleted matrix M0M_0 on the smaller support is nonsingular
base case before adding J
Claim·§3.4 One parameter for both twists·inside lemOne squarefree n serving both twists

Statement (paper)

On Q0Q_0, the deleted matrix has the block form M0=(ACCt0)M_0=\begin{pmatrix}A&C\\ C^{\mathsf t}&0\end{pmatrix} with 1BtA1B=1\mathbf1_B^{\mathsf t}A\mathbf1_B=1, and M0M_0 is nonsingular over F2\F_2. This holds also when ∣B∣|B| is even, and when ∣B∣=1|B|=1 one has simply M0=(1)M_0=(1).

In plain English

On the support Q0Q_0, the deleted matrix M0M_0 has block form (ACCt0)\begin{pmatrix}A&C\\ C^{\mathsf t}&0\end{pmatrix} with 1BtA1B=1\mathbf1_B^{\mathsf t}A\mathbf1_B=1, and it is nonsingular over F2\F_2. This also holds when ∣B∣|B| is even, and for ∣B∣=1|B|=1 it is simply M0=(1)M_0=(1).

Why it's here

This is the base case for the matrix target: it gives a nonsingular deleted matrix on the support before JJ is added. The kernel property K1B=0K\mathbf1_B=0 from the previous claim fixes the form of the BB block and gives 1BtA1B=1\mathbf1_B^{\mathsf t}A\mathbf1_B=1, which together with the zero lower-right block gives nonsingularity. The next claim then extends M0M_0 to the enlarged support by choosing the bits for JJ.
Classified routine:
A direct linear-algebra check over F_2 on the block form fixed by the previous claim (K·1_B = 0): the condition 1_B^t A 1_B = 1 together with the zero lower-right block gives nonsingularity. This is bookkeeping inside the paper's own construction, not a new idea.

Uses

claimSymbol prescription gives K·1_B = 0

Used by

claimChoosing J bits makes enlarged matrix nonsingular

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Block matrix M_0 nonsingular on smaller support" rests on claim-par-simultaneous-matrices-5