Coordinate powers of the rank-one root lattice

The coordinate power of A₁ over a finite index type has the same integral carrier as the standard unit lattice, with twice its dot-product form. The resulting lattice equality also covers the empty index type and identifies orthogonal sums of copies of A₁ with scaled standard coordinates.

theorem TauCeti.IntegralLattice.coordinatePower_a1_eq_smul_unitLattice (ι : Type u_1) [Fintype ι] : a1.coordinatePower ι = 2 • unitLattice ι

An orthogonal sum of copies of A₁ is the standard integer-coordinate lattice with its form scaled by two.