refactor(CompositionAlgebrasOverRings): deduplicate proofs flagged in review

[skipgaribaldi]

Follow-up to #665. This addresses the two proof-duplication findings in the code-quality rubric of the LLM review, and the unused private quaternion lemmas noted in the source review. It changes only LeanPool/CompositionAlgebrasOverRings/**/*.lean. No existing statement, definition, import or card entry changes. One theorem is added and two unused private lemmas are removed.

Classification specializations (Composition/Reduced/Classification.lean). The rank-four and rank-eight splitting theorems over LG rings and over PIDs, and the LG and PID forms of split ↔ isotropic (GPR 22.18, GPR 22.19), each repeated the argument of the matching theorem under GPR's freeness hypothesis. They are now wrappers that supply the freeness witness. Over an LG ring that is the existing ProjectiveConstantRankFree.of_isLGRing. Over a PID it is the new ProjectiveConstantRankFree.of_isPrincipalIdealRing: a finite projective module over a PID is torsion-free, hence free. The abstract rank-four and rank-eight theorems now come before their specializations.

Kernel splitting (Conic/Projective.lean, Composition/RankDichotomy.lean). norm_eq_of_projective, traceDefect_eq_zero_of_projective and eq_unitForm_smul_one_of_rankAtStalk_eq_one each built a projection onto ker unitForm by hand to get the Module.Finite and Module.Projective instances on it. Module.Finite.of_linearEquiv_prod and Module.Projective.of_linearEquiv_prod move unchanged from LGRing/ConstantRank.lean down to Module/Unimodular.lean, next to LinearMap.equivProdKerOfApplyEqOne. All three proofs now get the instances from that splitting.

Unused helpers (Composition/ComplexQuaternion.lean). This deletes the private quaternion_mk_mul and quaternion_star_mk, which nothing used. It also corrects the implementation note, which said the quaternion arithmetic went through them.

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 106 project modules: passed (2969 declarations).
• lake exe lint-style LeanPool, lake exe mk_all --module --check and git diff --check: passed.
• The unmodified lean_pool.quality checks, scoped to this project: passed. These cover the static repository checks, the card's declarations, the axiom audit (1548 declarations) and the option-backdoor audit.
• A dump of every project constant (name, kind, universe parameters and type, with binder names erased), compared between base and head. Leaving out compiler-generated _proof_N/_simp_N auxiliaries, the two dumps differ in exactly three entries: the added ProjectiveConstantRankFree.of_isPrincipalIdealRing and the two removed private lemmas. The moved of_linearEquiv_prod lemmas have identical types.

🤖 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] No blocking issue was found in the proof refactor or its public imports.

Summary

This proof-only refactor shares the classification arguments and the proofs that a kernel is finite and projective.

• LG rings and PIDs share the rank-four and rank-eight classification proof.
• Kernel proofs reuse one split to get finite and projective modules.
• The quaternion file drops two unused private lemmas.

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

[Vilin97]

{
"summary": "Reviewed all six complete diffs and the full changed modules at cc213de. The six LG/PID specializations now use the existing abstract freeness/classification theorems; their written public statements and surrounding hypotheses are preserved. The PID witness correctly supplies freeness for finite projective modules. The three unit-form-kernel arguments use the existing splitting equivalence and the same finite/projective complement lemmas, which have moved unchanged to Module/Unimodular. The removed private quaternion lemmas had no callers; the actual computations already use Mathlib's quaternion lemmas.\n\nThe project card, public entry/import modules, toolchain, manifest and lake configuration are unchanged. I found no source changes needed. This approval records the source review: authored run 39097751505 and main's separate push run 39094676507 were still building in the validation snapshots. Protected integration awaits applicable checks and the existing main-CI hold; no compile-time improvement is claimed.",
"assessment": {
"scope": "Existing CompositionAlgebrasOverRings refactor: six files, 62 additions and 159 deletions.",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Shared typed proofs replace repeated constructions while preserving the mathematical contracts, imports and public exposure."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: cc213de2ddff8a2a562225737c8f73c5c82faed9

Verdict: ✅ approve

The refactor replaces duplicated classification proofs with applications of the existing general theorems and reuses the kernel-splitting API in three proofs. The relocated complement lemmas remain available to their callers, and the deleted quaternion helpers were unused. Proof structure remains readable without added automation. Local compilation stopped at the first import because compiled Mathlib dependencies are absent, so the reported build results were not independently confirmed.

Aspect	Value
Scope	proof deduplication and helper relocation
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

Centralizing the shared arguments reduces maintenance work while retaining the structured proofs and reusable helpers.

---

Tokens: 636,373 in / 5,471 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.6276 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.