v1.5.2 — Corrections from the 2026-08-03/run-173410 closing review

Changelog — v1.5.2

← Changelog index

---

v1.5.2 — Corrections from the 2026-08-03/run-173410 closing review

A second closing-review pass (reviews/2026-08-03/run-173410/) ran the same
multi-model panel-then-adjudication pipeline again — six Phase-1 reviewers,
four Phase-2 cross-critiques, five specialized reviewers (category theory,
notation, proof search, Lean audit, typesetting) — adjudicated into one
fix-ready report. This release applies the confirmed findings from that
report, all re-verified against the working tree before being applied.

Mathematical and category-theoretic corrections

Chapter 11, Section 5 — the free-category associativity claim was false.
The prose said the cons case of Path.append's recursion "is exactly
associativity of concatenation." It is not: that case is a definitional
recursion lemma used to unfold Path.append one arrow at a time, not a
proof that composition is associative. True associativity is now stated
explicitly, with the correct induction argument — on the third path
argument, matching Path.append's own recursion on its second argument
(the adjudicated report's own suggested fix direction, induction on the
first argument, was itself checked against the Lean source and found
incorrect; corrected here).

Chapter 11 — the free-category universal property is now stated in
full. The book named "universal property" without formulating it. It now
states $\mathrm{Hom}{\mathbf{Cat}}(\mathrm{Free}(Q), C) \cong
\mathrm{Hom}{\mathbf{Quiv}}(Q, U(C))$ explicitly, with $U$ named as the
forgetful functor $\mathbf{Cat} \to \mathbf{Quiv}$.

Chapter 11 index and Section 5 — composition verification claims were
overstated. A single rfl check on one concrete instance
(pathBetaAlphaViaAppend = pathBetaAlpha) was described as if it verified
associativity and identity laws in general. Both now qualify the claim to
the single concrete check it actually is.

Chapter 1, Section 4 — ℕ mislabeled as the initial object of Type.
The terminology box conflated Nat.rec's uniqueness (which comes from ℕ
being the initial $F$-algebra / natural number object for the successor
endofunctor) with the initial object of Type itself (the empty type).
Corrected, with a cross-reference to Section 1's existing $F$-algebra/NNO
discussion, which already had this right.

Chapter 1, Section 4 — forgetful functor table cited nonexistent Lean
fields. The table claimed Ring → Group uses r.toGroup and
Group → Set uses g.carrier; neither field exists. Verified against
Ch08Rings.lean: the real chain is r.addGrp (Ring → CommGroup) then
.toGroup (CommGroup → Group, from extends); Group's carrier is the
type parameter G itself, not a projected field.

Faithfulness and exercise-solution fixes

• Chapter 7, Theorem 1 (id_unique) — the book presented this proof
  with sorry; replaced with the actual compiling proof.
• Chapter 10, linear maps — the claim that composition/identity
  linearity are "easy to prove" pointed at nothing; the appendix already
  proves both (idLinearMap, composeLinearMap), now cross-referenced
  instead of left dangling.
• Appendix, Chapter 3 — ⟨1, rfl⟩ was offered as an alternative proof
  of 1 > 0; it does not compile on Lean 4.32.2 (1 > 0 is propositional,
  not definitional, equality). Corrected to ⟨1, Nat.one_pos⟩ with an
  explanation tying back to Chapter 5.
• Appendix, Chapter 11 — the Path.cons Infoview description in the
  solutions appendix didn't match the actual tactic state (fixed variable
  vs. auto-generated intermediate vertex). Corrected.
• Appendix, Chapter 10, Exercise 3 — now flagged explicitly as a
  partial solution (natural-scalar case only; the Int case is left as an
  exercise).
• Appendix, Chapter 11, Exercise 1 — now notes explicitly that the
  solution builds a fresh CyclicArrow/cyclicQuiver rather than
  extending the book's own ExampleArrow.
• Chapter 3, exercises — a Socratic answer claimed rfl cannot prove
  ∀ n, n + 0 = n; it can (Nat.add recurses on its second argument, so
  this is the base case). The genuinely unprovable statement is
  0 + n = n. Corrected.
• Minor proof-search narrative sharpening in Chapter 7 (Theorems 1–3) and
  Chapter 9 (Theorem 1–2): a lemma-availability claim, an Eq.symm
  metaphor, and an rw-failure anecdote misattributed to the wrong proof
  step.

Reference tables

• · disambiguated into two rows (Group.op, Chapter 6, vs. SMul,
  Chapter 10) with an explanatory note — same math notation, two different
  Lean operations depending on context.
• ⟶ was listed as "Chapter 1, never used"; it is used, in Chapter 11 —
  first-appearance column corrected instead of removed.
• Added missing entries: ¬ (lambda-calculus dictionary), ↑ coercion,
  ⊕ direct sum, a dedicated rfl row distinguishing tactic-use
  (Chapter 1) from proof-term-use (Chapter 3).
• Corrected ⟨_, _⟩ first-appearance from Chapter 2 to Chapter 1.
• Lambda-calculus dictionary's Σ-type row, which conflated structure
  with ∃, split into separate rows.

Front matter and documentation

• README.md, lean_book/README.md: removed a promised "ring as a
  one-object preadditive category" viewpoint that doesn't exist anywhere
  in Chapter 8 or the book; removed a stale claim that learning objectives
  are "never listed explicitly" (v1.5.0 added Learning objectives boxes to
  every chapter).
• REPRODUCING.md: fixed an invalid unquoted TOML value in prose
  (rev = v4.32.2 → rev = "v4.32.2"; the real lakefile.toml was
  already correctly quoted).
• Fixed a stale chapter/section cross-reference in Chapter 13's next-steps
  material (pointed at Chapter 11 Section 1 instead of Section 3) and a
  pronoun-ambiguity fix in the same file's Church-numeral discussion.
• Fixed a wrong Chapter 6/Chapter 7 theorem cross-reference in the Chapter
  6 exercises.
• NOTICE.md, lean_book_latex/frontmatter.tex: removed the "free-tier"
  qualifier from the AI-model review-panel description (the models
  themselves are unaffected; this was a wording-only fix), and removed
  the paragraph describing the reviews/2026-08-02/ round now that that
  directory has been removed from the repository.

Notes

• Every fix landed in the Markdown source; lean_book_latex/ was
  regenerated from it via build_latex.py. No .tex chapter file was
  hand-edited. preamble.tex and frontmatter.tex, which are hand-
  maintained (not generated), were edited directly.
• The .tex-only typesetting defects from the same review round
  (Infoview image overflow, bibliography URL overflow, glue-shrinkage
  errors, overfull hboxes, bibliography chapter-numbering collision) are
  not fixed in this release — they require direct edits to
  preamble.tex/bibliography.tex beyond a markdown regeneration and
  remain open.
• reviews/2026-08-02/ was removed from the repository in this release.
• The fixes themselves have not had a further adversarial re-review.
  Discrepancies found in the adjudicated report itself while applying its
  findings are documented in that report's POST-HOC CORRECTIONS section
  (reviews/2026-08-03/run-173410/p3-adjudication/FINAL-REVIEW.md).