Split Chapter 1 into two balanced chapters - #245
Open
abderrahim-lectures wants to merge 10 commits into
Open
Conversation
…ences Chapter 1 was 18,278 words, 2.5x the next-biggest chapter, with three of its six sections each individually larger than most entire chapters elsewhere in the book. Split after Section 3 (not Section 2 as first suggested): the split boundary was chosen by weighing actual word counts rather than a guess, landing much closer to balanced (10,472 vs. 8,654 words, 1.2:1) than the alternative (5,735 vs. 13,391, 2.3:1, still an outlier). This also matches learning-paths.md's own pre-existing mermaid graph, which already anticipated exactly this boundary. New Chapter 1 (01-basics/, unchanged folder): Everything has a type, def/let/implicit arguments, Dependent types, plus its own exercises. New Chapter 2 (02-terminology-and-coc/, new folder): Terminology glossary, Pi/Sigma-types and the calculus of constructions, plus its own exercises, with genuine new chapter-opening narrative (learning objectives, "story of this chapter"), not a copy of the old framing. Every chapter from the old Chapter 2 onward renumbers up by one (functions-and-structures 2->3, ... appendix-solutions 14->15), including the parallel lean_project/LeanProject/ module-per-chapter naming and Ch01DependentTypes.lean's own split (its Pi/Sigma/CoC content moves to a new Ch02TerminologyAndCoC.lean). Fixed along the way, none of it pre-planned: - Hand-authored new files written mid-session with already-correct new numbers got double-bumped by the later mechanical sweep; fixed by hand. - Three reference forms beyond the literal word "Chapter N" needed their own sweeps: the abbreviated "Ch. N" nav-footer form, plural "Chapters N-M"/"Chapters N and M" ranges, and bare same-folder-relative links with no chapter-folder prefix in files that themselves moved. - Every appendix exercises-to-solutions cross-reference linked by filename, independently of the chapter-number text sweep, and was off-by-one after the appendix folder's internal renumbering. - build_latex.py's CHAPTERS list and DIAGRAM_MAP are hardcoded, not directory-scanned; updated, plus one more hardcoded appendix-folder string the plan didn't call out by name. - The multi-agent adversarial-review system (.opencode/agent/*.md, skills/*/SKILL.md) had real, functional chapter-scope assignments (file globs and chapter numbers) that would have misdirected future review runs, including a genuine coverage gap: old 01-basics/*.md implicitly covered what is now 02-terminology-and-coc/, which needed adding explicitly to a review slice rather than silently dropping out. - REPRODUCING.md is a historical prompt-replay log; past entries were left untouched (they describe the book's shape at the time), and this split was appended as a new entry instead. Explicitly not touched: changelog/, PROJECT-HISTORY.md, reviews/ (dated run outputs), AGENT_HANDOFF.md, all point-in-time historical records that should keep referencing chapter numbers as they were. Verified: full PDF rebuild (xelatex x3, biber), 289 pages, 0 errors, 0 missing-character errors, 0 broken internal links, 0 oversized images. An independent Markdown-level link+anchor checker found 0 broken links across all 115 non-changelog files (14 broken on the first pass, all same-folder-relative links that moved chapters, now fixed). lake build was launched against the real Mathlib dependency but its session-background process was lost before completion (no transcript, no completion record) and has not been re-verified in this pass; see the follow-up issue opened for it, matching the pattern from issue #242 on the previous PR. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
4 tasks
added 9 commits
August 7, 2026 21:27
… bugs; balance Chapter 3 Style: removes ~150 remaining sentence-connector colons and reintroduced possessives/em-dashes across Chapters 7-14 and the reference pages that survived the earlier prose-style pass, per the same no-colon/no-em-dash/ no-possessive rule. Correctness: fixes real regressions introduced by the chapter-1 split's renumbering script, found during a soundness/consistency audit: - 00-setup/00-index.md title said "Chapter 1" (collides with the Basics chapter); restored to "Chapter 0". - Every appendix-solutions file from the old Chapter 4 onward had its own heading, nav links, and in-body chapter/theorem citations numbered one chapter too high; corrected against the appendix index and spot- verified against real chapter content (e.g. Perm3.ext location). - Chapter 3's own index nav pointed back to Chapter 1 instead of Chapter 2. - learning-paths.md: "Why Lean?" mis-cited as Chapter 1 Section 1 (it's Chapter 0); a merged sentence wrongly attributed Chapter 1 content (Fin/Vec examples) to the toolchain-check step that belongs to Chapter 0. Balance: Chapter 3 was the only chapter in the book with no exercises section, which was most of why it read thin next to its neighbors. Adds 04-exercises.md (3 exercises: structure basics, type parameters, extends) with full worked solutions in a new appendix page, inserted as Chapter 3 in the appendix's sequence (renumbering the appendix's Chapter 4-12 files to make room, updating every cross-reference to them). LaTeX regenerated and PDF rebuilt; stale pre-split .tex files removed.
Add "Programmer's corner (Python)" boxes contrasting Lean guarantees with concrete Python failure modes: structure fields vs dict KeyError and mutable dataclasses (Chapter 3), and proof-carrying preconditions vs runtime assert statements (Chapter 4). Both motivate the value of Lean/functional programming with problems familiar from everyday Python code rather than abstract claims.
Add "Programmer's corner (Python)" boxes contrasting axiom-checked Lean structures with unchecked Python classes: a bare class silently accepting a non-associative operation as a "group" (Chapter 7), and duck-typed operator overloading discovering scalar/vector type mismatches only at run time, versus smul's fixed R -> M -> M type (Chapter 11).
Add "Programmer's corner (Python)" boxes: Python float breaking ring associativity via rounding, contrasted with the proof-obligated mul_assoc field (Chapter 9); and a hand-checked Python path-append function versus Path's connectivity guarantee baked into the type itself, making malformed paths unrepresentable rather than merely checked (Chapter 12).
Complete the Python-comparison pass across every main chapter: a proof-vs-test contrast for uniqueness of the identity (Chapter 8), NaN silently breaking the absorbing law that mul_zero proves unconditionally (Chapter 10), omega's proof of a universal statement versus an assert that only ever samples inputs (Chapter 13), and a capstone Programmer's corner in Chapter 14 tying the whole book's recurring theme together, invariants as types instead of conventions. Every main chapter (3, 4, 7, 8, 9, 10, 11, 12, 13, 14) now has at least one Programmer's corner grounding the value of Lean/functional programming in a concrete Python bug, alongside the pre-existing boxes in Chapters 1, 2, 5, 6.
…e pass Document the latest session as reproduction step 15 (style backlog, soundness audit, Chapter 3 balance, book-wide Python-comparison examples). Fix a stale appendix link left over from the chapter split (14-appendix-solutions -> 15-appendix-solutions), correct the chapter count (14 -> 15, Chapters 0-14), and describe the Programmer's corner boxes as now present in nearly every chapter rather than "at several points."
Fix section attributions left stale by the Chapter 1 split and earlier renumbering (e.g. "Chapter 1, Section 5" -> "Chapter 1, Section 3 (b)", "Chapter 4, Section 5" -> "Chapter 5, Section 5", "Chapter 8, Section 5" -> "Chapter 9, Section 5"), verified against where each box actually lives now. Add the ten new Programmer's corner snippets from this session's Chapters 3, 4, 7, 8, 9, 10, 11, 12, 13, 14 pass, so the notebook again matches its own claim of collecting every such box in the book. Every code cell verified to execute as commented.
Checkpoint projects sit after Chapter 6 (06-rigor-check) and Chapter 12 (12-path-algebras), not Chapter 5/11 as the README said, an off-by-one regression left over from before Chapter 1 was split into Chapters 1 and 2. Matches learning-paths.md, which already had this right.
Covers everything on this branch since the last release (v1.5.3): the unreleased v1.5.4 binder-styles work, the Chapter 1 split, the book-wide colon/possessive/em-dash style backlog, post-split numbering fixes, Chapter 3 balance (new exercises + appendix solutions), and ten new Python-comparison worked examples across Chapters 3-14.
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.
Summary
learning-paths.md's own pre-existing mermaid graph, which already anticipated exactly this boundary.01-basics/, unchanged folder): Everything has a type,def/let/implicit arguments, Dependent types, plus its own exercises.02-terminology-and-coc/, new folder): Terminology glossary, Π/Σ-types and the calculus of constructions, plus its own exercises, with genuine new chapter-opening narrative, not a copy of the old framing.lean_project/LeanProject/module-per-chapter naming (Ch01DependentTypes.leanitself split, its Π/Σ/CoC content moving to a newCh02TerminologyAndCoC.lean).Bugs found and fixed along the way (none pre-planned)
Ch. N, pluralChapters N-M/Chapters N and M, and bare same-folder-relative links with no chapter-folder prefix in files that themselves moved chapters.build_latex.py'sCHAPTERSlist andDIAGRAM_MAPare hardcoded, not directory-scanned; updated, plus one more hardcoded appendix-folder string..opencode/agent/*.md,skills/*/SKILL.md) had real, functional chapter-scope assignments that would have misdirected future review runs, including a genuine coverage gap (old01-basics/*.mdimplicitly covered what's now02-terminology-and-coc/, which needed adding explicitly to a review slice).REPRODUCING.mdis a historical prompt-replay log; past entries left untouched, this split appended as a new entry instead.Explicitly not touched:
changelog/,PROJECT-HISTORY.md,reviews/(dated run outputs),AGENT_HANDOFF.md, point-in-time historical records that should keep referencing chapter numbers as they were.Test plan
xelatex×3,biber): 289 pages, 0 errors, 0 missing-character errors, 0 broken internal\hyperreflinks, 0 oversized images.lake buildinlean_project/was launched against the real Mathlib dependency but its session-background process was lost before completion (no transcript, no completion record) and has not been re-verified in this pass. Tracked as a follow-up issue, matching the pattern from issue Verify the new Chapter 1 §3 Vec snippet (vecLen/vecLen') compiles with lake build #242 on the base PR.Base branch is
definition-styles-reducibility(the still-open binder-styles PR #241), since this work builds directly on top of it.🤖 Generated with Claude Code