An explicit finite list of Cayley units

import Definitions.Def_Octonion_cayleyIntegers
import Definitions.Def_Octonion_octonions
import Definitions.Def_Octonion_toRat8
import Mathlib.Algebra.Quaternion
import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic.Abel
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Push
import Mathlib.Tactic.Ring

/-!
# The 240 units of the Cayley integers

The units of `cayleyIntegers` are exactly its norm-one elements (`normSq_mul` plus integrality of
the norm gives one direction, `x · conj x = 1` the other), so enumerating them means solving
`Σ aᵢ² = 4` for doubled coordinate vectors `a` with Hamming parity pattern. Odd coordinates
contribute at least `1` each and their count lies in `{0, 4, 8}`, so there are exactly three
cases:

* pattern `0`: all coordinates even — one coordinate `±2`, giving the 16 units `±basisVec k`;
* a weight-`4` pattern: four odd coordinates, each `±1`, giving `14 · 16 = 224` units;
* pattern `255`: eight odd coordinates already have norm `≥ 2` — no units.

Total `16 + 224 = 240`. The half-integral units are coded by two bit masks `(m, t)`:
the weight-four parity mask `m` and a sign mask `t` marking where the sign is `+`
(only `t` restricted to `m` is visible). The integral units are listed separately.
That this is *exactly* the set of invertible Cayley integers is `mem_cayleyUnits_iff`.
-/

open Quaternion

namespace Octonion

/-- The fourteen weight-`4` codewords of `cayleyMasks`: the parity patterns on which a unit can
have half-integral coordinates. The all-ones word is too heavy to carry norm one. -/
def weight4Masks : Finset ℕ :=
  cayleyMasks.filter fun m => ((Finset.univ : Finset (Fin 8)).filter fun i => Nat.testBit m i.val).card = 4

/-- Signed half-vector of a mask pair: coordinates `±1/2` on the bits of `m` (`+` where `t` has a
bit) and `0` elsewhere. Doubled, this is an integer vector with parity pattern `patOfMask m`. Only the
restriction of `t` to `m` matters; other sign bits are ignored. -/
def signedRep (m t : ℕ) : octonions ℚ :=
  halfOf fun i => if Nat.testBit m i.val then if Nat.testBit t i.val then 1 else -1 else 0

/-- The set of all 240 units of the Cayley integers: the 16 sign vectors `±eₖ` (mask `0`) and
the 224 half-vectors with four odd coordinates on a weight-`4` Hamming word. The sign mask `t`
ranges over all of `2⁸`; only its restriction to `m` is visible, so the enumeration lists each
unit several times and the `Finset` deduplicates. That this is *exactly* the set of invertible
Cayley integers is `mem_cayleyUnits_iff`. -/
def cayleyUnits : Finset (octonions ℚ) :=
  ((Finset.univ : Finset (Fin 8)).biUnion fun k => {basisVec k, -basisVec k}) ∪
    weight4Masks.biUnion fun m => (Finset.range 256).image (signedRep m)

end Octonion