[skipgaribaldi]

Follow-up to #665 and #674. This adds one file, Composition/Fields/Euclidean.lean, connecting CompositionAlgebrasOverRings to the CompositionAlgebras project (Hurwitz's theorem for Euclidean composition algebras). It changes only LeanPool/CompositionAlgebrasOverRings/**/*.lean. No existing statement, definition or card entry changes. The two import indexes gain the new module, Imports.lean via lake exe mk_all.

The bridge. A Euclidean composition algebra in the sense of CompositionAlgebras is a real vector space with a unital bilinear product and a positive definite symmetric form B with B(xy, xy) = B(x, x) B(y, y). CompositionAlgebra.toConicAlgebra makes a nontrivial one into a ConicAlgebra ℝ C with norm nf; the degree-two identity is that project's sq_eq. isComposition_toConicAlgebra shows it is a composition algebra (GPR 19.5) when finite-dimensional. Multiplicativity is the composition law. Non-singularity follows from isGPRNonsingular_iff_nondegenerate and anisotropy, since 2 is invertible over ℝ.

The three results. Each is stated exactly as in CompositionAlgebras, in the namespace CompositionAlgebra.ViaConic:

CompositionAlgebras main result	Restated here as	Proved from
CompositionAlgebra.finrank_eq_one_or_two_or_four_or_eight	ViaConic.finrank_eq_one_or_two_or_four_or_eight	IsComposition.finrank_eq_one_or_two_or_four_or_eight (GPR 19.18)
CompositionAlgebra.hurwitz_classification	ViaConic.hurwitz_classification	IsComposition.isomorphic_of_anisotropic (GPR 23.13), via the new ViaConic.exists_isCompIso_of_finrank_eq
CompositionAlgebra.CD.instCompositionAlgebra (its composition law)	ViaConic.cd_comp	isMultiplicative_cay (GPR Exc. 18.18)

For the classification, two Euclidean composition algebras of the same dimension have positive definite norms of the same dimension, so isomorphic_of_anisotropic gives an isometry preserving 1 and multiplication. That is IsCompIso. It is applied directly against that project's structures on ℝ, ℂ, ℍ[ℝ] and Octonion. For the double, CompositionAlgebra.CD D is literally Cay(D, -1): both are D × D with (a, b)(c, d) = (ac - (conj d) b, da + b (conj c)), and cstar is conj (conj_toConicAlgebra). cd_comp is stated with CD.bilin rather than nf so that its statement does not pass through CD.instCompositionAlgebra. It needs no finite-dimensionality, like the original.

The fourth main result of CompositionAlgebras, Octonion.nucleus_real, is a computation in the concrete octonions and has no counterpart here.

What is and is not used from CompositionAlgebras. The statements use its definitions, including its composition-algebra instances on ℝ, ℂ, ℍ, 𝕆 and their dimensions. The proofs use its elementary identities (sq_eq, comp, nf_one, adjointness of cstar). The proofs do not use its doubling chain or its Cayley–Dickson cross-term computation. This was checked mechanically: the transitive constant closure of each of the three theorems contains none of CompositionAlgebra.finrank_eq_one_or_two_or_four_or_eight, CompositionAlgebra.hurwitz_classification, CompEmb.double, exists_unit_orthogonal, CD.compositionAlgebraOfAssoc or CD.cross.

Cross-project imports have precedent in the pool, e.g. Superdiffusion → HighContrastHomogenization and EscauriazaSereginSverak → CaffarelliKohnNirenberg.

Validation, run locally against the pinned Lean and Mathlib:

• lake build LeanPool.CompositionAlgebrasOverRings.Imports: no warnings.
• lake env lean --run scripts/ci/lint-project.lean on all 107 project modules: passed (2987 declarations).
• lake exe lint-style on the new file, lake exe mk_all --check, lake exe mk_all --module --check and git diff --check: passed.
• lean_pool.quality --static-only: passed.
• #print axioms for the three theorems: only propext, Classical.choice, Quot.sound.
• Each original statement was checked to be proved by its restatement, e.g. example : type_of% @CompositionAlgebra.hurwitz_classification.{0} := @fun C _ _ _ _ _ _ _ => ViaConic.hurwitz_classification C. For the double: example : CompositionAlgebra.B (x * y) (x * y) = CompositionAlgebra.B x x * CompositionAlgebra.B y y := ViaConic.cd_comp x y at CD D.

🤖 Generated with Claude Code

[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 impact] The PR adds theorem access within the Lean composition-algebra library.

