Albert's power-associativity theorem

The statement

A commutative Jordan ring can have a nonassociative multiplication. Nevertheless, powers of a single element multiply as expected: the product of two positive powers is the power with the summed exponent. The statement doesn’t require a multiplicative unit.

xᵐ⁺¹ · xⁿ⁺¹ = xᵐ⁺ⁿ⁺².

The Lean recursion starts at exponent one: jpow x 0 = x and jpow x (n + 1) = x * jpow x n. This explains the shifted indices in the declaration.

Hypotheses

• J is a NonUnitalNonAssocCommRing satisfying the Jordan identity, IsCommJordan J.
• Its additive group carries an ℝ-module structure. The proof uses this to cancel nonzero natural multiples, giving additive torsion-freeness.
• There are no finite-dimensionality, positivity, formal-reality, or inner-product hypotheses.

What’s not proved

The theorem doesn’t make the whole ring associative. It concerns repeated products of one element.

The real scalar action isn’t required to interact with multiplication. In particular, this registered statement doesn’t assert that the real subalgebra generated by an element is associative: the hypotheses don’t supply that algebra structure. It doesn’t establish the theorem in positive characteristic.

variable {J : Type*} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J]

theorem jpow_mul_jpow (x : J) (m n : ℕ) :
    jpow x m * jpow x n = jpow x (m + n + 1)