QuaternionReflections.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Pure quaternion lifts of the reflections needed to choose a local spectral frame. Only their concrete action on the two quaternion triples is used; no global eigenframe or representation theorem is assumed.

def OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination line 17
def OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection line 20
theorem OAI.PositiveEinsteinFour.QuaternionFrame.combination_square_expansion line 23
theorem OAI.PositiveEinsteinFour.QuaternionFrame.combination_square_symmetrized line 35

theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination_square line 51

Source documentation

The square of a pure quaternion is minus its real squared norm.

theorem imaginaryCombination_square
    (Q : Fin 3 → Mat4)
    (hQ : ∀ r s, Q r * Q s + Q s * Q r =
      (if r = s then (-2 : ℝ) else 0) • (1 : Mat4)) (u : Fin 3 → ℝ) :
    imaginaryCombination Q u * imaginaryCombination Q u =
      (-(∑ r, u r ^ 2)) • (1 : Mat4) := by
…

Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination

theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination_transpose line 76
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination_anticommutator line 90
theorem OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection_combination line 109
Source documentation
The lifted spectral change sends each imaginary basis element to its line reflection.
```
theorem axisReflection_combination (Q : Fin 3 → Mat4) (u : Fin 3 → ℝ) (s : Fin 3) :
    (∑ r, axisReflection u r s • Q r) =
      (2 * u s) • imaginaryCombination Q u - Q s := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection, OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination

theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination_orthogonal line 122

Source documentation

A unit pure quaternion is an orthogonal four-frame transformation.

theorem imaginaryCombination_orthogonal
    (Q : Fin 3 → Mat4)
    (hanti : ∀ r s, Q r * Q s + Q s * Q r =
      (if r = s then (-2 : ℝ) else 0) • (1 : Mat4))
    (hskew : ∀ r, (Q r)ᵀ = -Q r)
    (u : Fin 3 → ℝ) (hu : ∑ r, u r ^ 2 = 1) :
    (imaginaryCombination Q u)ᵀ * imaginaryCombination Q u = 1 := by
…

Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination

theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination_intertwines line 135
Source documentation
The explicit intertwining law for the imaginary basis, with the line reflection represented by a unit pure quaternion.
```
theorem imaginaryCombination_intertwines
    (Q : Fin 3 → Mat4)
    (hanti : ∀ r s, Q r * Q s + Q s * Q r =
      (if r = s then (-2 : ℝ) else 0) • (1 : Mat4))
    (u : Fin 3 → ℝ) (hu : ∑ r, u r ^ 2 = 1) (s : Fin 3) :
    imaginaryCombination Q u * Q s =
      (∑ r, axisReflection u r s • Q r) * imaginaryCombination Q u := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination, OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_commutes_opposite line 149
Source documentation
A left pure-quaternion frame change fixes the opposite triple.
```
theorem imaginaryLeft_commutes_opposite (u : Fin 3 → ℝ) (s : Fin 3) :
    imaginaryCombination quaternionMatrix u * Angular.oppositeMatrix s =
      Angular.oppositeMatrix s * imaginaryCombination quaternionMatrix u := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination, OAI.PositiveEinsteinFour.Angular.oppositeMatrix
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryRight_commutes_positive line 159
Source documentation
A right pure-quaternion frame change fixes the positive triple.
```
theorem imaginaryRight_commutes_positive (u : Fin 3 → ℝ) (s : Fin 3) :
    imaginaryCombination Angular.oppositeMatrix u * quaternionMatrix s =
      quaternionMatrix s * imaginaryCombination Angular.oppositeMatrix u := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination, OAI.PositiveEinsteinFour.Angular.oppositeMatrix
theorem OAI.PositiveEinsteinFour.QuaternionFrame.oppositeMatrix_transpose line 168
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_matrix line 176
Source documentation
The unit pure-quaternion lifts preserve four-dimensional orientation.
```
private theorem imaginaryLeft_matrix (u : Fin 3 → ℝ) :
    imaginaryCombination quaternionMatrix u =
      ![![0, -u 0, -u 1, -u 2], ![u 0, 0, -u 2, u 1],
        ![u 1, u 2, 0, -u 0], ![u 2, -u 1, u 0, 0]] := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryRight_matrix line 185
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_det line 195
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryRight_det line 205
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryLeft_det_one line 215
theorem OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryRight_det_one line 219
theorem OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection_apply line 225
Source documentation
The coefficient matrix is precisely the ordinary line reflection that occurs as minus a Cartan–Dieudonné plane reflection.
```
theorem axisReflection_apply (u x : EuclideanSpace ℝ (Fin 3)) (hu : ‖u‖ = 1) :
    WithLp.toLp 2 (axisReflection u *ᵥ (x : Fin 3 → ℝ)) =
      (Submodule.reflection (ℝ ∙ u)) x := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection