Parallelogram Norm Law

Abstract

Inner-product geometry forces the squared-norm parallelogram identity.

Theorem 1.1 (Inner-product norms obey the parallelogram law).

$$\forall E:\mathrm{Type},[\mathrm{NormedAddCommGroup}(E)],[\mathrm{InnerProductSpace}(\mathbb{R},E)],\forall x,y:E,\mathrm{norm}(x+y{)}^2+\mathrm{norm}(x-y{)}^2=2(\mathrm{norm}(x{)}^2+\mathrm{norm}(y{)}^2).$$

Proof. Machine-checked in Lean as D5/S3/QuantumContext/ParallelogramNormLaw.inner_product_norm_parallelogram_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any real inner-product space and vectors x and y, the sum of the squared lengths of x+y and x-y is twice the sum of their squared lengths. This is the parallelogram identity singled out by the Jordan-von Neumann criterion.

Pinned Mathlib already proves the exact statement as parallelogram_law_with_norm. The Lean declaration is therefore the thinnest wrapper: it imports and applies that theorem directly.

This closes only the parallelogram-law clause of appendix E.46. It does not formalize the triangle-group interpretation, Farey recursion, or the crossing-alignment problem stated elsewhere in that atom.

Repository searches found no equivalent D5 declaration. Pinned-Mathlib source search found the exact theorem; the local smart-search name query returned no additional declaration.

References

• Truth anchor: D5/S3/QuantumContext/ParallelogramNormLaw.inner_product_norm_parallelogram_law