The order structure on a Euclidean Jordan algebra #
The rest of this library runs on [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J],
which carries no order at all. This file supplies one: orderUnitSpaceOfBilinear produces an
OrderUnitSpace J for J a finite-dimensional formally real Jordan algebra, with the cone
of sums of squares as the positive cone and the Jordan unit as the order unit.
The cone, and why it is sums of squares rather than squares #
0 ≤ x is defined here as "x is a finite sum of Jordan squares" (IsSoS). The alternative —
x is a single square — is the right reading, but it is not usable as a definition:
closure of the single-square set under addition is not available before the spectral theorem,
whereas closure of the sums-of-squares set under addition is a concatenation of index sets. The
two readings are then proved equal in isSoS_iff_exists_sq — under the Euclidean
hypothesis of the third section, and not before.
Each field of OrderUnitSpace is paid for by exactly one thing:
| field | what pays for it |
|---|---|
le_refl, le_trans | the cone contains 0 and is closed under + |
le_antisymm | formal reality (eq_zero_of_isSoS_of_isSoS_neg) |
add_le_add_left | the order is a difference condition |
smul_nonneg_mono | r • (y ∘ y) = (√r • y) ∘ (√r • y) for r ≥ 0 |
ousUnit_nonneg | the unit is idempotent, hence a square |
archimedean (order-unit boundedness) | the spectral theorem |
★ The spectral theorem is what buys order-unit boundedness.
spectral_resolution_bilinear writes x = ∑ lam i • q i over an orthogonal idempotent family
summing to e, so r • e - x = ∑ (r - lam i) • q i is a sum of nonnegative multiples of
idempotents — a sum of squares — for any r dominating every lam i. The bound taken here is
∑ i, |lam i| rather than max lam: it dominates every coefficient, is manifestly
nonnegative, and needs no nonemptiness side condition when the resolution is empty.
Shape: a hypothesis-carrying def in bilinear-map vocabulary, not an instance #
Two deliberate choices, both forced by diamonds.
- A
def, never aninstance. A globalOrderUnitSpaceinstance keyed on the Jordan typeclasses would fire onHermitianMat d 𝕜, which already carries aPartialOrderand aNormfrom the vendored Loewner structure, putting two of each on the concrete carrier. Consumers writeletI := orderUnitSpaceOfBilinear …, exactly asEuclideanJordan/Bridge.lean'sringOfBilinearis used. - Bilinear-map vocabulary. Every statement takes the Jordan product as
m : J →ₗ[ℝ] J →ₗ[ℝ] Jover[NormedAddCommGroup J] [InnerProductSpace ℝ J], and reaches the ring vocabulary only inside proofs, viaringOfBilinear. Assuming[NonUnitalNonAssocCommRing J]and[NormedAddCommGroup J]together would give twoAddCommGroup Jinstances, which is the diamondEuclideanJordan/Bridge.leanwas written to dodge. Only oneAddCommGroupis ever in play here, and the produced structure'stoNormedAddCommGroupis the ambient instance on the nose (normedAddCommGroup_ofBilinear, proved byrfl).
Scope — what is and is not proved here #
- The Euclidean hypothesis
hassocis carried, not derived. Six declarations in the third section —inner_mul_self_nonneg_of_idem,inner_left_coeff,nonneg_coeff_of_inner_nonneg,nonneg_coeff_of_isSoS,isArchimedean_ofBilinear,isSoS_iff_exists_sq— assume an associative inner product,⟪x ∘ y, z⟫ = ⟪y, x ∘ z⟫. That is Faraut–Korányi's definition of Euclidean Jordan algebra (FK III.1), and over ℝ in finite dimension it is equivalent to formal reality — but that equivalence needs the trace form and is not formalized here. Both directions of the dependency are therefore hypotheses, andhermitian_jordan_assocsupplies a live carrier for the new one so that no theorem is conditional on an uninhabited premise. - The constructed order is the Loewner order on
H_n(𝕜). Both containments are proved —hermitian_isSoS_iff_nonneg,hermitian_le_ofEJA_iff. No square root on the carrier is needed for this: the spectral idempotents are themselves positive semidefinite, soHermitianMat.inner_ge_zeromakes⟪q i, A⟫ ≥ 0andinner_left_coeffreads the coefficient off.
The cone of sums of squares #
Nothing in this section mentions a norm or an inner product; the ambient structure is the
additive group and the ℝ-module, which is all the cone algebra needs.
The cone is closed under addition — the whole reason it is stated with sums of squares rather than squares: the witness is a concatenation of index sets.
Antisymmetry of the cone, and the only place formal reality is used in this file.
If a and -a are both sums of squares then the concatenated family has vanishing sum of
squares, so formal reality kills every member of it — including every member of a's own
family.
The partial order induced by the cone: x ≤ y iff y - x is a sum of squares.
Equations
- EuclideanJordan.partialOrderOfSoS m hfr = { le := fun (x y : J) => EuclideanJordan.IsSoS m (y - x), le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }
Instances For
The rearrangement both the order-unit bound and the Archimedean squeeze run on: against a
complete orthogonal idempotent family, r • e - x is again diagonal, with coefficients
r - lam i.
The order unit space #
From here the ambient structure is a finite-dimensional real inner product space carrying the Jordan product as a bundled bilinear map.
Order-unit boundedness, read off the spectral resolution. This is the field the EJA
layer had no way to supply before EuclideanJordan/Spectral.lean.
A Euclidean Jordan algebra is an order unit space, with the cone of sums of squares as the positive cone and the Jordan unit as the order unit.
A def, not an instance — see the module docstring. The NormedAddCommGroup and
NormedSpace parents are filled from the ambient instances, so no second normed structure is
created.
Equations
- One or more equations did not get rendered due to their size.
Instances For
No second normed structure. The produced order unit space's normed group is the
ambient one on the nose — the check that the ringOfBilinear diamond stays shut.
The effect space at EJA generality: the interval [0, e], unfolded to the two cone
conditions that define it.
EuclideanJordan/OrderUnitSpace.lean's spanning theorem, live at EJA generality. It is
here as evidence that the abstract effect API genuinely applies to the constructed structure,
not merely that the structure typechecks.
The Euclidean hypothesis: the Archimedean squeeze and the cone of squares #
The two results below need more than the order: they need the coefficients of a spectral resolution of a positive element to be nonnegative, which no amount of cone algebra supplies. What supplies it is the associative inner product — the "Euclidean" in Euclidean Jordan algebra.
L_c is a positive operator for an idempotent c.
L_c = P₁(c) + ½ P_{1/2}(c) on the nose, and both Peirce projections are idempotent
(EuclideanJordan/Peirce.lean's mul_peirceOne feeding peirceOne_of_eigen) and self-adjoint
(from
self-adjointness of L_c, which is hassoc at x := c). A self-adjoint idempotent P
satisfies ⟪P y, y⟫ = ⟪P y, P y⟫ ≥ 0, so the sum is nonnegative.
★ The eigenvalue trichotomy is never invoked, and no functional calculus is needed: the two
projections are polynomials in L_c that the tree already carries as linear maps.
A sum of squares has nonnegative spectral coefficients.
Pairing against q k reads the coefficient off — the idempotents are pairwise orthogonal for
the inner product because hassoc turns ⟪q k, q i⟫ into ⟪q k, q k ∘ q i⟫ — while pairing
against the sum-of-squares presentation is nonnegative term by term, each term being
⟪L_{q k} f j, f j⟫.
This is the fact that both isArchimedean_ofBilinear and isSoS_iff_exists_sq reduce to, and
it is the only content in this file that the order axioms themselves do not supply.
A coefficient is nonnegative as soon as its idempotent pairs nonnegatively with the
element — the shape shared by nonneg_coeff_of_isSoS (where the pairing is nonnegative
because x is a sum of squares) and by hermitian_nonneg_le_isSoS (where it is nonnegative
because x is positive semidefinite).
The genuine Archimedean property, in the sense
EuclideanJordan/OrderUnitSpace.lean's IsArchimedean carries: an element under every
positive multiple of the unit is nonpositive.
This is strictly stronger than the class's archimedean field, which is order-unit
boundedness only. ★ It is proved here at EJA generality; before this, H_n(𝕜) was the only
carrier known to satisfy it, so results assuming IsArchimedean had a single model.
The cone of the order is the cone of squares. The two readings of 0 ≤ x — a sum of
squares, and a single square — coincide, so a development that defines positivity as "is a
square" agrees with the one built here; that agreement is a theorem rather than a stipulation.
The forward direction is the whole content: a sum of squares has nonnegative coefficients, so
∑ √(lam i) • q i squares back to it by orthogonality.
A live carrier for the hypothesis bundle #
H_n(𝕜) satisfies every hypothesis above, including the associative-inner-product hypothesis
this file introduces, so nothing in the two previous sections is conditional on a premise with
no carrier. The construction is applied to it at the end; the resulting order unit space is a
second one on H_n(𝕜), kept as a def and never an instance, and it is not proved
equal to the vendored Loewner structure (see the module docstring).
The Euclidean hypothesis, live on H_n(𝕜). Both sides are
½(Tr[ABC] + Tr[BAC]) after Matrix.trace_mul_cycle.
The two facts below are the only ones that need HermMul's scoped multiplicative
instances (CommMagma, MulZeroClass, IsCommJordan), so the open is confined to this
block rather than covering the whole section.
★ That confinement is hygiene, not a fix, and the record should say so. It was made while
chasing an elaboration blow-up in hermitian_isArchimedean_ofEJA and
hermitian_isSoS_iff_exists_sq on the theory that a second multiplicative structure in scope
was making unification search a diamond. It changed nothing — the timeout survived it
unaltered, as did a second theory that the mismatch between HermitianMat.instAddCommGroup
and NormedAddCommGroup.toAddCommGroup was being paid for (that defeq costs about a second in
isolation). The real cause is recorded at the two call sites below.
★★ Why every application below pins (J := HermitianMat n 𝕜) explicitly.
Without it these three declarations exhausted 200 000 heartbeats, and raising the budget was
the wrong move: with maxHeartbeats 0 the elaboration ran for two minutes and then failed,
having defaulted J := ℕ off the bare numeral 1 supplied for the explicit e : J. The
profiler names the cost exactly. With J unsolved, the m argument stays a metavariable
through the argument list, so checking hermitian_formallyReal becomes the higher-order
problem
∑ i, (?m (f i)) (f i) =?= ∑ i, ((jordanBilinG ?n) (f i)) (f i),
and isDefEq unfolds Finset.sum through Multiset.foldr, Quot.liftOn and List.map
hunting for a match — thirteen seconds, and it fails. Pinning J makes the same unification
first-order and the whole file elaborates in about six seconds.
The transferable rule: an isDefEq timeout under a Finset.sum usually means a
metavariable in the function position, not a budget that is too small. Ascribing the
numeral ((1 : HermitianMat n 𝕜)) is necessary too but not sufficient — it removes the wrong
ℕ answer without removing the search.
The construction, applied to H_n(𝕜). Its only job is to witness that the
hypothesis bundle of orderUnitSpaceOfBilinear is inhabited.
Equations
Instances For
The Archimedean squeeze holds for the constructed structure on H_n(𝕜), so
isArchimedean_ofBilinear is not vacuous either.
And the cone of the constructed order is the cone of squares on H_n(𝕜).
The constructed order is the Loewner order on H_n(𝕜) #
Fidelity, not inhabitedness: the abstract cone could have been inhabited and still been the wrong cone. Both containments are below.
A Jordan square in H_n(𝕜) is positive semidefinite: the Jordan square is the matrix
square, and M M = Mᴴ M for M Hermitian.
A Jordan idempotent is therefore positive semidefinite: it is its own square.
Sums of squares are positive semidefinite.
The containment that needed the Euclidean hypothesis: a positive semidefinite matrix is
a sum of squares. Its spectral idempotents are themselves positive semidefinite, so
⟪q i, A⟫ ≥ 0 by HermitianMat.inner_ge_zero, and inner_left_coeff reads that off as
lam i ≥ 0.
The abstract cone is the Loewner cone on H_n(𝕜).
The constructed order relation is the Loewner order relation.