diff --git a/CLAUDE.md b/CLAUDE.md
index 27e6ff6..cf8cf95 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -64,11 +64,20 @@ AI-usage disclosure paragraph at the end of commit messages is important wheneve
 When migrating material, AI should try to translate (English to Portuguese) but not rewrite or invent new text. Only humans should deviate from the original CSwFP texts.
 
 
-# Pedagogical decisions
-
-We will avoid fragmented presentation of material. That is why we will largely reorder CSwFP.
-
-We should avoid presenting definitions that will be rephrased later, with the same name that in another chapter would have a new definition. Eventually, namespaces would avoid conflicts, but students may get confused. But exceptions can occur.
-
-We will never discuss `haskell vs Lean` decisions in the book. The reader does not necessarily know Haskell and should not worry about it. We also do not expect the reader to have read the original CSwFP. This book is self-contained. As a result, we never mention CSwFP sections, pages, etc.
+# Style guides
+
+The normative conventions live in two files, which are to be read in addition
+to this one. **Read both in full before creating or editing any file that ends
+up in the book**; everything you write must conform to them.
+
+- `STYLE-CODE.md` — Lean code and Verso markup: the ledger of which Lean
+  feature is first used in which chapter (the book's hard constraint is that
+  nothing is used before it is presented), the directive vocabulary, the build
+  variants, and naming.
+- `STYLE-WRITING.md` — prose: the project's pedagogical decisions, writing
+  advice, and the Portuguese conventions including the term list.
+
+`CONTRIBUTING.md` covers workflow. `DEVIATIONS.md` records what departs from
+CSwFP and why. In case of conflict, the style guides win on style and this
+file wins on project scope.
 
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 0000000..8198921
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,107 @@
+# Contributing to CSwL
+
+This file covers workflow and mechanics. For conventions, read `STYLE-CODE.md`
+(Lean and Verso) and `STYLE-WRITING.md` (prose and Portuguese) — both are
+normative, and both should be read before you edit anything that reaches the
+book.
+
+Everything about the project is in English: this file, identifiers, code
+comments, commit messages, issues. Only the book's prose is in Portuguese.
+
+## Who decides what
+
+The book's content and its structure — what a chapter says, what order the
+material comes in, which exercises exist, how chapters are divided — are the
+author's. Contributions are welcome on everything else, and are most valuable
+where a task is objective:
+
+- reporting anything that does not build, or builds with an unexpected warning;
+- reporting prose that is wrong, unclear, or badly translated;
+- working the exercises and reporting those that are unsolvable, ambiguous, or
+  mis-rated;
+- checking that a chapter uses no Lean feature the book has not yet presented
+  (`STYLE-CODE.md` has the ledger);
+- fixes to typos, markup slips, and broken references.
+
+A change that reorganizes material, adds or removes an exercise, or introduces
+a Lean feature earlier than the ledger records is a proposal, not a fix: open
+an issue and let the author decide.
+
+## Getting set up
+
+Install Lean via [elan](https://lean-lang.org/install), then clone the
+repository and fetch the prebuilt Mathlib — without this, `lake build`
+compiles all of Mathlib from scratch:
+
+```sh
+lake exe cache get
+lake build
+```
+
+Use VS Code with the Lean 4 extension. Opening any file under `CSwL/` will
+prompt to install the toolchain the book pins.
+
+To build and read the book locally:
+
+```sh
+make serve   # http://127.0.0.1:8000/
+```
+
+`make all` generates all four variants under `_out/`. See `STYLE-CODE.md` for
+what each variant is.
+
+## Issues
+
+Pending work is tracked in [GitHub
+issues](https://github.com/cslib-community/CSwL/issues). Anything you find that
+you are not fixing yourself belongs there.
+
+For a comment that is local to one passage and only makes sense with that
+section in view, use a `:::dev` note in the Lean file itself rather than an
+issue. Those render as editorial notes and never reach the student.
+
+## Branches and pull requests
+
+- `main` must always build.
+- Do not commit to `main`; work on a branch and open a pull request.
+- Keep a pull request to one coherent piece of work. Smaller and sooner beats
+  bigger and later.
+- Before opening it, check that what you touched still builds — `lake build
+  CSwL.Sets` for a single chapter, `make all` if you changed the
+  infrastructure or anything that affects the generated variants.
+- Delete the branch once it is merged.
+
+Commit messages follow [Conventional
+Commits](https://www.conventionalcommits.org/): `feat:`, `fix:`, `docs:`,
+`refactor:`, with an optional scope — `docs(readme): …`, `fix(logic): …`.
+
+## Editing the right file
+
+The book's sources are the Lean files under `CSwL/`. Everything under `_out/`
+is generated and is overwritten by the next `make` — never edit there.
+
+That includes the generated projects' `README.md`, which comes from
+`readmeTemplate` in `CSwLMeta/Save/Project.lean`.
+
+## AI usage
+
+AI may be used in this project, under conditions that differ from the ones
+some related projects adopt. The rules:
+
+- **AI never writes prose on its own initiative.** It produces text only when
+  explicitly asked, and what it produces is a draft for a human to revise.
+- **When migrating material, AI translates.** English to Portuguese, as
+  literally as the target language allows. It does not rewrite, expand,
+  restructure, or invent. Deviating from the source is a human decision.
+- **AI-generated commentary is marked as such**, and belongs in `:::dev`
+  blocks, which never reach the student.
+- **Infrastructure is different.** Code under `CSwLMeta/` and the scripts
+  around the build are not book content, and AI may write them — but a file
+  that is mostly AI-written says so at the top, because it will typically be
+  less carefully considered than hand-written code.
+- **Commit messages** that describe AI-assisted work carry a disclosure
+  paragraph in English, added only after a human approves it. Never
+  `Co-Authored-By: Claude`.
+
+`CLAUDE.md` holds the instructions Claude Code reads at the start of a
+session; it points at this file and the two style guides.
diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean
index 6609976..636d7c4 100644
--- a/CSwL/Logic/FOL.lean
+++ b/CSwL/Logic/FOL.lean
@@ -5,6 +5,8 @@ import Mathlib.Tactic.Use
 open Verso.Genre Manual
 open CSwLMeta
 
+set_option verso.code.warnLineLength 100
+
 #doc (Manual) "Lógica de predicados" =>
 %%%
 tag := "FOL"
@@ -57,8 +59,8 @@ arbitrário e prove que vale para ele. É a mesma `intro` agora sobre um objeto
 
 ```lean
 example (h : ∀ x, P x) : ∀ y, P y := by
-  intro y
-  exact h y
+  intro n
+  exact h n
 ```
 
 A introdução de `∃` exige exibir a testemunha. A tática `use` substitui a variável quantificada pelo objeto passado, e deixa como objetivo o que falta provar sobre ele.
diff --git a/CSwL/Logic/PL.lean b/CSwL/Logic/PL.lean
index 8b8615b..3664984 100644
--- a/CSwL/Logic/PL.lean
+++ b/CSwL/Logic/PL.lean
@@ -19,9 +19,9 @@ namespace PL
 
 # Introdução
 
-A lógica proposicional (LP, ou cálculo sentencial) trata de fórmulas construídas a partir de variáveis proposicionais usando os conectivos `¬`, `∧`, `∨`, `→` e `↔`. Intuitivamente, uma variável proposicional `p` representa uma sentença ou proposição que pode ser verdadeira ou falsa. Queremos usar lógica proposicional para fugir das impressões das línguas naturais. Formalizar proposições e provas quando podemos concluir uma proposição a partir de outras proposições tomadas como premissas.
+A lógica proposicional (PL, "Propositional Logic") trata de fórmulas construídas a partir de variáveis proposicionais usando os conectivos `¬`, `∧`, `∨`, `→` e `↔`. Intuitivamente, uma variável proposicional `p` representa uma sentença ou proposição que pode ser verdadeira ou falsa. Podemos usar lógica proposicional para fugir das impressões das línguas naturais. Queremos tornar precisa a noção de que uma proposição `α` decorre de outra proposição `β`.
 
-Como primeiro exemplo, adaptado de {citet Bib.enderton2001}[], a sentença "traços de potássio foram observados" pode ser traduzida para a linguagem formal como o símbolo `K`. Já para a sentença fortemente relacionada "traços de potássio não foram observados", podemos usar `¬ K`. Aqui `¬` é o nosso símbolo de negação, lido como "não". Poderíamos também pensar em traduzir "traços de potássio não foram observados" por algum símbolo novo `J`, mas preferimos decompor sentenças em suas partes atômicas tanto quanto possível. Para uma sentença não relacionada, "a amostra continha cloro" escolhemos o símbolo `C`. Assim, as seguintes sentenças compostas podem ser formalizadas.
+Como primeiro exemplo, adaptado de {citet Bib.enderton2001}[], a sentença "traços de potássio foram observados" pode ser traduzida para a linguagem formal como o símbolo `K`. Já para a sentença relacionada "traços de potássio não foram observados", podemos usar `¬ K`. Aqui `¬` é o nosso símbolo de negação, lido como "não". Poderíamos também pensar em traduzir "traços de potássio não foram observados" por algum símbolo novo `J`, mas preferimos decompor sentenças em suas partes atômicas tanto quanto possível. Para uma sentença não relacionada, "a amostra continha cloro" escolhemos o símbolo `C`. Assim, as seguintes sentenças compostas podem ser formalizadas.
 
 - A sentença "Se traços de potássio foram observados, então a amostra não continha cloro." é formalizada como `(K → (¬C))` com símbolo `→` significando "se ... então ...".
 - A sentença "A amostra continha cloro, e traços de potássio foram observados." é formalizada como `(C ∧ K)` com símbolo `∧` significando a conjunção "e".
diff --git a/CSwL/Sets.lean b/CSwL/Sets.lean
index 0ab3e93..110c3ea 100644
--- a/CSwL/Sets.lean
+++ b/CSwL/Sets.lean
@@ -583,6 +583,10 @@ modelo a um fragmento — um domínio de entidades e, para cada verbo, a
 relação que ele denota — e à qual o tratamento de verbos de mais de dois
 lugares, e do escopo entre eles, volta mais tarde.
 
+:::dev "Alexandre (arademaker)"
+Estamos apresentando conceitos dentro do enunciado de um exercício. Talvez seja melhor evitar isso.
+:::
+
 ::::exercise (rating := 2) (name := "cartesian-square")
 
 Tome `A` como o conjunto `{Kasparov, Karpov, Anand}`. Encontre `A × A`.
diff --git a/CSwLMeta/Comment.lean b/CSwLMeta/Comment.lean
index 383c2da..38d730f 100644
--- a/CSwLMeta/Comment.lean
+++ b/CSwLMeta/Comment.lean
@@ -77,10 +77,13 @@ def decodeDevData? (data : Json) : Option (Option String × Option String × Opt
     some (str? a, str? u, nat? y)
   | _ => none
 
-/-- Should a dev note surface in reader-facing outputs (the HTML book and the
-generated `.lean` files)?  Only *actionable* notes are shown: those with urgency
-`NOW` or `BeforeNextRelease`, or with no urgency at all.  `PotentialImprovement`
-notes remain suppressed. -/
+/-- Should a dev note be rendered at all, in the variants that keep it (every
+one but `student`)?  Only *actionable* notes are: those with urgency `NOW` or
+`BeforeNextRelease`, or with no urgency at all.  `PotentialImprovement` notes
+remain suppressed.
+
+This is the second of two filters and is about urgency alone; which variants
+keep a note is decided in `Block.devcomment`'s `traverse`. -/
 def devNoteShown (urgency : Option String) : Bool :=
   match urgency with
   | none => true
@@ -98,8 +101,9 @@ def devUrgencyText (urgency : String) : String :=
 /-- Label for a rendered dev note —
 `Nota editorial (Alexandre Rademaker, before next release, 2026)` — with
 absent fields omitted.  The heading names the note without naming the source
-this book adapts: `CSwL` is self-contained, and a rendered note reaches every
-variant, the student one included. -/
+this book adapts, since `CSwL` is self-contained: the note does not reach the
+student build, but it does reach the `terse` one the instructor opens in
+class. -/
 def devNoteLabel (author urgency : Option String) (year : Option Nat)
     (heading : String := "Nota editorial") : String :=
   let fields := author.toList ++ (urgency.map devUrgencyText).toList ++ (year.map toString).toList
@@ -107,17 +111,29 @@ def devNoteLabel (author urgency : Option String) (year : Option Nat)
   else s!"{heading} ({String.intercalate ", " fields})"
 
 /-! `Block.devcomment` carries the note body as its children and records its
-author/urgency metadata in `data`. All notes survive traversal (the CSwL has
-no student/solutions split on this block — every variant is a "reader" of the
-book). Among the surviving blocks, a note is rendered only when its urgency
-passes `devNoteShown` (`NOW`, `BeforeNextRelease`, or none): highlighted in the
-HTML book, and passed through as a labelled comment in generated `.lean` files
-by `CSwLMeta.Save.Extract.walkBlock`.  `PotentialImprovement` notes render
+author/urgency metadata in `data`.
+
+A dev note is addressed to the book's authors, so **no note survives traversal
+in the `student` variant** — neither the HTML nor the generated `.lean`, since
+both are produced from the per-variant traversed tree. The other three
+variants keep every note: `solutions` and `grading` are the authors' own, and
+`terse` is the instructor's, where a note on screen during a class is
+harmless.
+
+Among the surviving blocks, a note is rendered only when its urgency passes
+`devNoteShown` (`NOW`, `BeforeNextRelease`, or none): highlighted in the HTML
+book, and passed through as a labelled comment in generated `.lean` files by
+`CSwLMeta.Save.Extract.walkBlock`.  `PotentialImprovement` notes render
 nothing. -/
 block_extension Block.devcomment (author : Option String)
     (urgency : Option String) (year : Option Nat) where
   data := Json.arr #[toJson author, toJson urgency, toJson year]
-  traverse _ _ _ := return none
+  traverse _ _ _ := do
+    if (← getCurrVariant).isStudent then
+      -- Dev notes are for the authors; the student build gets none of them.
+      return some (.concat #[])
+    else
+      return none
   toHtml :=
     open Verso.Output.Html in
     some fun _ goB _ data contents => do
diff --git a/CSwLMeta/Save/Project.lean b/CSwLMeta/Save/Project.lean
index 5f12454..be15fd9 100644
--- a/CSwLMeta/Save/Project.lean
+++ b/CSwLMeta/Save/Project.lean
@@ -112,15 +112,49 @@ private def lakefileTemplate (vol : String) (v : Variant)
   "name = \"" ++ vol ++ "\"\n" ++
   libs
 
+/-- The `student` variant is the one the students receive, so its README is the
+  whole set-up guide: how to build, how to work an exercise, how to report a
+  problem. The `solutions` and `terse` variants are read by the instructor, who
+  has the repository itself, and get only the note saying where they came from.
+  The `grading` variant gets additional instructions for its private autograder
+  below. Written in English, like every other document about the project; only
+  the book's prose is in Portuguese. -/
 private def readmeTemplate (vol : String) (v : Variant) : String :=
-  s!"# {vol} — variante `{v}`\n\n" ++
-  "Gerado a partir do livro (Verso, gênero `Manual`) por " ++
-  s!"`lake exe cswl-book {v}` — **não edite aqui**: a fonte é o `CSwL`.\n\n" ++
-  (if v.isGrading then
-    "Esta variante traz as provas completas e os atributos " ++
-    "`[autogradedProof …]`. Para corrigir uma entrega:\n\n" ++
-    "    lake exe autograder --local <entrega> <arquivo deste projeto>\n\n" ++
-    "Ela nunca sai do repositório privado.\n"
+  s!"# {vol} — `{v}` variant\n\n" ++
+  "Generated from the book (Verso, `Manual` genre) by " ++
+  s!"`lake exe cswl-book {v}` — **do not edit here**: the source is `{vol}`, " ++
+  "and the next build overwrites this directory.\n\n" ++
+  (if v.isStudent then
+    "## Setting up\n\n" ++
+    "Install Lean with [elan](https://lean-lang.org/install). Then, in this\n" ++
+    "directory, fetch the prebuilt Mathlib and build:\n\n" ++
+    "    lake exe cache get\n" ++
+    "    lake build\n\n" ++
+    "`lake exe cache get` matters: without it, `lake build` compiles all of\n" ++
+    "Mathlib from scratch.\n\n" ++
+    "Use VS Code with the Lean 4 extension, and open **this directory** as\n" ++
+    "the folder — not a file inside it, or the extension will not find the\n" ++
+    "project.\n\n" ++
+    "## Working the exercises\n\n" ++
+    "Each exercise is a `sorry` to replace. Lean checks your answer as you\n" ++
+    "type: while a `sorry` remains, the file reports a warning, and when the\n" ++
+    "proof or definition is complete the warning disappears. The InfoView\n" ++
+    "panel shows the goal at the cursor.\n\n" ++
+    "The exercises are in the same order as the book, and each one sits in\n" ++
+    "the chapter section that discusses it. Read the corresponding section\n" ++
+    "of the book alongside the code.\n\n" ++
+    "Keep your own copy of anything you want to survive: this directory is\n" ++
+    "regenerated from the book, and a rebuild overwrites whatever is here.\n\n" ++
+    "## Reporting a problem\n\n" ++
+    "If something does not build, a statement is ambiguous, or the prose is\n" ++
+    "wrong, open an issue at\n" ++
+    "<https://github.com/cslib-community/CSwL/issues>. Say which chapter and\n" ++
+    "which exercise, and paste the message Lean gave you.\n"
+   else if v.isGrading then
+    "This variant carries the complete proofs and the `[autogradedProof …]`\n" ++
+    "attributes. To grade a submission:\n\n" ++
+    "    lake exe autograder --local <submission> <file in this project>\n\n" ++
+    "It never leaves the private repository.\n"
    else "")
 
 /-- Writes the generated project to `dest`: the extracted files, plus
diff --git a/DEVIATIONS.md b/DEVIATIONS.md
index 98d384a..100e649 100644
--- a/DEVIATIONS.md
+++ b/DEVIATIONS.md
@@ -61,7 +61,7 @@ The exception: `IntroCS.lean`, described in that chapter's section below.
 Everywhere else, a construct in a code block is one an earlier chapter has
 presented.
 
-This document is the migration plan: which CSwFP sections each `CSwL` chapter consumes, in which order, and what each chapter presupposes. The order below is the book's order; the dependency columns are what justify it. Everything through CSwFP/6 is settled — where a section records a decision, that decision is made, not proposed. What remains is execution, tracked in `TODO.md`. Exercise-level correspondence with CSwFP is in `PROVENANCE.md`.
+This document is the migration plan: which CSwFP sections each `CSwL` chapter consumes, in which order, and what each chapter presupposes. The order below is the book's order; the dependency columns are what justify it. Everything through CSwFP/6 is settled — where a section records a decision, that decision is made, not proposed. What remains is execution, tracked in [GitHub issues](https://github.com/cslib-community/CSwL/issues). Exercise-level correspondence with CSwFP is in `PROVENANCE.md`.
 
 The current state of CSwL need major review to fulfill all decisions from this document.
 
@@ -353,7 +353,7 @@ CSwFP/7 (The Composition of Meaning in Natural Language) goes after `ModelChecki
 
 A proof system as data — CSLib's `Cslib.Logic.PL.Theory.Derivation` — is deferred rather than rejected, for the reasons in the `Logic.lean` section. It becomes attractive exactly where `CSwL` would have something to give back: CSLib has the derivations but no propositional semantics, and this book builds the valuation. Soundness — every derivable sequent is true under every valuation satisfying its context — needs both halves, and neither project has both today. `Cslib/Logics/README.md` invites exactly this ("we are interested in expanding them or creating new ones that can cover your use cases"). Its natural place is after `Sets.lean`, once relations and quantifiers are available. It stays out of the plan until CSwFP/1–6 are in place.
 
-Mathlib's `ContextFreeGrammar` for the grammars of `Games.lean` is deferred on the same footing, and for reasons that are ours rather than the library's — see "Reusing Mathlib and CSLib". It is the one deferred item that would change a chapter already written, so it belongs after the pending work in `TODO.md`, not before it.
+Mathlib's `ContextFreeGrammar` for the grammars of `Games.lean` is deferred on the same footing, and for reasons that are ours rather than the library's — see "Reusing Mathlib and CSLib". It is the one deferred item that would change a chapter already written, so it belongs after the pending work already tracked, not before it.
 
 The related question — whether `PL.lean`'s valuation is written in CSLib's shape from the start — is settled above, and settled against it.
 
diff --git a/README.md b/README.md
index 5026137..7f08e23 100644
--- a/README.md
+++ b/README.md
@@ -66,16 +66,20 @@ exercises not reused later in the chapter itself).
 
 ## Conventions
 
-Mnemonic file names. A short chapter is a single file (`CSwL/Sets.lean`,
-`namespace Sets`); a chapter whose sections are long enough to deserve
-their own file is a "glue" file (`CSwL/Games.lean`) that only gathers, via
-`{include 1 ...}`, sections living in a same-named directory
+Mnemonic file names, never numbers. A short chapter is a single file
+(`CSwL/Sets.lean`, `namespace Sets`); a chapter whose sections are long enough
+to deserve their own file is a "glue" file (`CSwL/Games.lean`) that only
+gathers them, via `{include 1 ...}`, from a same-named directory
 (`CSwL/Games/SeaBattle.lean`, `CSwL/Games/Mastermind.lean`) — the same pattern
-used by [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/). Each content file has its own `namespace`, 
-mnemonic and necessary: the book redefines the same names in different chapters.
+used by [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/).
 
 CSwL developments connect with those in [CSLib](https://github.com/leanprover/cslib/) where possible. We aim to reuse CSLib and contribute to CSLib.
 
+The normative conventions are in [STYLE-CODE.md](STYLE-CODE.md) (Lean and
+Verso, including which Lean feature each chapter is allowed to use) and
+[STYLE-WRITING.md](STYLE-WRITING.md) (prose, pedagogy, and Portuguese).
+[CONTRIBUTING.md](CONTRIBUTING.md) covers workflow.
+
 ## Deviations from CSwFP
 
 `CSwL` is inspired by CSwFP, not a 1-to-1 port of it: chapters get
diff --git a/STYLE-CODE.md b/STYLE-CODE.md
new file mode 100644
index 0000000..6b3a722
--- /dev/null
+++ b/STYLE-CODE.md
@@ -0,0 +1,226 @@
+# CSwL Code Style Guide
+
+This file records the conventions for the Lean code and the Verso markup that
+make up the book. `STYLE-WRITING.md` covers prose, pedagogy, and translation;
+`CONTRIBUTING.md` covers workflow. In case of conflict with `CLAUDE.md`, the
+style guides win on style and `CLAUDE.md` wins on project scope.
+
+The book's prose is in Portuguese. Everything else — this file, identifiers,
+code comments, commit messages — is in English.
+
+## The hard constraint: nothing is used before it is presented
+
+`DEVIATIONS.md` states the rule that governs the whole book:
+
+> **Nothing is used before it is presented.**
+
+In a book whose chapters are largely programs rather than proofs, this covers
+**every Lean feature**, not only tactics: commands, declaration forms, syntax,
+notation, standard-library types, and typeclasses alike. A reader meeting
+`instance` for the first time inside a chapter on morphology has been given a
+feature the book never introduced, exactly as much as one meeting `by_contra`
+would have been.
+
+The table below is the ledger that makes the rule checkable.
+
+### How to read the table
+
+It records the chapter where each feature is **first used in the sources**, in
+book order (`Book.lean`). It is derived from the code inside ```` ```lean ````
+blocks and must be kept in sync as chapters are rewritten.
+
+First use is evidence, not compliance. The rule is about first *presentation* —
+the prose that introduces the feature — and a row whose feature is used but
+never presented is a defect, not an entry. Rows known to be in that state are
+marked, and the open ones are listed under "Known gaps" below.
+
+**A feature can be presented outside a `lean` block**, so the table's first-use
+column does not by itself settle whether the rule holds. `IntroL.lean` presents
+fourteen tactics in a plain code fence — one line each, `rfl` through `funext` —
+and a scan that reads only ```` ```lean ```` blocks misses it. Check the prose
+before recording a gap.
+
+A feature marked **(solution only)** first appears inside a `solution!(…)`
+block. Those rows are a distinct case: the feature is invisible in the
+`student` and `terse` variants and visible in `solutions` and `grading`, so a
+reader working the exercise meets it only in the answer. Introducing a feature
+this way is usually a mistake; see "Known gaps."
+
+### Features by chapter of first use
+
+| Chapter | Commands and declarations | Types and syntax | Tactics |
+| --- | --- | --- | --- |
+| `IntroCS` | `namespace`, `def` (by pattern matching), `inductive`, `deriving Repr`, `example`, `#eval` | `Nat`, function type `→`, dot-notation constructors (`.num`) | `rfl`, `induction … with`, `rw`, `rewrite`, `unfold`, `repeat` |
+| `IntroL` | `#check`, `#print`, `theorem`, `structure`, `instance`, `section`, `variable` | `Type`, `Prop`, `Bool`, `List`, `Option`, `Char`, `String`, `fun`/`λ`, `match`, `if … then … else`, `⟨…⟩`, implicit `{}`, instance-implicit `[]`, `∘`, `BEq`, `∀`, `∃`, `∧`, `∨`, `↔`, `≠` | `intro`, `exact`, `apply`, `cases … with`, `constructor`, `obtain`, `show`, `funext`, `omega`, `decide` (solution only) |
+| `Morphology` | `abbrev`, `open`, `deriving BEq` | `×` | `native_decide` (solution only) |
+| `Games` | — | `DecidableEq`, `Vector`, subtypes (`{ x : T // p x }`), `¬`, `∈` | `simp` (solution only) |
+| `Logic` | `mutual`, `private` | `\|>` | `have`, `use`, `left`, `right`, `rcases`, `by_cases`, `by_contra` |
+| `Sets` | — | `Set`, `Rel`, `Finset`, `Fintype`, `Setoid`, `⊆`, `∪`, `∩` | `assumption`, `trivial`, `symm`, `simp_all` |
+| `InfEngine` | — | `do`-notation | — |
+| `English` | *(none new)* | *(none new)* | *(none new)* |
+
+`English` introduces no new feature: it is where `abbrev` and `ToString`
+instances become the dominant idiom, but both arrive earlier.
+
+`Games` introduces `Vector` and subtypes in `Games/Mastermind.lean`, and the
+subtype gets a paragraph of prose before its first use — the rule working as
+intended.
+
+The table records features, not every piece of notation. Type ascription,
+list literals, projection dots, and the like are not tracked: they arrive with
+the constructs that use them and tracking them would produce a ledger nobody
+maintains.
+
+### Known gaps
+
+Open questions about the table, recorded so they are not lost. Each needs an
+author decision, not a mechanical fix.
+
+- **`native_decide`** (`Morphology/SwedishPlural.lean:69`, `:72`) is used
+  inside solutions and is not in `IntroL`'s tactic table. It closes a goal by
+  compiling and running it, trusting the compiler rather than the kernel — a
+  materially different promise from `decide`. Its use is justified where it
+  appears, and a comment at `:63-66` says why, but that comment is inside the
+  solution and in Portuguese, so the explanation reaches neither the student
+  nor the English code-comment rule.
+- **`trivial`** — one term-level use in `Sets.lean:507`, not presented
+  anywhere. Give it a line or replace it when that chapter is revised.
+
+`IntroCS` is the constraint's one accepted exception: it uses Lean that
+`IntroL` only presents later, deliberately, and the chapter says so where its
+first code block appears — the code is there to show where the book is going,
+nothing in it is presented, and reading it is optional. `DEVIATIONS.md`
+records the decision.
+
+## Verso markup
+
+The book is written in [Verso](https://verso.lean-lang.org), in the `Manual`
+genre. The directives below are defined in `CSwLMeta/` and are the vocabulary
+available to a chapter.
+
+### Chapter structure
+
+A chapter file opens with its imports, the `#doc` declaration, and a metadata
+block:
+
+```
+#doc (Manual) "Title in Portuguese" =>
+%%%
+tag := "ChapterTag"
+htmlSplit := .never
+file := "ChapterTag"
+%%%
+```
+
+Mnemonic names, never numbers — for files, tags, and exercise names alike.
+Material moves between chapters, and a number would be wrong the moment it
+did.
+
+A short chapter is a single file (`CSwL/Sets.lean`). A chapter whose sections
+are long enough to deserve their own files is a "glue" file (`CSwL/Games.lean`)
+that only gathers them via `{include 1 …}` from a same-named directory. Each
+content file has its own `namespace`: the book redefines the same names in
+different chapters, deliberately.
+
+### Exercises and solutions
+
+`:::exercise (rating := N) (name := "mnemonic")` — an exercise. `rating` is
+difficulty, 1 to 5. `name` is the identifier used by `PROVENANCE.md` and by
+the grading variant, and follows the mnemonic rule.
+
+Inside an exercise, the answer is wrapped so the build variants can strip it:
+
+- `solution!(…)` — an inline solution, for a term or a `by` block.
+- `solution!` on its own line, followed by an indented block — a multi-line
+  solution.
+- `:::solution` — a prose solution, for exercises answered in words.
+
+The `student` and `terse` variants replace these with `sorry`; `solutions` and
+`grading` keep them. This is why a feature first used inside `solution!` is
+invisible to the student.
+
+### Grading
+
+`:::gradeTheorem <points> <name> …` marks theorems the autograder scores.
+Points may be a decimal in double quotes (`"0.25"`); an integer needs no
+quotes. The directive is defined in `CSwLMeta/Grade.lean` and emitted as an
+`[autogradedProof]` attribute by `CSwLMeta/Save/Extract.lean`, into the
+`grading` variant only.
+
+The theorems must be `theorem`s and not `example`s, since the attribute needs
+a name to refer to.
+
+### Build variants
+
+Four variants are generated by `make all`, from the same sources:
+
+| Variant | Solutions | Audience |
+| --- | --- | --- |
+| `student` | stripped to `sorry` | the students, published to the book repository |
+| `terse` | stripped to `sorry` | the instructor, opened in VS Code during class |
+| `solutions` | kept | the instructor |
+| `grading` | kept, plus grading attributes | the autograder; never leaves the private repository |
+
+Prose can be routed to a variant:
+
+- `:::full` — appears in the full-prose variants, omitted from `terse`.
+- `:::terse` — appears only in `terse`.
+- `:::suppressPreviousHeaderWhenTerse` — drops the preceding heading in the
+  `terse` build, where the prose under it is gone and the heading would dangle.
+
+### Notes and commentary
+
+- `:::dev` — an internal note to the authors, rendered under the heading
+  "Nota editorial". AI-generated commentary belongs here, and is marked as
+  such.
+
+  It takes an optional author (a string, as `Full Name (github-handle)`), an
+  optional urgency (`NOW`, `BeforeNextRelease` or `PotentialImprovement`, a
+  bare identifier), and an optional `(year := N)`.
+
+  Two filters decide where a note appears, and they are independent:
+
+  - **By variant**, in `Block.devcomment`'s `traverse`: the `student` build
+    drops every note, from the HTML and from the generated `.lean` alike.
+    `terse`, `solutions` and `grading` keep them all — `terse` is the
+    instructor's, so a note on screen during a class is harmless.
+  - **By urgency**, in `devNoteShown`: a `PotentialImprovement` note renders
+    nothing even where it is kept. Notes marked `NOW` or `BeforeNextRelease`,
+    and unmarked ones, render.
+
+  So a dev note never reaches a student, and nothing in one has to be written
+  with a student in mind.
+- `:::quiz` and `:::quizSolution` — a comprehension check.
+- `:::diagramWithAlt` — a diagram with its textual alternative, for
+  accessibility.
+
+### Other blocks
+
+- ```` ```lean ```` — live Lean, elaborated by `lake build`. Everything in the
+  book's code is checked; there are no illustrative-only Lean blocks.
+- ```` ```lean (name := tag) ```` with ```` ```leanOutput tag ```` — code whose
+  output is shown and checked against the block.
+- `{include N Module}` — pulls a section file into its glue chapter at heading
+  depth `N`.
+
+## Lean style
+
+Follow the Mathlib
+[style guide](https://leanprover-community.github.io/contribute/style.html)
+and [naming conventions](https://leanprover-community.github.io/contribute/naming.html),
+except where pedagogy asks otherwise. In particular:
+
+- Types and propositions in `PascalCase` (`Phoneme`, `WellFormed`).
+- Functions and values in `camelCase` (`appendSuffixF`, `surfaceTable`).
+- Theorems in `snake_case` (`defeated_last`), keeping the casing of the
+  definitions they are about (`WellFormed.ne_nil`).
+- Greek letters for type variables (`α`, `β`).
+
+All identifiers and all code comments are in English, including in the code
+the students read.
+
+Prefer `cases … with` and `induction … with`, one alternative per line, over
+goal selectors.
+
+Reuse Mathlib and CSLib where they fit; `DEVIATIONS.md` records where they
+deliberately do not, and why.
diff --git a/STYLE-WRITING.md b/STYLE-WRITING.md
new file mode 100644
index 0000000..5dd3f3a
--- /dev/null
+++ b/STYLE-WRITING.md
@@ -0,0 +1,149 @@
+# CSwL Writing Style Guide
+
+This file records the conventions for the book's prose: pedagogy,
+presentation, and the Portuguese it is written in. `STYLE-CODE.md` covers Lean
+code and Verso markup; `CONTRIBUTING.md` covers workflow.
+
+The book's prose is in Portuguese. This guide, like every other document about
+the project, is in English — the rule is about the medium, not the audience.
+
+## Pedagogical decisions
+
+These are the project's standing decisions about how material is presented.
+
+**Avoid fragmented presentation.** A topic is developed in one place, as far
+as the material allows. This is the reason the book largely reorders its
+source: a presentation that is natural in Lean is not the one the source
+needed.
+
+**Do not present a definition that a later chapter will rephrase under the
+same name.** Namespaces would keep such a pair compiling, but the reader is
+not a compiler and will read the second definition as a correction of the
+first. Exceptions happen; they should be deliberate and visible.
+
+**Never discuss the book's sources or alternatives in the prose.** The reader
+has not read the book this one adapts and does not need to know Haskell. The
+book is self-contained: it never names sections, pages, or exercises of
+another work, and it never explains itself by contrast with one.
+
+`DEVIATIONS.md` draws the line precisely, and that discussion is not repeated
+here: a **technical consequence in Lean** is content, because the reader will
+meet it; an **editorial preference** is meta, and belongs in `DEVIATIONS.md`.
+The test is whether the sentence would still be worth writing if this book had
+no source and no alternatives.
+
+**The course is not about Lean.** Lean is introduced as far as the semantics
+needs it and no further. A feature that earns no work in a later chapter does
+not need a section.
+
+**Exercises should not be load-bearing.** Prefer exercises whose solutions are
+not required by later presentations; a reader who skips one, or gets it wrong,
+should not be locked out of the next chapter.
+
+**Prefer naming a chapter over naming a position.** "O capítulo anterior",
+"mais adiante", "já vimos" are true only of one arrangement, and material
+moves between chapters — that is why nothing in this book is numbered. A
+`{ref "Tag"}[…]` survives a reorder; "the previous chapter" silently becomes
+false.
+
+Where a positional phrase is genuinely the clearest thing to write, it is a
+liability to be repaid: **after moving any chapter or section, sweep for the
+prose the move invalidated.** The search that has caught them so far:
+
+```
+capítulo anterior | capítulos anteriores | próximo capítulo |
+no capítulo seguinte | adiante | mais adiante | já vimos | vimos no | visto no
+```
+
+plus every `{ref "…"}`, whose target still resolves but may now be so far away
+that the sentence around it stops making sense.
+
+## Writing advice
+
+This section adapts the guidance developed for SF-in-Lean, whose exercise-led
+structure this book follows. It is about how to write a section, not about
+what the project has decided.
+
+**Imagine your audience.** What do the students know before this course? They
+arrive by different paths. What do they know *so far in this book*, at the
+point you are writing? Use concepts they have; do not use terms they have not
+met. Do not re-explain what they know well — but do remind them of something
+introduced a while back, because they will have forgotten it.
+
+**Context, Gap, Solution.** Readers want to know why they are reading
+something. They will suspend impatience, but not for long. Three parts: what
+do we want to do, what stops us, what do we do about it.
+
+Two near-misses to watch for. The problem may be stated too big, so the path
+to the solution is long and its rightness is not obvious — break it into
+smaller problems, each with the three parts. Or the solution may not
+obviously match the problem, appearing to do more than was asked — then either
+simplify it or explain the excess.
+
+**Start from something specific the reader knows; work toward the general.**
+You begin on the same page as the reader and make small deltas before the
+bigger leaps. Use good examples, simple before general.
+
+**Minimize complexity.** Ask what would make this simpler. Reuse an example
+rather than introducing a new one. Prefer a multi-step development where the
+concerns separate. Avoid an expert-level solution that solves problems you do
+not want to explain yet.
+
+**Do not forget exercises.** This book's signature is that each interesting
+concept comes with something to do. An explanation plus an example can often
+become an explanation plus an exercise.
+
+**Cutting is good.** Material grows and the temptation is to keep everything.
+Ask: does this serve the goal, does the audience need it? If some readers
+would benefit but not all, a `:::details` block or an appendix will hold it.
+
+## Portuguese conventions
+
+The book is in Brazilian Portuguese.
+
+Where AI is used to translate, the translation is as literal as the target
+language allows, produced as a draft for a human to revise. Prose is never
+invented, expanded, or restructured on the AI's initiative — see `CLAUDE.md`.
+The failure mode this section guards against is the systematic one: a
+translation that is fluent, plausible, and consistently wrong about a term.
+
+### Terms
+
+The preferred form, then the form to avoid. This list is short on purpose: it
+records decisions actually taken, not a vocabulary invented in advance.
+Prescribing a term the book has never used, against an alternative it has
+never used, is the same failure this section exists to catch. Add an entry
+when a bad translation is found and corrected.
+
+The chapters are already consistent on their main terms — "tática",
+"tipo indutivo", "hipótese de indução", "predicado" — and those need no
+entry until something contradicts them. What the sweep found instead:
+
+- "supor" / "assumir" (in the sense of English *to assume*; the Portuguese
+  verb means *to take on*, and the false friend is the commonest
+  translation error in this material)
+- "avaliar" / "rodar" (for `#eval`)
+
+### Code and prose
+
+Lean identifiers, keywords, and literal values keep their Lean spelling and go
+in code font: write `true` and `false`, not "verdadeiro" and "falso", when the
+term is the Lean value. Use the Portuguese words when the sense is the
+ordinary one — a proposition is *verdadeira*, a `Bool` is `true`.
+
+Keep a term's translation stable across the whole book. A concept that
+acquires a second name in a later chapter reads as a second concept.
+
+### Punctuation and typography
+
+- Em dashes for parenthetical breaks, spaced as the surrounding prose does.
+- Portuguese quotation marks or straight quotes, consistently within a file.
+- Lean code in prose always in code font, never italicized.
+- Every sentence starts with a capital letter. If a sentence would open with a
+  lowercase Lean identifier, rephrase it — `Nat.add` may open a sentence,
+  `omega` may not.
+
+## Informal proofs
+
+The book uses informal proofs sparingly: to teach a reasoning principle in the
+abstract, as opposed to a Lean tactic. When one appears, it ends with *QED*.