docs(SpinRepresentations): drop roadmap Layer references from Suggested.lean - #290
Open
kim-em wants to merge 1 commit into
Open
docs(SpinRepresentations): drop roadmap Layer references from Suggested.lean#290kim-em wants to merge 1 commit into
kim-em wants to merge 1 commit into
Conversation
…ed.lean Suggested.lean is a Lean code document, so it should use mathematical terms rather than roadmap planning vocabulary. Replace all 32 "Layer" references with the objects they name: section headings lose the "Layer N:" prefix, and in-prose references name the declaration or theorem instead. Also give Lawson-Michelsohn a precise citation in place of a chapter-wide one: the classification is §I.4, with Theorem 4.1 for the three recurrences (cliff_bott is their (4.3)), Theorem 4.3 for eight-periodicity, and Tables I and II for the tables. Record that their Cl(r,s) is this roadmap's Cliff(s, r), since §I.4 (4.0) sets Cl(1,0) = ℂ against Cliff(1,0) = ℝ × ℝ here; following the citation without that note gives the mirror image. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR removes the roadmap's "Layer" vocabulary from
SpinRepresentations/Suggested.leanand replaces a chapter-wide Lawson-Michelsohn citation with a precise one.Suggested.leanis a Lean code document, so it should use terms that fit in the final Lean source rather than roadmap planning concepts, per #225 (comment). All 32Layerreferences are gone: section headings lose theLayer N:prefix, and each in-prose reference names the object it meant (Layer 3's bivectorLieRingbecomesbivectorLieRing,the Layer-1 structure theorembecomesthe structure theorem,Independent of Layers 6-8becomesIndependent of the exceptional isomorphisms, the real forms, and triality, and so on). Nothing outside the file referenced these headings.The Lawson-Michelsohn entry now cites sections rather than the whole of Chapter I: §I.2 for Pin and Spin, §I.3 for the algebras, §I.4 for the classification, §I.5 for the representations, §I.10 for the
(1,1)-periodicity theorem.cliff_bottgains the specific pointer: it is Theorem I.4.1 (4.3), the two recurrences it needs are (4.1) and (4.2), eight-periodicity is Theorem I.4.3 (4.11)-(4.12) withCl(8,0) = M₁₆(ℝ)at (4.14), and the tables are Tables I and II.It also records a trap: Lawson-Michelsohn's
Cl(r,s)is this roadmap'sCliff(s, r). Their §I.4 (4.0) setsCl(1,0) = ℂandCl(0,1) = ℝ ⊕ ℝ, while the base entries here areCliff(1,0) ≅ ℝ × ℝandCliff(0,1) ≅ ℂ. Anyone following the citation without that note gets the mirror image of the table.Every claim above was checked against the book rather than recalled: §I.4 pp. 25-29, including the section list on the contents page.
Only comments and docstrings change; no target, signature or statement is touched.
🤖 Prepared with Claude Code