skew_char_p

The skew quadratic form over a field of characteristic $\ne 2$ — TARGET 21 (filler)

Seal

Rung rung-1 · Status sealed · #print axioms verbatim in The machine seal — fully closed, no interface hypotheses. Library-completeness lift of the L3 lemma in passivity_identity.
Links: module index · interface ledger · related passivity_identity · pin pin_skew_charp.py

Sealed theorems

dotProduct_mulVec_self_of_skew_of_charP

Over any field with $\mathrm{ringChar}F\ne 2$, a skew-symmetric quadratic form vanishes — the exact algebraic frontier of the passivity identity.

Statement

Theorem. Let $F$ be a field with $\mathrm{ringChar}F\ne 2$, let $n$ be a finite index set, and let $A$ be an $n\times n$ matrix over $F$ with $A^{\top }=-A$. Then ${\mathbf{x}}^{\top }\mathbf{Ax}=0$ for every $\mathbf{x}\in F^n$.

Machine name: Leanpunov.dotProduct_mulVec_self_of_skew_of_charP in SkewCharP.lean.

What it is and why it exists

This is the characteristic-$\ne 2$ lift of the sealed L3 lemma Leanpunov.dotProduct_mulVec_self_of_skew (in Passivity.lean, stated over $\mathbb{R}$). The passivity derivation’s closing note flagged it: “Lemma 1 holds over any ring; only Lemma 2 uses division by two. A char-$\ne 2$ generalization is a one-line change if ever needed — not done, because the thesis lives over $\mathbb{R}$.” This target does that one-line change.

It is filler. The thesis runs over $\mathbb{R}$, where the sealed lemma already applies, so nothing downstream in the Leanpunov cascade calls this generalization. Its value is library completeness: it records the exact algebraic frontier of the passivity identity — precisely which scalar hypothesis the skew-form-vanishing fact needs. That frontier is ”$2$ is not a zero divisor”, and for a field that is exactly $\mathrm{ringChar}\ne 2$.

Proof narrative

Write $s:={\mathbf{x}}^{\top }\mathbf{Ax}$ (in Lean, x ⬝ᵥ A *ᵥ x). The manipulation is identical to the sealed $\mathbb{R}$ proof — it is pure transpose/bilinear algebra, valid over any commutative ring:

1. ${\mathbf{x}}^{\top }\mathbf{Ax}=({\mathbf{x}}^{\top }\mathbf{A})\mathbf{x}$ — associativity of the vector–matrix–vector product (dotProduct_mulVec).
2. ${\mathbf{x}}^{\top }\mathbf{A}=-(A\mathbf{x})$ — because ${\mathbf{x}}^{\top }\mathbf{A}=(A^{\top }\mathbf{x}{)}^{\top }$ and $A^{\top }=-A$ (mulVec_transpose, neg_mulVec).
3. Combining 1 and 2 with neg_dotProduct: $s=-((A\mathbf{x})\cdot \mathbf{x})$.
4. Symmetry of the dot product: $(A\mathbf{x})\cdot \mathbf{x}=\mathbf{x}\cdot (A\mathbf{x})=s$ (dotProduct_comm).

Substituting 4 into 3 gives the whole content in one line: $s=-s$, i.e. $-s=s$.

The only step that touches the characteristic is closing $-s=s\Rightarrow s=0$. Over $\mathbb{R}$ the sealed proof did this with linarith (which silently divides by two). Over a general field the same fact is a named Mathlib stone:

$\text{‘Ring.eq\_self\_iff\_eq\_zero\_of\_char\_ne\_two‘}:-a=a⟺a=0$

which holds in any NonAssocRing that is Nontrivial and NoZeroDivisors, given ringChar R ≠ 2. A field supplies all three instances automatically. Applying its forward direction to $-s=s$ yields $s=0$. $\square$

Why characteristic $\ne 2$ is the right hypothesis (and is necessary)

The characteristic enters through the diagonal. Skewness $A^{\top }=-A$ forces $A_{ii}=-A_{ii}$, i.e. $2A_{ii}=0$. Over a domain of characteristic $\ne 2$ this gives $A_{ii}=0$, the diagonal disappears, and pairing entry $(i,j)$ with $(j,i)$ (which cancel because $A_{ij}+A_{ji}=0$) kills the off-diagonal — so the whole form collapses.

Over characteristic $2$ the fact is false: there $-1=1$, so $A^{\top }=-A$ is the same condition as $A^{\top }=A$, the diagonal is unconstrained, and $A=\mathrm{diag}(1)$ is “skew” while ${\mathbf{x}}^{\top }\mathbf{Ax}=x_0^2=1\ne 0$ at $\mathbf{x}=(1)$. This counterexample is verified in the SymPy pin (test_char2_necessity_counterexample), confirming the Lean hypothesis is not decorative.

SymPy pin

pin_skew_charp.py in this directory. Three checks, all passing on new-pin-env:

• test_char0_symbolic_skew_vanishes — a symbolic $4\times 4$ skew matrix over $\mathbb{Q}$ (char $0$, hence $\ne 2$) has ${\mathbf{x}}^{\top }\mathbf{Ax}$ expand to exactly $0$ for symbolic $\mathbf{x}$.
• test_char_ne_2_finite_field_random_skew — random skew matrices over $\mathrm{GF}(3),\mathrm{GF}(5),\mathrm{GF}(7),\mathrm{GF}(11)$ give ${\mathbf{x}}^{\top }\mathbf{Ax}=0$ for random $\mathbf{x}$.
• test_char2_necessity_counterexample — the $\mathrm{GF}(2)$ diagonal counterexample above.

Mathlib stones used

• Matrix.dotProduct_mulVec, Matrix.mulVec_transpose, Matrix.neg_mulVec, Matrix.neg_dotProduct, Matrix.dotProduct_comm — the transpose/bilinear algebra (all commutative-ring generic, reused verbatim from the sealed $\mathbb{R}$ proof).
• Ring.eq_self_iff_eq_zero_of_char_ne_two — the single characteristic-sensitive step; Mathlib/Algebra/CharP/Basic.lean:127.

Interfaces left named

None. The theorem is fully closed — no sorry, no applier-side hypothesis beyond the mathematical content ($A^{\top }=-A$ and $\mathrm{ringChar}F\ne 2$).

Cost feel

Well under an L2-scale push — a single fix-free build. The generalization is genuinely one line versus the sealed proof: swap the trailing linarith for Ring.eq_self_iff_eq_zero_of_char_ne_two, and carry the ringChar F ≠ 2 hypothesis. The only work was locating the exact stone and confirming a Field discharges its Nontrivial/NoZeroDivisors obligations, which it does.

The machine seal

SkewCharP.lean in this directory (tracked source of truth); build copy at ~/lean/leanpunov/Leanpunov/SkewCharP.lean. Verbatim #print axioms (build 2026-07-06):

info: Leanpunov/SkewCharP.lean:46:0: 'Leanpunov.dotProduct_mulVec_self_of_skew_of_charP' depends on axioms: [propext, Classical.choice, Quot.sound]

No sorryAx — sealed.