Degen's eight-square identity

DefinitionSign of a product of octonion basis elements#✓fully proved

The sign of the product of basis elements indexed by p and q.

The output basis index is p ^^^ q. Bits are read least-significant first, so bits 0, 1, and 2 correspond to the source coordinates 1, 2, and 3.

def basisSign (p q : BitVec 3) : Int :=
  let p₁ := (p.getLsbD 0).toNat
  let p₂ := (p.getLsbD 1).toNat
  let p₃ := (p.getLsbD 2).toNat
  let q₁ := (q.getLsbD 0).toNat
  let q₂ := (q.getLsbD 1).toNat
  let q₃ := (q.getLsbD 2).toNat
  (-1) ^ (p₁ * q₁ + p₁ * q₂ + p₁ * q₃ + p₂ * q₂ + p₂ * q₃ + p₃ * q₃ +
    q₁ * p₂ * p₃ + p₁ * q₂ * p₃ + p₁ * p₂ * q₃)

Used by 4

Used bySign cancellation for two decompositions of an xor index · Basis multiplication signs square to one · Signed structure constant of the eight-square algebra · Contraction of two structure constants

DefinitionSigned structure constant of the eight-square algebra#✓fully proved

The signed structure constant for the basis product indexed by p and q.

def structureConstant (p q k : BitVec 3) : Int :=
  if p ^^^ q = k then basisSign p q else 0

Uses 1 · Used by 4

Statement usesSign of a product of octonion basis elements

Used byStructure constants are bounded by one · Contractions of structure constants are bounded by one · Eight-square crossing identity · Contraction of two structure constants

TheoremBasis multiplication signs square to one#✓fully proved

Every basis multiplication sign squares to one.

@[simp] theorem basisSign_mul_self (p q : BitVec 3) :
    basisSign p q * basisSign p q = 1

Uses 1

Statement usesSign of a product of octonion basis elements

TheoremSign cancellation for two decompositions of an xor index#✓fully proved

The cancellation rule of signs for two distinct decompositions of one xor index.

theorem basisSign_mul_add_swap {p q p' q' : BitVec 3}
    (hxor : p ^^^ q = p' ^^^ q') (hne : q ≠ q') :
    basisSign p q * basisSign p' q' +
      basisSign p q' * basisSign p' q = 0

Uses 1

Statement usesSign of a product of octonion basis elements

TheoremContraction of two structure constants#✓fully proved

Contracting two structure constants leaves their common xor component.

theorem sum_structureConstant_mul (p q p' q' : BitVec 3) :
    (∑ k : BitVec 3, structureConstant p q k * structureConstant p' q' k) =
      (if p ^^^ q = p' ^^^ q' then basisSign p q * basisSign p' q' else 0)

Uses 2

Statement usesSign of a product of octonion basis elements · Signed structure constant of the eight-square algebra

TheoremEight-square crossing identity#✓fully proved

The two contractions in the eight-square crossing decomposition.

theorem crossing_identity (x y u v : BitVec 3) :
    (∑ k : BitVec 3, structureConstant x y k * structureConstant v u k) +
      (∑ k : BitVec 3, structureConstant x u k * structureConstant v y k) =
        2 * (if x = v ∧ y = u then 1 else 0)

Uses 1

Statement usesSigned structure constant of the eight-square algebra

TheoremStructure constants are bounded by one#✓fully proved

A structure constant has absolute value at most one.

theorem abs_structureConstant_le_one (p q k : BitVec 3) :
    abs (structureConstant p q k) ≤ 1

Uses 1

Statement usesSigned structure constant of the eight-square algebra

TheoremContractions of structure constants are bounded by one#✓fully proved

A contraction of two structure constants has absolute value at most one.

theorem abs_sum_structureConstant_mul_le_one (p q p' q' : BitVec 3) :
    abs (∑ k : BitVec 3, structureConstant p q k * structureConstant p' q' k) ≤ 1

Uses 1

Statement usesSigned structure constant of the eight-square algebra

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.