lemmaroutine

Structure of the line blocks U_A

Blocks UAU_A have dimension bb, trace annihilator AA, and span X⊕BX\oplus B
basic block facts for the kernel computation
Lemma·lem:latent-block·§3.1 The quadratic block

Statement (paper)

For every line AA, the space UAU_A is binary linear of dimension bb. For a∈Aa\in A and x∈Xx\in X, one has D(x,a)∈DAD(x,a)\in D_A; for a,a′∈Aa,a'\in A, one has D(a,a′)=0D(a,a')=0. The trace annihilator of DAD_A in B∗=F3B^*=F^3 is AA, and the spaces UAU_A together span X⊕BX\oplus B.

In plain English

For every line AA, the space UAU_A is a binary linear space of dimension bb. D(x,a)D(x,a) lies in DAD_A for a∈Aa\in A and x∈Xx\in X, and D(a,a′)=0D(a,a')=0 for a,a′∈Aa,a'\in A. The trace annihilator of DAD_A in B∗=F3B^*=F^3 is AA, and the spaces UAU_A together span X⊕BX\oplus B.

Why it's here

This lemma collects the basic properties of the blocks UAU_A that later arguments rely on: each block has the right dimension, the form DD behaves as claimed on and inside the line, and the blocks cover the whole space X⊕BX\oplus B. Results such as the kernel of a block restriction (Lemma 3.4) use these facts to analyse the restriction map to each UAU_A.}
Classified routine:
These are basic structural facts about the paper's own construction of the line blocks UAU_A. They are checked directly from the definitions of the quadratic form DD and the lines over F3F^3, using linear-algebra bookkeeping and trace duality.

Uses

Nothing else in the paper

Used by

lemKernel of block restriction map

Sources

PaperOpen
Section
§3.1 The quadratic block
Page
—
Label
lem:latent-block
Line
sections/02-latent.tex:101
Leannot aligned

Phase 2 aligns this node to a Lean declaration.