An integer quadratic map from the parallelogram law

Abstract

An integer quadratic map from the parallelogram law.

Definition 1.1 (An integer quadratic map from the parallelogram law).

Lean statement: D5/S3/QuadraticForms/ParallelogramConstruction.ofParallelogram

Formalization. D5/S3/QuadraticForms/ParallelogramConstruction.ofParallelogram (✓ std3).

Citation. Michael Stoll; David Kurniadi Angdinata; The Tau Ceti contributors; Kevin Buzzard (2026). Canonical heights, parallelogram constructions and arithmetic point transport. URL: https://github.com/TauCetiProject/TauCeti/tree/934db6ae0034643ffe7b5180242f9ec4c00a56ae.

Commentary.

For additive commutative groups M and N with injective doubling on N, a function f satisfying f(x + y) + f(x - y) = 2f(x) + 2f(y) determines an integer quadratic map with underlying function f and companion polarization f(x + y) - f(x) - f(y).

The construction derives the value at zero, evenness, integer quadratic scaling and the three-variable polarization identity. The latter gives biadditivity. Injective doubling permits cancellation; without it a constant nonzero function on a group of exponent two can satisfy the parallelogram law and fail the required zero identity.

References

• Truth anchor: D5/S3/QuadraticForms/ParallelogramConstruction.ofParallelogram