claimroutineinferred_dep

Nonsingular deleted matrix forces kernel line

Nonsingular deleted matrix forces ker⁡K#=⟨1⟩\ker K^\#=\langle\mathbf1\rangle
reduces the kernel condition to nonsingularity
Claim·§3.4 One parameter for both twists·inside lemOne squarefree n serving both twists

Statement (paper)

For either support, let MM be the matrix obtained from K#K^\# by deleting the q0q_0 row and column. If MM is nonsingular, then ker⁡K#=⟨1⟩\ker K^\#=\langle\mathbf1\rangle.

In plain English

Let MM be the matrix obtained from K#K^\# by deleting the q0q_0 row and column, for either support. If MM is nonsingular, then ker⁡K#=⟨1⟩\ker K^\#=\langle\mathbf1\rangle.

Why it's here

This reduces the kernel condition from the previous claim to checking that one smaller matrix is nonsingular. The later claims, including the one that toggles the JJ diagonal entries, then only need to verify nonsingularity of MM on each support.
Classified routine:
Elementary linear algebra: since K#1=0K^\#\mathbf1=0, the rank of K#K^\# is at least that of the nonsingular principal minor MM, so the kernel is one-dimensional and spanned by 1\mathbf1. This is a direct bookkeeping consequence of the preceding claim.

Uses

claimMatrix target reduces to kernel of K-sharp

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:618
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Suffices that deleted matrix is nonsingular" rests on claim-par-simultaneous-matrices-3