{"id":"palomar/PALOMAR-2026-09-13-000001","url":"https://github.com/macgregor-sudo/albert-frame-triple-invariants/tree/dd06ef5d423a0e4a5d814d2c221e999b98887ee1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-13-000001-v1.json","repo":"https://github.com/macgregor-sudo/albert-frame-triple-invariants","tags":["math.RA","msc:17C40","msc:17C30","jordan-algebras","lean","invariant-theory"],"score":0,"title":"Rational invariants of three frames in the split Albert algebra: a Lean formalization","trust":"qualified","domain":"math.RA","source":"palomar","authors":["Robert R. MacGregor"],"reviews":0,"subject":"math.RA","summary":"Let J be the split Albert algebra over a field k of characteristic zero, the 27-dimensional Jordan algebra of 3 by 3 Hermitian matrices over the split octonions, with trace tr. A frame is an ordered triple of trace-one idempotents summing to 1. Three frames E, F, K carry 54 natural invariants under the group G of all unital k-linear bijections of J preserving its Jordan product: the pair traces tr(eᵢ∘fⱼ), tr(fⱼ∘kₗ), tr(kₗ∘eᵢ) and the triple traces tr(eᵢ∘(fⱼ∘kₗ)). This Lean 4 development proves that these traces do not generate all rational invariants of three frames, and that adjoining one…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-13","reactions":{},"formalized":true,"formalizes":[{"title":"Unpublished notes on frame-triple invariants","identifier":"","relationship":"adapts"},{"title":"Unpublished notes on comparison algebras","identifier":"","relationship":"adapts"},{"title":"Unpublished notes on rational coordinates","identifier":"","relationship":"adapts"}]}