Jordan.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Orientation of surjective Jordan maps

This is the algebraic argument recalled in §5 of Universal strong Kadison–Kastler stability (2026), following I. N. Herstein, Jordan homomorphisms, Trans. Amer. Math. Soc. 81 (1956), 331–341. The target is assumed prime explicitly; no von Neumann algebra representation is needed for this algebraic step.

def OAI.KadisonKastler.PreservesJordan line 27
Source documentation
Preservation of twice the Jordan product. Over the complex numbers this is equivalent to preservation of (x * y + y * x) / 2.
```
def PreservesJordan (θ : A →ₗ[ℂ] B) : Prop :=
…
```
def OAI.KadisonKastler.IsPrimeAlgebra line 31
Source documentation
The ring-theoretic primeness condition used by the orientation proof.
```
def IsPrimeAlgebra (B : Type*) [Ring B] : Prop :=
…
```
theorem OAI.KadisonKastler.eq_of_add_self_eq_add_self line 34
theorem OAI.KadisonKastler.PreservesJordan.map_square line 38
theorem OAI.KadisonKastler.PreservesJordan.map_triple line 43
theorem OAI.KadisonKastler.PreservesJordan.map_triple_add_reverse line 57

theorem OAI.KadisonKastler.PreservesJordan.defect_relation line 72

Source documentation

The two potential multiplicative defects anticommute through every element of the target.

theorem PreservesJordan.defect_relation {θ : A →ₗ[ℂ] B}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ) (a b : A) (C : B) :
    (θ (a * b) - θ a * θ b) * C * (θ (a * b) - θ b * θ a) +
      (θ (a * b) - θ b * θ a) * C * (θ (a * b) - θ a * θ b) = 0 := by
…

Mentions: OAI.KadisonKastler.PreservesJordan

theorem OAI.KadisonKastler.prime_or_of_anticommutation line 88

theorem OAI.KadisonKastler.PreservesJordan.map_mul_or_map_mul_reverse line 103

Source documentation

For each pair of source elements, one of the two orientations holds.

theorem PreservesJordan.map_mul_or_map_mul_reverse {θ : A →ₗ[ℂ] B}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ)
    (hprime : IsPrimeAlgebra B) (a b : A) :
    θ (a * b) = θ a * θ b ∨ θ (a * b) = θ b * θ a := by
…

Mentions: OAI.KadisonKastler.PreservesJordan, OAI.KadisonKastler.IsPrimeAlgebra

theorem OAI.KadisonKastler.additive_zero_cover line 111
def OAI.KadisonKastler.mulDefect line 136
def OAI.KadisonKastler.reverseMulDefect line 149
theorem OAI.KadisonKastler.PreservesJordan.multiplicative_or_antimultiplicative line 166
Source documentation
Herstein's orientation theorem in the complex prime-target case. A surjective complex-linear Jordan map is multiplicative or antimultiplicative. The two applications of additive_zero_cover are the two additive-subgroup union arguments in the manuscript's proof.
```
theorem PreservesJordan.multiplicative_or_antimultiplicative {θ : A →ₗ[ℂ] B}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ)
    (hprime : IsPrimeAlgebra B) :
    (∀ a b, θ (a * b) = θ a * θ b) ∨ (∀ a b, θ (a * b) = θ b * θ a) := by
…
```
Mentions: OAI.KadisonKastler.PreservesJordan, OAI.KadisonKastler.IsPrimeAlgebra