Import Euclidean Jordan algebras and frame Peirce decomposition

[Vilin97]

Imports the complete Euclidean Jordan development from https://github.com/ehrlich-b/euclidean-jordan at a83407e4dbf73c77c31a2291c02f20b37a5ebbaf. All 49 production source files and proved solution bridges are retained: power associativity, spectral and trace-form results, order structure, Koecher/Alfsen–Shultz results, Hermitian matrix realizations, and the frame Peirce decomposition. Duplicate open statement surfaces and the diagnostic harness are omitted; their mathematical results remain in the proved bridges.

The Lean/Mathlib 4.34.0 port preserves the custom Hermitian Frobenius norm, updates matrix and continuous-functional-calculus APIs, documents public constructions, and removes unused finite/decidable assumptions. The standalone structure solution has a dedicated namespace. Original Bryan Ehrlich and vendored Alex Meiburg attribution, Apache-2.0 notices, and upstream AI provenance are preserved.

Validation at the September 25 module-migration checkpoint: warning-free project build, all 15 declaration linters, style, global module index, recursive proof-size/static quality, public axiom audit, and compiled environment audit pass. Project metadata checks pass. Fresh latest-head aggregate CI and independent review remain pending.

September 25 update: all retained files use the required Lean module system; public imports preserve the transitive API. Current main changes are integrated. Existing PR lifecycle state is preserved; no merge is requested.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Automation disposition: needs-maintainer

Reviewed exact head c1cf1d9e843d0ab9951448742ecc88550778a2d9 for this draft pooled-project/content import, Import Euclidean Jordan algebras and frame Peirce decomposition. The changed tree is a substantial source import (including LeanPool/EuclideanJordan.lean) with the pinned upstream source, project metadata, and generated index present. Observed exact-head required checks have no failures; profile evidence: no proof-profile comment was posted for this exact head.

No concrete author-actionable defect was established in this bounded review that would justify an ordinary change request. The PR is still marked draft, so protected merge is not permitted. Maintainer decision required: confirm the headline result's significance, faithfulness, novelty, source/provenance and scope, then ask the author to mark the PR ready (or give scope direction). This is a maintainer disposition, not an approval.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds mathematical library code for Jordan algebras.

No outstanding finding or new actionable issue prevents merging on this review.

Summary

Imports the Euclidean Jordan algebra development, including its Hermitian matrix carrier and frame Peirce decomposition.

• Registers the project and exposes its modules through the Lean Pool entry import.
• Changes since the previous review are unrelated Erdős 367 proof and import adjustments incorporated from main.

