claimroutineinferred_dep

Fixed symbol sums for B and J

Records fixed symbol sums over BB and JJ
constrains the auxiliary prime choices
Claim·§3.4 One parameter for both twists·inside lemOne squarefree n serving both twists

Statement (paper)

For the fixed sets BB and JJ, one has ∑i∈Bsi=∑j∈Jsj=0\sum_{i\in B}s_i=\sum_{j\in J}s_j=0, ∑i∈Bλi=1\sum_{i\in B}\lambda_i=1 and ∑j∈Jλj=0\sum_{j\in J}\lambda_j=0. Moreover, the cross symbols satisfy ∑j∈J[qj/qi]=0\sum_{j\in J}[q_j/q_i]=0 for every i∈Bi\in B and ∑i∈B[qi/qj]=0\sum_{i\in B}[q_i/q_j]=0 for every j∈Jj\in J.

In plain English

For the fixed prime sets BB and JJ, the sums of sis_i over BB and over JJ both vanish, ∑i∈Bλi=1\sum_{i\in B}\lambda_i=1, and ∑j∈Jλj=0\sum_{j\in J}\lambda_j=0. Also, ∑j∈J[qj/qi]=0\sum_{j\in J}[q_j/q_i]=0 for each i∈Bi\in B and ∑i∈B[qi/qj]=0\sum_{i\in B}[q_i/q_j]=0 for each j∈Jj\in J.

Why it's here

This claim records the fixed-prime part of the symbol data, which the construction of the auxiliary primes must be compatible with. It follows from the local square conditions in the cross-squares lemma: θ\theta is a square at primes of BB, β\beta is a square at primes of JJ, and β\beta is a nonsquare unit at 3. The later claims use these sums to choose the auxiliary prime types and symbols so that the matrix target holds.
Classified routine:
Direct bookkeeping consequence of the cross-square lemma (par-cross-squares): evaluating the local square conditions at primes of B, J and at 3 gives the stated symbol sums via standard Legendre/Hilbert symbol computations.

Uses

lemCross-square conditions on B, J, β, θ

Used by

claimAuxiliary primes give required congruencesclaimSymbol prescription gives K·1_B = 0

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Fixed symbol sums for B and J" rests on par:cross-squares