claimroutineinferred_dep

Matrix target reduces to kernel of K-sharp

Reduces the matrix target to ker⁡K#=⟨1⟩\ker K^\#=\langle\mathbf1\rangle
single kernel condition replacing the two-part target
Claim·§3.4 One parameter for both twists·inside lemOne squarefree n serving both twists

Statement (paper)

Assume K1B=0K\mathbf1_B=0 on the support QQ (for Q=Q0Q=Q_0 and Q=Q1Q=Q_1), and put K#=K+λatK^\#=K+\lambda a^{\mathsf t}. If ker⁡K#=⟨1⟩\ker K^\#=\langle\mathbf1\rangle, then ker⁡K=⟨1,1B⟩\ker K=\langle\mathbf1,\mathbf1_B\rangle and λ∉im⁡K\lambda\notin\operatorname{im}K; that is, the matrix target holds on QQ.

In plain English

Suppose K1B=0K\mathbf1_B=0 on the support QQ, and set K#=K+λatK^\#=K+\lambda a^{\mathsf t}. If ker⁡K#=⟨1⟩\ker K^\#=\langle\mathbf1\rangle, then ker⁡K=⟨1,1B⟩\ker K=\langle\mathbf1,\mathbf1_B\rangle and λ∉im⁡K\lambda\notin\operatorname{im}K, which is the matrix target on QQ.

Why it's here

This replaces the two-part matrix target by a single condition: the kernel of the modified matrix K#K^\# is just the all-ones line. That condition can then be checked by a nonsingularity argument on a deleted matrix, as the later claims do for both supports Q0Q_0 and Q1Q_1. The hypothesis K1B=0K\mathbf1_B=0 is what ties the kernel of KK to that of K#K^\#.
Classified routine:
Elementary linear algebra: a rank-one perturbation K + λaᵗ is compared with K using the hypothesis K1_B = 0, which gives the kernel and image conclusions by direct bookkeeping from the setup of the earlier claims.

Uses

claimAuxiliary primes give required congruences

Used by

claimNonsingular deleted matrix forces kernel lineclaimChoosing J bits makes enlarged matrix nonsingular

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Matrix target reduces to kernel of K-sharp" rests on claim-par-simultaneous-matrices-2