No blocking code issue was found; narrowing the import would remove an unnecessary dependency.

Findings

1.  Unused proofs become required imports ▶

Summary

Adds a bridge from Euclidean composition algebras to ConicAlgebra over the reals.

• Euclidean composition algebras connect to the general conic-algebra theory.
• Finite-dimensional Euclidean algebras have dimensions one, two, four, or eight.
• Finite-dimensional Euclidean algebras match ℝ, ℂ, ℍ, or 𝕆.
• Associative Euclidean doubles satisfy the composition law.

Review covered the added module, related definitions and proofs, project cards, and import paths. External source texts, independent upstream license verification, and compile-time measurements were unavailable and remain unverified. No runtime or build verification was performed.

_{Reviews (1) · Last reviewed commit: "feat(CompositionAlgebrasOverRings): deri..." · Reviewed by Greptile}

[greptile-apps]

Unused proofs become required imports

Euclidean.lean imports Classification, but its proofs only need the definitions and instances available through Isomorphisms. Classification also imports Hurwitz, bringing the original dimension proof and doubling chain into both public entry points of CompositionAlgebrasOverRings. This adds an avoidable dependency for users and future changes. Import LeanPool.CompositionAlgebras.Composition.Isomorphisms instead.

Suggested change

	public import LeanPool.CompositionAlgebras.Composition.Classification
	public import LeanPool.CompositionAlgebras.Composition.Isomorphisms

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 193.15 s (= 3.22 min) — user 549.20 s, sys 63.86 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

A base→head comparison was attempted but its measurements are unavailable (see the run log); modified files are omitted from the tables below.

Statement changes

✅ No statements changed — all 0 tracked declarations across 2 modified files kept their type; only proofs / definition bodies changed.

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Total heartbeats: 56,649 maxHeartbeats units across 1 valid file (201 added LOC).

Sum of lean --profile: 4880.8 ms (= 4.88 s) across 1 valid file. Import-excluded time: 1970.8 ms (= 1.97 s).

Count-heartbeats wall-clock total: 7.60 s. Repeated import cost inside lean --profile: 2910.0 ms (= 2.91 s).

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Commands	Errors
LeanPool/CompositionAlgebrasOverRings/Composition/Fields/Euclidean.lean	199	56,649	7.60	4.88	1.97	2.91	56	0
LeanPool/CompositionAlgebrasOverRings.lean	1	—	—	—	—	—	0	1
LeanPool/CompositionAlgebrasOverRings/Imports.lean	1	—	—	—	—	—	0	1
Total	201	56,649	7.60	4.88	1.97	2.91	56	2

Aggregate phase totals

Phase	Time
import	2910.0 ms (= 2.91 s)
typeclass inference	928.0 ms (= 0.93 s)
interpretation	328.0 ms (= 0.33 s)
tactic execution	201.0 ms (= 0.20 s)
elaboration	167.0 ms (= 0.17 s)
type checking	95.5 ms (= 0.10 s)
simp	64.6 ms (= 0.06 s)
initialization	48.3 ms (= 0.05 s)
tacticAnalysis	36.2 ms (= 0.04 s)
ring	24.3 ms (= 0.02 s)
linting	17.9 ms (= 0.02 s)
overlappingInstancesLinter	13.8 ms (= 0.01 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.CompositionAlgebrasOverRings.Composition.Fields.Euclidean	2.70 s

Per-file `lean --profile` output

LeanPool/CompositionAlgebrasOverRings/Composition/Fields/Euclidean.lean

import took 2.91s
cumulative profiling times:
	attribute application 3.63ms
	compilation (IR) 0.0901ms
	compilation (LCNF base) 2.39ms
	compilation (LCNF impure) 0.362ms
	compilation (LCNF mono) 0.642ms
	congr simp thm 3.63ms
	elaboration 167ms
	fix level params 1.72ms
	import 2.91s
	initialization 48.3ms
	instantiate metavars 1.62ms
	interpretation 328ms
	let-to-have transformation 0.413ms
	linting 17.9ms
	module linting 0.00141ms
	norm_num 2.93ms
	overlappingInstancesLinter 13.8ms
	parsing 9.94ms
	process pre-definitions 11.7ms
	ring 24.3ms
	share common exprs 7.17ms
	simp 64.6ms
	tactic execution 201ms
	tacticAnalysis 36.2ms
	type checking 95.5ms
	typeclass inference 928ms
real 5.07
user 3.04
sys 1.30

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.