The Moufang identities

In any alternative ring the three Moufang identities hold:

1. left a * (b * (a * c)) = ((a * b) * a) * c
2. right ((c * a) * b) * a = c * (a * (b * a))
3. middle (a * b) * (c * a) = a * ((b * c) * a)

Modulo the flexible law (IsAlternative.flexible) these agree with the forms in GPR 13.3.

⚠ Load-bearing for Layer 6. GPR 18.1 derives the Cayley–Dickson identities from the middle Moufang identity together with the linearized left alternative law (IsAlternative.left_alt_linearized). Both must remain available in exactly these shapes; if you restate them, check Conic/CayleyDickson.lean still elaborates.

Implementation notes

right_moufang is a short calc from the linearized alternative laws (IsAlternative.left_alt_linearized, IsAlternative.right_alt_linearized); its docstring gives the computation. left_moufang is obtained from right_moufang by transport along MulOpposite, using the IsAlternative αᵐᵒᵖ instance from Defs.lean, and middle_moufang from left_moufang, flexibility, the linearized right law and the alternating property of the associator.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 13.2, 13.3.
• Schafer, An Introduction to Nonassociative Algebras, §3.
• Zhevlakov et al., Rings That Are Nearly Associative, Ch. 2.

theorem IsAlternative.right_moufang {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b c : α) : c * a * b * a = c * (a * (b * a))

Right Moufang identity: ((c * a) * b) * a = c * (a * (b * a)).

Expand ((c a) b) a by the linearized left alternative law at (c a, b, a), and then (c a)(b a) by the linearized right alternative law at (c, a, b a); the right alternative law turns (c a) a and (b a) a into c a² and b a². What remains beside c (a (b a)) is c (b a²) + b (c a²) - ((c (b a)) a + (b (c a)) a), which vanishes because both sums equal (c b) a² + (b c) a²: the first by the linearized left law at (c, b, a²), the second by the linearized left law at (c, b, a) multiplied on the right by a, and the right alternative law.

theorem IsAlternative.left_moufang {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b c : α) : a * (b * (a * c)) = a * b * a * c

Left Moufang identity: a * (b * (a * c)) = ((a * b) * a) * c.

Proved by applying right_moufang in the opposite ring.

theorem IsAlternative.middle_moufang {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b c : α) : a * b * (c * a) = a * (b * c * a)

Middle Moufang identity: (a * b) * (c * a) = a * ((b * c) * a).

This is the form consumed by GPR 18.1 in the Cayley–Dickson construction.