Diagonal forms with coefficients in the same square classes

Rescaling each coordinate by a unit identifies diagonal quadratic forms whose corresponding coefficients differ by squares. This is the form-level comparison used when choosing coefficients by approximation in local square classes. The comparison uses Mathlib's QuadraticForm.isometryEquivWeightedSumSquaresWeightedSumSquares.

theorem TauCeti.equivalent_weightedSumSquares_of_isSquare_div {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {w v : ι → Rˣ} (h : ∀ (i : ι), IsSquare (w i / v i)) : (QuadraticMap.weightedSumSquares R w).Equivalent (QuadraticMap.weightedSumSquares R v)

Two diagonal forms with unit weights are isometric if corresponding weights differ by squares.