claimroutineinferred_dep

Nonzero binary residuals are nonalternating

Nonzero binary edge residuals are nondegenerate and nonalternating
checks the hypothesis for orthonormal bases
Claim·§3.3 Subspaces attached to the gates·inside lemEdge residuals and rank budget

Statement (paper)

Over F2\mathbb F_2, every nonzero orthogonal residual of an edge is a nondegenerate symmetric bilinear space that is nonalternating, i.e. it contains a vector of norm one.

In plain English

Over F2\mathbb F_2, every nonzero orthogonal residual of an edge is a nondegenerate symmetric bilinear space that contains a vector of norm one, so it is not alternating.

Why it's here

This is the hypothesis check for the last step of the parent lemma. Using the residual table from the previous claim, it shows each nonzero residual is nondegenerate and nonalternating, so the next claim gives an orthonormal basis for the binary label space.
Classified routine:
A direct check against the residual table from the previous claim. Over F_2, a nondegenerate symmetric form is alternating only when every vector has norm zero, so the check reduces to exhibiting one vector of norm one in each residual, using standard facts about symmetric bilinear forms in characteristic 2.

Uses

claimEdge residual table; only center 3→4 decreases

Used by

claimNonalternating binary spaces have orthonormal bases

Sources

PaperOpen
Section
§3.3 Subspaces attached to the gates
Page
—
Label
—
Line
sections/03-motifs.tex:427
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Nonzero binary residuals are nonalternating" rests on claim-lem-motif-residuals-1