feat: normalize quadratic forms over separably closed fields

[utensil]

Roadmap: RepresentationTheory

Summary

Adds the quadratic-form normalization used by the Spin polarization construction.

• Proves that a finite-dimensional nondegenerate form over a separably closed field is equivalent to the unit-weight sum of squares.
• Reuses the generic result at both polarization normalization sites.

Roadmap target

Supplies the normalization step used by SpinRepresentations Layer 4.

Verification

Full gates, consumers, import probes, golf, and aggregate 2+1 pass at 089ed41e4926dc3115a30850e96b131d6a0d7443.

Scale and generality

Changes two files by +64/−28 lines. The theorem applies to finite-dimensional nondegenerate quadratic forms over separably closed fields with invertible 2.

Scope

• Consumes: Mathlib’s sum-of-squares normalization and separably closed square roots.
• Provides: the unit-weight normalization theorem.
• Fits: removes duplicate normalization machinery from the Spin polarization constructor.
• Boundary: split-model construction and odd-dimensional Clifford structure remain separate.

_{🤖 GPT-5.6 Sol high · local aggregate 2+1 fixed: attribution (1)}

[CBirkbeck]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The normalization theorem faithfully follows from orthogonal diagonalization and the existence of square roots of nonzero weights over separably closed fields with characteristic different from two. Its two polarization uses preserve the original semantics.
✅	reuse	approved	codex/gpt-5.6-sol	The separably closed normalization is genuinely more general than Mathlib’s algebraically closed result, and the implementation reuses Mathlib’s weighted-sum equivalence and scaling combinator.
✅	scope	approved	codex/gpt-5.6-sol	This is a single-topic extraction of normalization machinery already present in the Spin polarization implementation, with direct use in the roadmap’s Layer 4 maximal-isotropic construction.
✅	attribution	approved	codex/gpt-5.6-sol	The new module explicitly credits both central Mathlib declarations whose normalization argument it adapts and identifies the relevant roadmap layer; no missing attribution was found.
✅	api-design	approved	codex/gpt-5.6-sol	The new canonical theorem exposes the normalization required by downstream Spin construction, while its proof-only isometry helper remains private. No obsolete, over-exposed, or insufficiently characterized public surface is introduced.
✅	generality	approved	codex/gpt-5.6-sol	The normalization theorem matches Mathlib’s natural finite-dimensional quadratic-form API and uses the assumptions required by the underlying orthogonal-basis classification and separably closed square-root result.
✅	placement	approved	codex/gpt-5.6-sol	The generic normalization theorem is correctly placed under LinearAlgebra/QuadraticForm, and its two focused Mathlib imports directly supply the separably closed and quadratic-isometry APIs it uses.
✅	naming	approved	codex/gpt-5.6-sol	The new public theorem follows the adjacent Mathlib precedent QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed, accurately describes its conclusion and hypothesis, and introduces no notation.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive module and its public theorem are documented accurately, with appropriate scope, purpose, and attribution.
✅	proof-quality	approved	codex/gpt-5.6-sol	The new normalization proof is concise, readable, and follows the established Mathlib construction without undocumented definitional-equality manipulation or brittle proof chains.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 089ed41. rubrics @ f854a7e. Review spend: $1.42.}