_{Reviews (15) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: c19522d81fd92abd8d6dbdddb637525d32b329b9

Verdict: 🛑 request_changes — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	🛑 block	Both card headlines are faithful, but the imported public API contains a vacuous monotonicity theorem requiring False.
Novelty	✅ pass	Searches of the pinned Mathlib and existing pool found no duplicate of either frame Peirce headline.
Significance	✅ pass	The frame Peirce decomposition and its supporting spectral, trace-form, and order theory constitute a substantial project that meets the pool’s significance bar.
Sources	🛑 block	Correct Albert’s stated characteristic requirements and the van de Wetering paper reference.
Code quality (advisory)	🤔 discuss	The core is organized, but duplicated public interfaces and avoidable low-level reproofs create substantial maintenance debt.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The headlines assume the defining Euclidean Jordan algebra identities and a complete family of pairwise orthogonal primitive idempotents; the dimension theorem additionally assumes finite dimensionality, as disclosed in the card.
Matches cited source	🛑 mismatch
Fit	✅ good_fit
Level	graduate
Branch	nonassociative algebra
Mode	theory_building
Code quality	2 / 5

Statement check: For a supplied Jordan frame, Lean proves the internal direct-sum decomposition and, under finite dimensionality, dimension one for every diagonal block.

The project develops Euclidean Jordan algebra structure theory, including frame existence, Peirce direct sums with one-dimensional diagonal blocks, and preservation of the Jordan product by unital linear order isomorphisms.

Faithfulness findings (1)

• vacuous-hypotheses — LeanPool/EuclideanJordan/EuclideanJordan/Vendor/HermitianMat/CFC.lean:1429
  This exported theorem assumes False, so it establishes no realizable case of CFC monotonicity: its entire conclusion follows by contradiction regardless of f. Retaining it presents an unusable statement as a mathematical result. Remove this declaration or replace the impossible premise with appropriate satisfiable hypotheses and establish the corresponding conclusion. The two card headlines do not depend on it.
  Evidence: theorem cfc_monoOn_pos_of_monoOn_posDef {d : Type*} [Fintype d] [DecidableEq d]
  {f : ℝ → ℝ} (hf_is_operator_convex : False) :
  MonotoneOn (HermitianMat.cfc · f) { A : HermitianMat d ℂ | A.mat.PosDef } := by
  exact False.elim hf_is_operator_convex

Sources findings (2)

• source-mismatch — LeanPool/EuclideanJordan/EuclideanJordan/PowerAssoc.lean:44
  The documentation for cm_eq_zero and jpow_mul_jpow misstates Albert’s theorem: Jordan power associativity holds in characteristic different from two, including positive characteristic. See Schafer, Chapter IV §1, pp. 91–93. Cancelling N + 3 is a requirement of this particular proof. Label it accordingly and remove the assertion that the theorem fails in positive characteristic; the real-scalar Lean statements can remain unchanged.
  Evidence: “Albert's theorem needs every positive integer invertible — it would fail in characteristic p for any p ≤ N+3”. The declarations instead assume [Module ℝ J], and prove theorem jpow_mul_jpow (x : J) (m n : ℕ) : jpow x m * jpow x n = jpow x (m + n + 1); the proof uses nsmul_eq_zero_iff' (n := N + 3).
• source-mismatch — LeanPool/EuclideanJordan/EuclideanJordan/OrderAuto.lean:86
  The explanation surrounding orderIso_preservesJordan sends readers to the wrong paper for the unformalized construction and its properties. arXiv:1803.11139 is Sequential Product Spaces are Jordan Algebras. The cited construction, fixing property, and cocycle identities are propositions 5.3, 5.5, and 5.7 of Three characterisations of the sequential product, arXiv:1803.08453. Correct the reference for all three propositions.
  Evidence: “the construction of Θ_a (van de Wetering, arXiv:1803.11139, Prop 5.3)” and “the fixing and cocycle properties (vdW Props 5.5, 5.7)”. The file explicitly says “Only the upgrade is proved here”; its declaration orderIso_preservesJordan concludes Φ (m x y) = m (Φ x) (Φ y).

Code quality findings (2)

• duplicate-definition — LeanPool/EuclideanJordan/StructureSolution.lean:324
  StructureSolution copies the trace implementation from TraceFormSolution and the frame implementation from FramePeirceSolution verbatim under another namespace. This includes fresh EuclideanJordanAlgebra and JordanFrame types, eigenspace/block definitions, and conversion proofs. Namespace isolation prevents name collisions but leaves separate public interfaces that must evolve together. Keep one implementation of each bridge and expose aliases from the combined solution; also share the formal-reality conversion repeated in both positivity proofs of both trace interfaces.
  Evidence: StructureSolution:324 and FramePeirceSolution:154 independently declare class EuclideanJordanAlgebra (J : Type*) [NormedAddCommGroup J] [InnerProductSpace ℝ J] extends Mul J, One J where, with identical fields. StructureSolution:384 and FramePeirceSolution:214 independently declare structure JordanFrame (J : Type*) [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (n : ℕ) where. Their block definitions are identical: def frameBlock (F : JordanFrame J n) : Sym2 (Fin n) → Submodule ℝ J := Sym2.lift ⟨frameBlockRaw F, frameBlockRaw_comm F⟩. StructureSolution:92 and TraceFormSolution:66 also repeat noncomputable def jtr : J →ₗ[ℝ] ℝ := (LinearMap.trace ℝ J).comp mulLₗ. The full trace and frame implementation blocks match their respective solution files exactly.
• proof-reimplementation — LeanPool/EuclideanJordan/EuclideanJordan/Vendor/HermitianMat/CFC.lean:526
  Several vendor proofs rebuild results already available in the same development. continuousOn_cfc_of_compact obtains a globally continuous extension, then unnecessarily goes through polynomial approximation and an epsilon-delta continuity proof; use cfc_continuous and cfc_congr on that extension. Matrix.sub_iInf_eignevalues similarly reconstructs a spectral-coordinate argument for the bound supplied by smul_one_le_of_eigenvalues_iff. Matrix.spectrum_subset_Ici_of_sub additionally proves finite-sum linearity by induction and reindexing instead of Matrix.sum_mulVec and dotProduct_sum, already used in HermitianMat/Order.lean:530. Reusing these APIs would remove parallel proofs that otherwise need separate maintenance during ports.
  Evidence: In continuousOn_cfc_of_compact, the extension is obtained with specialize this ( show IsClosed K from hK.isClosed ) ( ContinuousMap.mk ( fun x => g x ) <| by exact continuousOn_iff_continuous_domRestrict.mp hg ); refine ⟨_, this.choose.continuous.continuousOn, fun x hx => ?_⟩. Earlier declarations already provide protected theorem cfc_continuous {f : ℝ → ℝ} (hf : Continuous f) : Continuous (HermitianMat.cfc · f : HermitianMat d ℂ → HermitianMat d ℂ) and nonrec theorem cfc_congr (hfg : Set.EqOn f g (spectrum ℝ A.mat)) : A.cfc f = A.cfc g. Matrix.lean:1306 begins lemma sub_iInf_eignevalues (hA : A.IsHermitian) : (A - iInf hA.eigenvalues • 1).PosSemidef := by rw [Matrix.posSemidef_iff_dotProduct_mulVec], followed by diagonalization and coordinate calculations, while :1409 proves the equivalent bound with (PosSemidef.smul_one_le_of_eigenvalues_iff hA (iInf hA.eigenvalues)).mp (ciInf_le (Finite.bddBelow_range _)). In IsHermitian.spectrum_subset_Ici_of_sub, :1502 introduces have h_induction : ∀ (n : ℕ) (M : Fin n → Matrix d d 𝕜) (v : d → 𝕜), Star.star v ⬝ᵥ (∑ i, M i).mulVec v = ∑ i, Star.star v ⬝ᵥ (M i).mulVec v := by, followed by induction and Fintype.equivFin transport.

---

Tokens: 18,266,983 in / 41,305 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $368.4375 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 361a9eff8360eb89e9ec2da116cfea5c291d5a7c.

The exact-head Build project check fails because LeanPool.EuclideanJordan is not module-compatible under the current module root. Port the imported entry and closure, regenerate LeanPool.lean, and rerun complete protected CI.

Acceptance condition: repair the named defect on a new head and make all required protected checks green. Do not change repository policy or add waivers.

[Vilin97]

Changes requested by automated review

Reviewed head 74849305771d5a1abffb50b9aa0022aeae0ae2c8. Peirce decomposition for a given Jordan frame is independently substantial; not a claim of full classification.

1. Complete the pinned-toolchain integration. The exact-head build fails. Its concrete error includes:

   error: LeanPool.lean:1:0: cannot import non-`module` LeanPool.EuclideanJordan from `module`
   

   The file/dependency audit finds 36 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

Review coverage: complete changed-file inventory and full diff retained; 53 changed project files, 17,113 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Jordan, Peirce and orthogonal decomposition interfaces. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

[Vilin97]

Reviewed db56e96c5e7ad55e66d63d35b7d4ccdf8da2b315. The frame-relative Peirce direct-sum theorem and one-dimensional diagonal blocks are independently substantial. The project card correctly assumes a Jordan frame and does not claim a classification or a rank theorem. The source, Apache attribution and AI provenance remain intact.

Removed 32 duplicate copyright/license/author comment blocks after checking that each repeated the same copyright and authors and that the retained header preserves the license. Every executable token is unchanged. The mathematical source is also unchanged from the previously reviewed import after accounting for the module/public-import migration. Integrated current main while preserving all 218 existing project cards and this project's own card.

Validation: executable-token comparison, exact header/attribution comparison, generated module-index check and git diff --check passed. These comment-only repairs require no local proof rebuild; the required CI checks must pass on this head before normal merge. Approval recommendation is conditional on that CI.

[Vilin97]

Reviewed current integration head 305646bb13117450ad1b9b04c01cb78245e8745d. The project's Lean source is byte-identical to the previously reviewed db56e96c5e7ad55e66d63d35b7d4ccdf8da2b315; the existing mathematical assessment and fixes carry forward. The merge retains all 218 current-main project cards and this project's complete card, including their original text. The actual pinned mk_all --module --check command passes.

Recommendation: accept once fresh required CI passes. This review covers the lossless main integration; it does not claim another full local rebuild.

[Vilin97]

Changes requested by automated review

Reviewed 26619deb152f0bfce5bb60286856b00d998ed6d1. The frame Peirce decomposition and one-dimensional diagonal blocks are independently significant and faithfully stated for a supplied Euclidean Jordan algebra/frame. Current main integration leaves the project source unchanged, so the newly published substantive findings at its parent still apply.

1. Remove or meaningfully prove HermitianMat.cfc_monoOn_pos_of_monoOn_posDef in EuclideanJordan/Vendor/HermitianMat/CFC.lean:1429: its hypothesis is literally False, and its entire proof is False.elim. It has no callers, and neither headline needs it. It must not remain a public theorem purporting to establish matrix monotonicity.
2. Correct EuclideanJordan/PowerAssoc.lean:44: cancellation of N+3 restricts this particular real-vector-space proof, not Albert’s theorem to characteristic zero. The cited classical Jordan theorem holds in characteristic other than two; Schafer IV §1, pp. 91–93 supplies the source distinction.
3. Consolidate the duplicated CFC continuity and solution interfaces. continuousOn_cfc_of_compact constructs a continuous extension, then redoes polynomial approximation and an epsilon/3 proof despite the existing cfc_continuous/cfc_congr API. StructureSolution separately reproduces the trace/frame classes and block definitions exported by TraceFormSolution/FramePeirceSolution. Retain public names as wrappers around shared implementations, preserve headline statements, and rerun targeted build, linter/trust checks and exact-head quality review.

The repository source-size/trust-token scan passes, and earlier integration repairs are preserved. Green compilation does not resolve the vacuous public API or the source error; these have bounded author-actionable repairs, so no maintainer label is warranted.

[Vilin97]

Changes requested by automated review

Reviewed exact head e77d34d30d6a5fd1e90d0a03cad217befe326acd. The previous full diff, declaration/dependency and source review was reconciled with all current changed files, intervening edits, review threads, and available CI; preceding-head failures remain applicable to unchanged source. Valid earlier repairs are preserved.

The frame-relative Peirce decomposition and one-dimensional diagonal blocks are independently significant. However, the exported cfc_monoOn_pos_of_monoOn_posDef still takes _hFalse : False, so it proves no usable positivity-to-monotonicity bridge. The unchanged source-attribution/quality findings remain applicable; a green build does not repair a vacuous API.

Acceptance condition: Remove the vacuous exported bridge or replace it with a theorem proved from satisfiable, accurately documented hypotheses; reconcile the Albert/source scope and the concrete repeated proof scaffolding identified in the existing review. Preserve the exact limited Peirce scope.

Preceding completed CI on unchanged project source evidence: full job log.

Formal self-review is unavailable for this account; this is the changes-requested disposition, not an approval.

Successor-head reconciliation (e77d34d30d6a5fd1e90d0a03cad217befe326acd): The successor only integrates the already independently reviewed main changes; the submitted project source and the cited blocker/repair evidence are unchanged. Current observed gates: Build project=pending, Documentation preflight=pending, Content / non-content separation=SUCCESS. The disposition remains changes requested. This updates the existing review rather than adding a duplicate comment.