TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

If $char F \neq 2$ , quadratic forms and symmetric bilinear forms correspond by $q (v) = B (v, v)$ and $B (u, v) = \frac{1}{2} b_{q} (u, v)$

Statement

Let $char F \neq 2$ . The assignments

$B ⟼ q_{B}, q_{B} (v) = B (v, v), q ⟼ B_{q}, B_{q} (u, v) = \frac{1}{2} b_{q} (u, v)$

are inverse bijections between symmetric bilinear forms and quadratic forms.

Facts & Assumptions

Given: A field $F$ with $char F \neq 2$ and an $F$ -vector space $V$ .

[L1]

A quadratic form satisfies $q (a v) = a^{2} q (v)$ and has bilinear polar form $b_{q} (u, v) = q (u + v) - q (u) - q (v)$ (A quadratic form $q$ in arbitrary characteristic and its polar form $b_{q} (u, v) = q (u + v) - q (u) - q (v)$ ).

[L2]

A symmetric bilinear form is bilinear and satisfies $B (u, v) = B (v, u)$ (Bilinear forms, and symmetric, skew-symmetric, and alternating bilinear forms).

[L3]

The characteristic is the least positive natural multiple of $1_{F}$ that is zero, or $0$ if none exists (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise); in a field $0_{F} \neq 1_{F}$ and every nonzero scalar is invertible (Field).

Proof

technique · explicit inverse

1.1

Because $char F \neq 2$ , [L3] makes the scalar $2 = 1_{F} + 1_{F}$ nonzero and hence invertible. If $B$ is symmetric bilinear, then $q_{B} (a v) = a^{2} q_{B} (v)$ and $b_{q_{B}} (u, v) = B (u + v, u + v) - B (u, u) - B (v, v) = 2 B (u, v)$ . Thus $q_{B}$ is a quadratic form.

L1L2L3algebra

1.2

If $q$ is quadratic, [L1] makes $b_{q}$ bilinear, and its defining formula is symmetric. Hence $B_{q} = \frac{1}{2} b_{q}$ is symmetric bilinear by [L2] and [L3].

L1L2L3

2.1

Step 1.1 gives $B_{q_{B}} = B$ . Conversely, $b_{q} (v, v) = q (2 v) - 2 q (v) = 4 q (v) - 2 q (v) = 2 q (v)$ , so $q_{B_{q}} (v) = \frac{1}{2} b_{q} (v, v) = q (v)$ .

step 1.1step 1.2L1L3algebra

3.1

The two assignments are therefore mutually inverse bijections. The use of $2^{- 1}$ identifies precisely where the characteristic hypothesis enters.

step 2.1L3∎

Depends on

Used by

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, Bilinear Forms, §7 (standard reference, not scraped)

If char⁡F≠2charF=2, quadratic forms and symmetric bilinear forms correspond by q(v)=B(v,v)q(v)=B(v,v) and B(u,v)=12bq(u,v)B(u,v)=21​bq​(u,v)