diff --git a/bookspec/Cargo.lock b/bookspec/Cargo.lock
index 059cda3..6f77824 100644
--- a/bookspec/Cargo.lock
+++ b/bookspec/Cargo.lock
@@ -34,6 +34,16 @@ dependencies = [
  "toml",
 ]
 
+[[package]]
+name = "bookspec-gnucash"
+version = "0.1.0"
+dependencies = [
+ "bookspec-checker",
+ "bookspec-runner",
+ "rust_decimal",
+ "serde_json",
+]
+
 [[package]]
 name = "bookspec-runner"
 version = "0.1.0"
diff --git a/bookspec/Cargo.toml b/bookspec/Cargo.toml
index c8c0410..78db5ec 100644
--- a/bookspec/Cargo.toml
+++ b/bookspec/Cargo.toml
@@ -3,7 +3,7 @@
 # repository (P13 step 6, D-34).
 [workspace]
 resolver = "2"
-members = ["checker", "runner"]
+members = ["checker", "runner", "gnucash"]
 
 [workspace.package]
 edition = "2024"
diff --git a/bookspec/README.md b/bookspec/README.md
index f1a6398..9510900 100644
--- a/bookspec/README.md
+++ b/bookspec/README.md
@@ -421,6 +421,16 @@ the 1st, among others) and `untagged_control_line` (a hand line on a
 receivables or payables control account, which only a document may post
 to: rules.md B-38's control guard).
 
+The refusals of the ledger's own laws (BS-entry, BS-ledger, BS-period)
+are spelled `unbalanced` (debits differ from credits), `too_few_lines`,
+`negative_amount` and `zero_amount` (BS-entry-2), `finer_than_minor_unit`
+(an amount finer than the currency's smallest unit, BS-ledger-1),
+`parent_type_mismatch` (a child account of another type than its parent,
+BS-ledger-2), `already_reversed` (BS-ledger-6) and `period_closed` (an
+entry dated inside a closed period, BS-period-2). A refused entry may
+carry the amount the books refuse (zero or negative, in the amount's
+exact decimal spelling); an accepted one carries a positive amount.
+
 `cash_flow` (rules.md B-14): the statement of cash flows for `[from, to]`.
 
 | key | the value |
@@ -453,6 +463,68 @@ event taken or refused as it says, on the books' own store. Each query is
 then checked by the crate that answers it (the table above), so the shape
 never rots either.
 
+## The specification, the laws, the checks (P13 steps 4 and 5)
+
+- `spec/` is the specification text: `00-model.md` (definitions, the
+  model, the five laws, how an example is checked) and one file per area
+  (`entry.md`, `ledger.md`, ... `format.md`), each rule a section with its
+  status, its MUST/MUST NOT/MAY statement, its sources (a vendored source
+  with a verbatim pin, or an exact external reference), its symbolic form,
+  its examples by id and its applicability. `spec/rules-index.md` is the
+  table from `docs/spec/rules.md`'s B-1 to B-45. The checker's
+  `tests/spec.rs` fails the build when a rule lacks its section, a
+  statement lacks MUST/SHOULD/MAY, a pin is not verbatim in its vendored
+  source, a rule's examples differ from the catalogue's, or the edition
+  passes 60 pages.
+- `lean/` is the five laws as Lean theorems (`Bookspec.law_*`), ported
+  from `verify/lean`; `lake build` in that directory builds them and
+  `lake env lean Audit.lean` prints their axioms, which the checker's
+  `tests/lean.rs` requires to be only `propext`, `Quot.sound` and
+  `Classical.choice`.
+- The checker derives expected figures itself (`checker/src/derive.rs`):
+  an engine-free reference model with exact decimals replays an example's
+  entries, reversals, close, bills and invoices and computes its
+  `trial_balance`, `balances`, `profit_and_loss` and `entry` figures from
+  the rules' symbolic forms, and checks that each refusal the example
+  expects is justified by its rule. An example whose figure disagrees
+  fails `checker/tests/derive.rs`, before any engine is consulted. What
+  the model does not cover is reported as skipped, never passed.
+- `gnucash/` is the second engine: GnuCash 5.10 in the oracle container
+  (`just oracle` builds it), driven through `oracle/gnucash/books.py`.
+  `cargo test -p bookspec-gnucash -- --ignored` runs it (it needs
+  Docker). It claims the rules whose examples ask only for balances and
+  passes `BS-entry-3`, `BS-ledger-3`, `BS-statement-1` and
+  `BS-statement-2`.
+
+### GnuCash, the second engine: where it differs
+
+GnuCash is a cross-check, never the authority (`docs/oracle.md`, "Who is
+right"). It differs from three examples, each settled from the sources
+and pinned by `gnucash/tests/gnucash.rs`:
+
+- **`entry-an-unbalanced-entry-is-refused`.** GnuCash accepts debits of
+  100.00 against credits of 90.00 and parks the ten dollars in an
+  `Imbalance-USD` account of its own making; the accounts it lists no
+  longer net to zero. BS-entry-1 (Pacioli ch. 36; IRS Pub. 583: "the
+  total debits must equal the total credits") says such an entry is
+  refused. The example stands; GnuCash records a difference, flagged for
+  the user to repair, instead of refusing it.
+- **`entry-a-line-amount-is-positive`.** GnuCash takes a credit of
+  minus 100.00 as a debit of 100.00, both lines debits, and parks 200.00
+  in the Imbalance account. BS-entry-2 is a CONVENTION (no authority
+  forbids a negative amount); the example stands as the convention the
+  specification chose, and GnuCash's reading is the very ambiguity the
+  convention removes.
+- **`ledger-a-fraction-of-a-cent-is-refused`.** GnuCash rounds 10.005 to
+  10.01 silently. BS-ledger-1 is a CHOICE (the owner, 2026-10-13, found
+  by the first GnuCash cross-check): the books never round silently. An
+  engine's pick is its own; GnuCash's is the other option, recorded.
+
+The example `ledger-a-mistake-is-reversed-never-erased` and the others
+that need an engine's own reversal link or entry query are not claimed by
+the GnuCash adapter: GnuCash has no reversal link, so it cannot answer
+`already_reversed`.
+
 ## Licence and sources
 
 The examples state rules in their own words with the paragraph cited
diff --git a/bookspec/checker/src/derive.rs b/bookspec/checker/src/derive.rs
new file mode 100644
index 0000000..ade3974
--- /dev/null
+++ b/bookspec/checker/src/derive.rs
@@ -0,0 +1,680 @@
+//! The specification's own checker (`plan/served.md` P13 step 5):
+//! every example's expected figures derived from its rule's symbolic
+//! form, by an engine-free reference model with exact decimals.
+//!
+//! The runner asks an *engine* whether it agrees with an example. This
+//! module asks whether the *example* agrees with the specification: it
+//! replays the example's events on the smallest ledger the rules of
+//! `bookspec/spec/*.md` describe (entries, reversals, a close, a bill, an
+//! invoice) and computes each expectation it can from the symbolic forms
+//! (`sum` of signed values, normal balances, the accounting equation,
+//! net income). An expectation whose figure disagrees with the
+//! derivation, or an event whose refusal the rules do not justify, fails
+//! the specification's build, before any engine is consulted.
+//!
+//! What the model does not cover (depreciation, schedules, members,
+//! 1099s, formats, the cash-flow sections) is not derived here: an
+//! expectation is [`Derived::Skipped`] with the reason, never silently
+//! passed, and the example is still checked by the engines.
+
+use std::collections::BTreeMap;
+use std::str::FromStr;
+
+use chrono::NaiveDate;
+use rust_decimal::Decimal;
+
+use crate::engine::RuleId;
+use crate::rules::Area;
+use crate::schema::{Event, Example, Expect, Values};
+
+/// What the derivation found of one expectation or event.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Derived {
+    /// The specification derives the example's figures, and they agree.
+    Agrees {
+        /// The rule whose symbolic form derived them.
+        rule: RuleId,
+    },
+    /// The specification derives different figures, or does not justify
+    /// a refusal: the example is wrong.
+    Disagrees {
+        /// The rule whose symbolic form was applied.
+        rule: RuleId,
+        /// What differs, in words.
+        why: String,
+    },
+    /// The reference model does not cover it.
+    Skipped {
+        /// Why not.
+        why: String,
+    },
+}
+
+/// The derivation of one example: one result per event that was refused
+/// and per expectation.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Derivation {
+    /// The example's id.
+    pub example: String,
+    /// What was derived, in the order met.
+    pub results: Vec<(String, Derived)>,
+}
+
+impl Derivation {
+    /// The disagreements, each as a sentence.
+    pub fn disagreements(&self) -> Vec<String> {
+        self.results
+            .iter()
+            .filter_map(|(what, d)| match d {
+                Derived::Disagrees { rule, why } => {
+                    Some(format!("{}: {what}: {why} ({rule})", self.example))
+                }
+                _ => None,
+            })
+            .collect()
+    }
+
+    /// How many results agree.
+    pub fn agreed(&self) -> usize {
+        self.results
+            .iter()
+            .filter(|(_, d)| matches!(d, Derived::Agrees { .. }))
+            .count()
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+enum Side {
+    Debit,
+    Credit,
+}
+
+#[derive(Clone, Debug)]
+struct Line {
+    account: String,
+    side: Side,
+    amount: Decimal,
+}
+
+#[derive(Clone, Debug)]
+struct Posted {
+    date: NaiveDate,
+    lines: Vec<Line>,
+    closing: bool,
+    reversed: bool,
+}
+
+/// The reference model: posted entries, the closed periods, the types.
+struct Model {
+    types: BTreeMap<String, String>,
+    entries: Vec<Posted>,
+    /// Event number (from 1) to the entry it posted.
+    event_entry: BTreeMap<usize, usize>,
+    closed_through: Vec<NaiveDate>,
+    minor_digits: u32,
+}
+
+fn sign(side: Side) -> Decimal {
+    match side {
+        Side::Debit => Decimal::ONE,
+        Side::Credit => -Decimal::ONE,
+    }
+}
+
+fn dec(s: &str) -> Option<Decimal> {
+    Decimal::from_str(s).ok()
+}
+
+fn date(s: &str) -> Option<NaiveDate> {
+    NaiveDate::parse_from_str(s, "%Y-%m-%d").ok()
+}
+
+fn rule(area: Area, n: u32) -> RuleId {
+    RuleId::new(area, n)
+}
+
+/// The accounts the books create for a document or a close, with their
+/// types (rules.md B-23's default roles).
+fn role_type(code: &str) -> Option<&'static str> {
+    match code {
+        "1200" => Some("asset"),
+        "2000" => Some("liability"),
+        "3999" => Some("equity"),
+        "4000" => Some("revenue"),
+        "6999" => Some("expense"),
+        _ => None,
+    }
+}
+
+impl Model {
+    fn new(ex: &Example) -> Self {
+        let mut types: BTreeMap<String, String> = ex
+            .setup
+            .accounts
+            .iter()
+            .map(|a| (a.code.clone(), a.kind.clone()))
+            .collect();
+        for code in ["1200", "2000", "3999", "4000", "6999"] {
+            types
+                .entry(code.to_string())
+                .or_insert_with(|| role_type(code).unwrap().to_string());
+        }
+        // ISO 4217: the currency's minor-unit digits (two unless listed).
+        let minor_digits = match ex.setup.currency.as_str() {
+            "JPY" | "KRW" | "VND" | "CLP" | "ISK" => 0,
+            "BHD" | "KWD" | "OMR" | "JOD" => 3,
+            _ => 2,
+        };
+        Self {
+            types,
+            entries: Vec::new(),
+            event_entry: BTreeMap::new(),
+            closed_through: Vec::new(),
+            minor_digits,
+        }
+    }
+
+    /// Signed sum of an account's lines dated on or before `through`
+    /// (debit positive), counting entries that stand as written: the
+    /// reversal is its own entry, so the original is always counted.
+    fn signed(
+        &self,
+        code: &str,
+        from: Option<NaiveDate>,
+        through: NaiveDate,
+        closings: bool,
+    ) -> Decimal {
+        self.entries
+            .iter()
+            .filter(|e| {
+                e.date <= through && from.is_none_or(|f| e.date >= f) && (closings || !e.closing)
+            })
+            .flat_map(|e| e.lines.iter())
+            .filter(|l| l.account == code)
+            .map(|l| sign(l.side) * l.amount)
+            .sum()
+    }
+
+    fn is_debit_normal(&self, code: &str) -> bool {
+        matches!(
+            self.types.get(code).map(String::as_str),
+            Some("asset") | Some("expense")
+        )
+    }
+
+    fn on_normal_side(&self, code: &str, signed: Decimal) -> Decimal {
+        if self.is_debit_normal(code) {
+            signed
+        } else {
+            -signed
+        }
+    }
+
+    /// Why the rules refuse this entry, if they do: (reason, rule).
+    fn refusal_justified(&self, e: &Event, reason: &str) -> Result<RuleId, String> {
+        let on = |side: &str| -> Vec<Decimal> {
+            e.lines
+                .iter()
+                .filter(|l| l.side == side)
+                .filter_map(|l| dec(&l.amount))
+                .collect()
+        };
+        let d: Decimal = on("debit").into_iter().sum();
+        let c: Decimal = on("credit").into_iter().sum();
+        let amounts: Vec<Decimal> = e.lines.iter().filter_map(|l| dec(&l.amount)).collect();
+        match reason {
+            "unbalanced" if d != c => Ok(rule(Area::Entry, 1)),
+            "unbalanced" => Err(format!("debits {d} equal credits {c}")),
+            "too_few_lines" if e.lines.len() < 2 => Ok(rule(Area::Entry, 1)),
+            "negative_amount" if amounts.iter().any(|a| *a < Decimal::ZERO) => {
+                Ok(rule(Area::Entry, 2))
+            }
+            "zero_amount" if amounts.iter().any(|a| a.is_zero()) => Ok(rule(Area::Entry, 2)),
+            "finer_than_minor_unit"
+                if amounts
+                    .iter()
+                    .any(|a| a.normalize().scale() > self.minor_digits) =>
+            {
+                Ok(rule(Area::Ledger, 1))
+            }
+            "period_closed" => {
+                let day = e.date.as_deref().and_then(date).ok_or("no date")?;
+                if self.closed_through.iter().any(|end| day <= *end) {
+                    Ok(rule(Area::Period, 2))
+                } else {
+                    Err(format!("{day} is in no closed period"))
+                }
+            }
+            "already_reversed" => {
+                let of = e.reverses.ok_or("no reversal named")?;
+                let idx = self.event_entry.get(&of).ok_or("names no entry")?;
+                if self.entries[*idx].reversed {
+                    Ok(rule(Area::Ledger, 6))
+                } else {
+                    Err(format!("event {of} was not yet reversed"))
+                }
+            }
+            other => Err(format!("{other:?} is not derived by the reference model")),
+        }
+    }
+
+    /// Post an accepted event; `Err` says what the model cannot post.
+    fn post(&mut self, n: usize, e: &Event) -> Result<(), String> {
+        let day = e.date.as_deref().and_then(date);
+        let lines = |ls: &[crate::schema::LineSpec]| -> Option<Vec<Line>> {
+            ls.iter()
+                .map(|l| {
+                    Some(Line {
+                        account: l.account.clone(),
+                        side: if l.side == "debit" {
+                            Side::Debit
+                        } else {
+                            Side::Credit
+                        },
+                        amount: dec(&l.amount)?,
+                    })
+                })
+                .collect()
+        };
+        let posted = if !e.lines.is_empty() {
+            Posted {
+                date: day.ok_or("undated")?,
+                lines: lines(&e.lines).ok_or("an unreadable amount")?,
+                closing: false,
+                reversed: false,
+            }
+        } else if let Some(of) = e.reverses {
+            let idx = *self
+                .event_entry
+                .get(&of)
+                .ok_or("reverses an event that posted nothing")?;
+            let original = self.entries[idx].clone();
+            self.entries[idx].reversed = true;
+            Posted {
+                date: day.ok_or("undated")?,
+                lines: original
+                    .lines
+                    .iter()
+                    .map(|l| Line {
+                        account: l.account.clone(),
+                        side: match l.side {
+                            Side::Debit => Side::Credit,
+                            Side::Credit => Side::Debit,
+                        },
+                        amount: l.amount,
+                    })
+                    .collect(),
+                closing: false,
+                reversed: false,
+            }
+        } else if let Some(b) = &e.bill {
+            let total = document_total(
+                b.amount.as_deref(),
+                &b.lines.iter().map(|l| l.amount.clone()).collect::<Vec<_>>(),
+            )?;
+            if b.lines.iter().any(|l| l.project.is_some()) {
+                return Err("project tags are not modelled".into());
+            }
+            Posted {
+                date: day.ok_or("undated")?,
+                lines: vec![
+                    Line {
+                        account: "6999".into(),
+                        side: Side::Debit,
+                        amount: total,
+                    },
+                    Line {
+                        account: "2000".into(),
+                        side: Side::Credit,
+                        amount: total,
+                    },
+                ],
+                closing: false,
+                reversed: false,
+            }
+        } else if let Some(i) = &e.invoice {
+            let total = document_total(
+                i.amount.as_deref(),
+                &i.lines.iter().map(|l| l.amount.clone()).collect::<Vec<_>>(),
+            )?;
+            if i.lines.iter().any(|l| l.project.is_some()) {
+                return Err("project tags are not modelled".into());
+            }
+            Posted {
+                date: day.ok_or("undated")?,
+                lines: vec![
+                    Line {
+                        account: "1200".into(),
+                        side: Side::Debit,
+                        amount: total,
+                    },
+                    Line {
+                        account: "4000".into(),
+                        side: Side::Credit,
+                        amount: total,
+                    },
+                ],
+                closing: false,
+                reversed: false,
+            }
+        } else if let Some(c) = &e.close {
+            if c.to != "retained_earnings" {
+                return Err("a close to the members is not modelled".into());
+            }
+            let end = day.ok_or("undated")?;
+            let mut out = Vec::new();
+            let mut net = Decimal::ZERO;
+            let codes: Vec<String> = self.types.keys().cloned().collect();
+            for code in codes {
+                let ty = self.types[&code].as_str();
+                if ty != "revenue" && ty != "expense" {
+                    continue;
+                }
+                let s = self.signed(&code, None, end, true);
+                if s.is_zero() {
+                    continue;
+                }
+                net -= s; // net income is credit-normal: revenue - expense
+                out.push(Line {
+                    account: code,
+                    side: if s > Decimal::ZERO {
+                        Side::Credit
+                    } else {
+                        Side::Debit
+                    },
+                    amount: s.abs(),
+                });
+            }
+            if !net.is_zero() {
+                out.push(Line {
+                    account: "3999".into(),
+                    side: if net > Decimal::ZERO {
+                        Side::Credit
+                    } else {
+                        Side::Debit
+                    },
+                    amount: net.abs(),
+                });
+            }
+            self.closed_through.push(end);
+            Posted {
+                date: end,
+                lines: out,
+                closing: true,
+                reversed: false,
+            }
+        } else {
+            return Err("an event the reference model does not post".into());
+        };
+        // The symbolic form of BS-entry-1: what is posted balances.
+        let (d, c): (Decimal, Decimal) =
+            posted
+                .lines
+                .iter()
+                .fold((Decimal::ZERO, Decimal::ZERO), |(d, c), l| match l.side {
+                    Side::Debit => (d + l.amount, c),
+                    Side::Credit => (d, c + l.amount),
+                });
+        if d != c {
+            return Err(format!(
+                "the example posts an unbalanced entry (debits {d}, credits {c})"
+            ));
+        }
+        self.entries.push(posted);
+        self.event_entry.insert(n, self.entries.len() - 1);
+        Ok(())
+    }
+}
+
+fn document_total(amount: Option<&str>, lines: &[String]) -> Result<Decimal, String> {
+    match amount {
+        Some(a) => dec(a).ok_or_else(|| "an unreadable amount".into()),
+        None => lines
+            .iter()
+            .map(|l| dec(l).ok_or_else(|| "an unreadable amount".to_string()))
+            .sum(),
+    }
+}
+
+/// Derive what the specification says about `ex`.
+pub fn derive(ex: &Example) -> Derivation {
+    let mut results = Vec::new();
+    let mut model = Model::new(ex);
+    // The expectations asked after event N are checked right after it; the
+    // rest at the end. The model keeps one state per point, so replay.
+    let mut usable = true;
+    let mut why_not = String::new();
+    let unsupported_setup = !ex.setup.assets.is_empty()
+        || !ex.setup.schedules.is_empty()
+        || !ex.setup.fixed_assets.is_empty()
+        || !ex.setup.members.is_empty();
+    if unsupported_setup {
+        usable = false;
+        why_not = "the setup holds assets, schedules or members, which the reference model does not carry".into();
+    }
+    for (i, e) in ex.events.iter().enumerate() {
+        let n = i + 1;
+        if usable {
+            match &e.refused {
+                Some(reason) => match model.refusal_justified(e, reason) {
+                    Ok(rule) => results.push((
+                        format!("event {n} refused {reason}"),
+                        Derived::Agrees { rule },
+                    )),
+                    Err(why) => results.push((
+                        format!("event {n} refused {reason}"),
+                        if why.contains("not derived") {
+                            Derived::Skipped { why }
+                        } else {
+                            Derived::Disagrees {
+                                rule: rule(Area::Entry, 1),
+                                why,
+                            }
+                        },
+                    )),
+                },
+                None => {
+                    if let Err(why) = model.post(n, e) {
+                        usable = false;
+                        why_not = format!("event {n}: {why}");
+                    }
+                }
+            }
+        }
+        for x in ex.expect.iter().filter(|x| x.after == Some(n)) {
+            results.push(expectation(&model, x, usable, &why_not));
+        }
+    }
+    for x in ex.expect.iter().filter(|x| x.after.is_none()) {
+        results.push(expectation(&model, x, usable, &why_not));
+    }
+    Derivation {
+        example: ex.id.clone(),
+        results,
+    }
+}
+
+fn expectation(model: &Model, x: &Expect, usable: bool, why_not: &str) -> (String, Derived) {
+    let what = format!(
+        "{} {}",
+        x.query,
+        x.as_of.as_deref().or(x.to.as_deref()).unwrap_or("")
+    );
+    if !usable {
+        return (
+            what,
+            Derived::Skipped {
+                why: why_not.to_string(),
+            },
+        );
+    }
+    let Some(Values::Figures(want)) = &x.values else {
+        return (
+            what,
+            Derived::Skipped {
+                why: "no figures to derive".into(),
+            },
+        );
+    };
+    let derived = match x.query.as_str() {
+        "trial_balance" => x.as_of.as_deref().and_then(date).map(|d| {
+            (
+                rule(Area::Statement, 1),
+                want.keys()
+                    .map(|k| (k.clone(), model.signed(k, None, d, true)))
+                    .collect::<Vec<_>>(),
+            )
+        }),
+        "balances" => x.as_of.as_deref().and_then(date).map(|d| {
+            (
+                rule(Area::Ledger, 3),
+                want.keys()
+                    .map(|k| {
+                        (
+                            k.clone(),
+                            model.on_normal_side(k, model.signed(k, None, d, true)),
+                        )
+                    })
+                    .collect(),
+            )
+        }),
+        "profit_and_loss" => {
+            let from = x.from.as_deref().and_then(date);
+            let to = x.to.as_deref().and_then(date);
+            from.zip(to).map(|(f, t)| {
+                let mut figs = Vec::new();
+                for k in want.keys() {
+                    if k == "net_income" {
+                        let mut net = Decimal::ZERO;
+                        for (code, ty) in &model.types {
+                            if ty == "revenue" || ty == "expense" {
+                                net += model
+                                    .on_normal_side(code, model.signed(code, Some(f), t, false))
+                                    * if ty == "revenue" {
+                                        Decimal::ONE
+                                    } else {
+                                        -Decimal::ONE
+                                    };
+                            }
+                        }
+                        figs.push((k.clone(), net));
+                    } else {
+                        figs.push((
+                            k.clone(),
+                            model.on_normal_side(k, model.signed(k, Some(f), t, false)),
+                        ));
+                    }
+                }
+                (rule(Area::Statement, 3), figs)
+            })
+        }
+        "entry" => x.entry.and_then(|n| model.event_entry.get(&n)).map(|idx| {
+            let e = &model.entries[*idx];
+            let figs = want
+                .keys()
+                .map(|k| {
+                    let (code, side) = k.split_once('.').unwrap_or((k, ""));
+                    let v: Decimal = e
+                        .lines
+                        .iter()
+                        .filter(|l| {
+                            l.account == code
+                                && matches!(
+                                    (side, l.side),
+                                    ("debit", Side::Debit) | ("credit", Side::Credit)
+                                )
+                        })
+                        .map(|l| l.amount)
+                        .sum();
+                    (k.clone(), v)
+                })
+                .collect();
+            (rule(Area::Ledger, 4), figs)
+        }),
+        other => {
+            return (
+                what,
+                Derived::Skipped {
+                    why: format!("{other} is not derived by the reference model"),
+                },
+            );
+        }
+    };
+    let Some((rule, figs)) = derived else {
+        return (
+            what,
+            Derived::Skipped {
+                why: "an undated or unresolved query".into(),
+            },
+        );
+    };
+    for (k, got) in figs {
+        match want.get(&k).and_then(|w| dec(w)) {
+            Some(w) if w == got => {}
+            Some(w) => {
+                return (
+                    what,
+                    Derived::Disagrees {
+                        rule,
+                        why: format!("{k}: the example says {w}, the rule derives {got}"),
+                    },
+                );
+            }
+            None => {
+                return (
+                    what,
+                    Derived::Disagrees {
+                        rule,
+                        why: format!("{k}: no exact figure"),
+                    },
+                );
+            }
+        }
+    }
+    // The laws on the whole book, at the day asked: BS-statement-2.
+    if let (true, Some(d)) = (
+        matches!(x.query.as_str(), "trial_balance" | "balances"),
+        x.as_of.as_deref().and_then(date),
+    ) {
+        let (mut a, mut l, mut e, mut r, mut xp) = (
+            Decimal::ZERO,
+            Decimal::ZERO,
+            Decimal::ZERO,
+            Decimal::ZERO,
+            Decimal::ZERO,
+        );
+        let mut net = Decimal::ZERO;
+        for (code, ty) in &model.types {
+            let s = model.signed(code, None, d, true);
+            net += s;
+            let n = model.on_normal_side(code, s);
+            match ty.as_str() {
+                "asset" => a += n,
+                "liability" => l += n,
+                "equity" => e += n,
+                "revenue" => r += n,
+                "expense" => xp += n,
+                _ => {}
+            }
+        }
+        if !net.is_zero() {
+            return (
+                what,
+                Derived::Disagrees {
+                    rule: self::rule(Area::Statement, 1),
+                    why: format!("the books do not net to zero ({net})"),
+                },
+            );
+        }
+        if a != l + e + (r - xp) {
+            return (
+                what,
+                Derived::Disagrees {
+                    rule: self::rule(Area::Statement, 2),
+                    why: format!("A {a} != L {l} + E {e} + (R {r} - X {xp})"),
+                },
+            );
+        }
+    }
+    (what, Derived::Agrees { rule })
+}
diff --git a/bookspec/checker/src/lib.rs b/bookspec/checker/src/lib.rs
index 9d398bf..81bbb56 100644
--- a/bookspec/checker/src/lib.rs
+++ b/bookspec/checker/src/lib.rs
@@ -14,10 +14,12 @@
 //! store. That is what lets a second engine (the GnuCash oracle, later) be
 //! checked by the same examples.
 
+pub mod derive;
 pub mod engine;
 pub mod rules;
 pub mod schema;
 
+pub use derive::{Derivation, Derived, derive};
 pub use engine::{Claims, Engine, Refusal, RuleId, RuleIdError, fallback_refusal};
 pub use rules::{Area, Rule, Status, covered_rules, rule, rule_for_id, rule_for_refusal, rules};
 pub use schema::*;
diff --git a/bookspec/checker/src/rules.rs b/bookspec/checker/src/rules.rs
index b2c5275..94087c4 100644
--- a/bookspec/checker/src/rules.rs
+++ b/bookspec/checker/src/rules.rs
@@ -156,6 +156,12 @@ pub fn rule_for_id(id: &RuleId) -> Option<&'static Rule> {
 /// (bookspec/README.md).
 pub fn rule_for_refusal(reason: &str) -> Option<&'static Rule> {
     let b = match reason {
+        "unbalanced" | "too_few_lines" => 1,
+        "negative_amount" | "zero_amount" => 2,
+        "finer_than_minor_unit" => 3,
+        "parent_type_mismatch" => 4,
+        "already_reversed" => 10,
+        "period_closed" => 12,
         "end_before_start" | "start_after_today" => 30,
         "blank" | "unchanged" | "sibling_has_it" | "holds_a_tin" | "not_one_line"
         | "code_taken" => 31,
@@ -211,84 +217,87 @@ const SPEC: Spec = &[
         Area::Entry,
         "Every entry is a double entry: debits equal credits",
         Some(Status::Authority),
-        &[],
+        &[
+            "entry-an-unbalanced-entry-is-refused",
+            "statement-the-books-balance-and-the-equation-holds",
+        ],
     ),
     (
         2,
         Area::Entry,
         "A line's amount is positive; its side gives the direction",
         Some(Status::Convention),
-        &[],
+        &["entry-a-line-amount-is-positive"],
     ),
     (
         3,
         Area::Ledger,
         "One money through the ledger; foreign amounts at the transaction-date rate",
         Some(Status::Authority),
-        &[],
+        &["ledger-a-fraction-of-a-cent-is-refused"],
     ),
     (
         4,
         Area::Ledger,
         "Five elements, closed list",
         Some(Status::Authority),
-        &[],
+        &["ledger-a-child-account-has-its-parents-type"],
     ),
     (
         5,
         Area::Ledger,
         "Normal balances",
         Some(Status::Convention),
-        &[],
+        &["statement-the-books-balance-and-the-equation-holds"],
     ),
     (
         6,
         Area::Statement,
         "The trial balance balances",
         Some(Status::Authority),
-        &[],
+        &["statement-the-books-balance-and-the-equation-holds"],
     ),
     (
         7,
         Area::Statement,
         "The accounting equation",
         Some(Status::Authority),
-        &[],
+        &["statement-the-books-balance-and-the-equation-holds"],
     ),
     (
         8,
         Area::Ledger,
         "Posted is forever: the book is written only forward",
         Some(Status::Authority),
-        &[],
+        &["ledger-a-mistake-is-reversed-never-erased"],
     ),
     (
         9,
         Area::Ledger,
         "A mistake is corrected by an opposite entry, never erased",
         Some(Status::Authority),
-        &[],
+        &["ledger-a-mistake-is-reversed-never-erased"],
     ),
     (
         10,
         Area::Ledger,
         "An entry is reversed at most once; a closing entry never",
         Some(Status::Choice),
-        &[],
+        &["ledger-a-mistake-is-reversed-never-erased"],
     ),
     (
         11,
         Area::Period,
         "Revenue and expenses close into profit and loss, and that into capital",
         Some(Status::Authority),
-        &[],
+        &["period-a-close-sweeps-the-year-into-capital"],
     ),
     (
         12,
         Area::Period,
         "A closed period takes no new postings; periods close in order",
         Some(Status::Convention),
-        &[],
+        &["period-a-close-sweeps-the-year-into-capital"],
     ),
     (
         13,
@@ -316,6 +325,7 @@ const SPEC: Spec = &[
             "cash-flow.reversal-of-a-reversal",
             "cash-flow.reversed-property-contribution",
             "cash-flow.two-member-llc-first-year",
+            "period-a-close-sweeps-the-year-into-capital",
         ],
     ),
     (
@@ -392,7 +402,7 @@ const SPEC: Spec = &[
         Area::Entry,
         "Exact amounts in the books; rounding only on returns",
         Some(Status::Authority),
-        &[],
+        &["entry-cents-add-exactly"],
     ),
     (
         22,
@@ -406,7 +416,7 @@ const SPEC: Spec = &[
         Area::Ledger,
         "Control roles: one account each, of the right kind, moved only when empty",
         Some(Status::Convention),
-        &[],
+        &["arap-hand-control-posting-refused"],
     ),
     (
         24,
@@ -570,8 +580,8 @@ const SPEC: Spec = &[
     (
         44,
         Area::Ledger,
-        "Extraction and dedup (allocated, not yet stated)",
-        None,
+        "Evidence is read from the bytes, never trusted over them; identical files are kept once",
+        Some(Status::Convention),
         &[],
     ),
     (
diff --git a/bookspec/checker/src/schema.rs b/bookspec/checker/src/schema.rs
index ac4c9d7..aa78ab7 100644
--- a/bookspec/checker/src/schema.rs
+++ b/bookspec/checker/src/schema.rs
@@ -1193,7 +1193,9 @@ impl Example {
                 if !matches!(line.side.as_str(), "debit" | "credit") {
                     return Err(what(format!("side {:?}", line.side)));
                 }
-                check_amount(&line.amount, true, &what)?;
+                // A refused entry may carry the amount the books refuse (zero or
+                // negative, B-2); an accepted one carries a positive amount.
+                check_amount(&line.amount, ev.refused.is_none(), &what)?;
                 if let Some(p) = &line.project
                     && !projects.contains(p.as_str())
                 {
diff --git a/bookspec/checker/tests/derive.rs b/bookspec/checker/tests/derive.rs
new file mode 100644
index 0000000..7a80016
--- /dev/null
+++ b/bookspec/checker/tests/derive.rs
@@ -0,0 +1,107 @@
+//! The specification's own checker: every example's expected figures are
+//! derived from its rules' symbolic forms, engine-free (P13 step 5).
+
+use std::path::{Path, PathBuf};
+
+use bookspec_checker::{Derived, Example, derive};
+
+fn examples() -> Vec<Example> {
+    let dir = Path::new(env!("CARGO_MANIFEST_DIR")).join("../examples");
+    let mut files: Vec<PathBuf> = std::fs::read_dir(dir)
+        .unwrap()
+        .map(|e| e.unwrap().path())
+        .filter(|p| p.extension().is_some_and(|x| x == "toml"))
+        .collect();
+    files.sort();
+    files
+        .iter()
+        .map(|f| Example::from_toml(&std::fs::read_to_string(f).unwrap()).unwrap())
+        .collect()
+}
+
+/// No example's figure disagrees with what its rule derives.
+#[test]
+fn no_example_disagrees_with_its_derivation() {
+    let mut bad = Vec::new();
+    let mut agreed = 0;
+    for ex in examples() {
+        let d = derive(&ex);
+        bad.extend(d.disagreements());
+        agreed += d.agreed();
+    }
+    assert!(
+        bad.is_empty(),
+        "the examples and the rules disagree:\n{}",
+        bad.join("\n")
+    );
+    assert!(
+        agreed >= 30,
+        "the reference model derived only {agreed} results"
+    );
+}
+
+/// The nine examples written for the ledger's own laws are derived in
+/// full: not one of their results is skipped.
+#[test]
+fn the_law_examples_are_derived_in_full() {
+    for id in [
+        "entry-an-unbalanced-entry-is-refused",
+        "entry-a-line-amount-is-positive",
+        "ledger-a-fraction-of-a-cent-is-refused",
+        "statement-the-books-balance-and-the-equation-holds",
+        "ledger-a-mistake-is-reversed-never-erased",
+        "period-a-close-sweeps-the-year-into-capital",
+        "entry-cents-add-exactly",
+    ] {
+        let ex = examples().into_iter().find(|e| e.id == id).unwrap();
+        let d = derive(&ex);
+        assert!(!d.results.is_empty(), "{id}");
+        for (what, r) in &d.results {
+            assert!(matches!(r, Derived::Agrees { .. }), "{id}: {what}: {r:?}");
+        }
+    }
+}
+
+/// An example whose expectation is wrong fails the specification's build:
+/// the same example with one cent moved is caught, and so is a refusal the
+/// rules do not justify.
+#[test]
+fn a_wrong_expectation_is_caught() {
+    let ex = examples()
+        .into_iter()
+        .find(|e| e.id == "statement-the-books-balance-and-the-equation-holds")
+        .unwrap();
+    let text = std::fs::read_to_string(
+        Path::new(env!("CARGO_MANIFEST_DIR"))
+            .join("../examples/statement-the-books-balance-and-the-equation-holds.toml"),
+    )
+    .unwrap();
+    assert!(derive(&ex).disagreements().is_empty());
+    let wrong = text.replacen("\"1000\" = \"6550.25\"", "\"1000\" = \"6550.26\"", 1);
+    let d = derive(&Example::from_toml(&wrong).unwrap());
+    assert!(
+        d.disagreements().iter().any(|m| m.contains("6550.26")),
+        "{:?}",
+        d.disagreements()
+    );
+    // A refusal the rules do not justify: the entry balances.
+    let ex = examples()
+        .into_iter()
+        .find(|e| e.id == "entry-an-unbalanced-entry-is-refused")
+        .unwrap();
+    let text = std::fs::read_to_string(
+        Path::new(env!("CARGO_MANIFEST_DIR"))
+            .join("../examples/entry-an-unbalanced-entry-is-refused.toml"),
+    )
+    .unwrap();
+    assert!(derive(&ex).disagreements().is_empty());
+    let wrong = text.replacen("amount = \"90.00\"", "amount = \"100.00\"", 1);
+    let d = derive(&Example::from_toml(&wrong).unwrap());
+    assert!(
+        d.disagreements()
+            .iter()
+            .any(|m| m.contains("equal credits")),
+        "{:?}",
+        d.disagreements()
+    );
+}
diff --git a/bookspec/checker/tests/lean.rs b/bookspec/checker/tests/lean.rs
new file mode 100644
index 0000000..78517bc
--- /dev/null
+++ b/bookspec/checker/tests/lean.rs
@@ -0,0 +1,93 @@
+//! The five laws are Lean theorems in `bookspec/lean` (P13 step 4), with
+//! no assumption beyond Lean's standard axioms.
+
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+const LAWS: [&str; 5] = [
+    "law_debits_equal_credits",
+    "law_accounting_equation",
+    "law_trial_balance",
+    "law_net_income_articulates",
+    "law_cash_flow_is_change_in_cash",
+];
+
+fn lean_dir() -> PathBuf {
+    Path::new(env!("CARGO_MANIFEST_DIR")).join("../lean")
+}
+
+/// Every law is stated in `Laws.lean`, audited in `Audit.lean`, and no
+/// file of the library says `sorry`.
+#[test]
+fn the_five_laws_are_stated_and_audited() {
+    let laws = std::fs::read_to_string(lean_dir().join("Bookspec/Laws.lean")).unwrap();
+    let audit = std::fs::read_to_string(lean_dir().join("Audit.lean")).unwrap();
+    for law in LAWS {
+        assert!(laws.contains(&format!("theorem {law}")), "{law} is stated");
+        assert!(
+            audit.contains(&format!("#print axioms {law}")),
+            "{law} is audited"
+        );
+    }
+    for entry in std::fs::read_dir(lean_dir().join("Bookspec")).unwrap() {
+        let path = entry.unwrap().path();
+        let text = std::fs::read_to_string(&path).unwrap();
+        for (i, line) in text.lines().enumerate() {
+            let code = line.split("--").next().unwrap();
+            assert!(
+                !code
+                    .split(|c: char| !c.is_alphanumeric() && c != '_')
+                    .any(|w| w == "sorry"),
+                "{}:{}: sorry",
+                path.display(),
+                i + 1
+            );
+        }
+    }
+}
+
+/// With Lean installed, the library builds and every law depends only on
+/// `propext`, `Quot.sound` and `Classical.choice`. Without it the test
+/// says so and passes: `mise install` provides Lean (`just prove` is
+/// where the machine is known to have it).
+#[test]
+fn the_laws_use_standard_axioms_only() {
+    let built = Command::new("lake")
+        .arg("build")
+        .current_dir(lean_dir())
+        .output();
+    let Ok(built) = built else {
+        eprintln!("lake is not installed: the Lean build is not checked here");
+        return;
+    };
+    assert!(
+        built.status.success(),
+        "lake build:\n{}",
+        String::from_utf8_lossy(&built.stdout)
+    );
+    let out = Command::new("lake")
+        .args(["env", "lean", "Audit.lean"])
+        .current_dir(lean_dir())
+        .output()
+        .unwrap();
+    let text = String::from_utf8_lossy(&out.stdout);
+    assert!(out.status.success(), "audit:\n{text}");
+    for law in LAWS {
+        let line = text
+            .lines()
+            .find(|l| l.contains(&format!("Bookspec.{law}'")))
+            .unwrap_or_else(|| panic!("{law} is not audited:\n{text}"));
+        for axiom in line
+            .split('[')
+            .nth(1)
+            .unwrap()
+            .trim_end_matches(']')
+            .split(", ")
+        {
+            assert!(
+                ["propext", "Quot.sound", "Classical.choice"].contains(&axiom.trim()),
+                "{law}: axiom {axiom}"
+            );
+        }
+    }
+}
diff --git a/bookspec/checker/tests/spec.rs b/bookspec/checker/tests/spec.rs
new file mode 100644
index 0000000..4fdf725
--- /dev/null
+++ b/bookspec/checker/tests/spec.rs
@@ -0,0 +1,261 @@
+//! The specification text (`bookspec/spec/*.md`, P13 step 4): every rule
+//! has its section, its statement, its pinned sources, its symbolic form
+//! and its examples, and every citation resolves.
+
+use std::collections::{BTreeMap, BTreeSet};
+use std::path::{Path, PathBuf};
+
+use bookspec_checker::{Rule, rules};
+
+fn spec_dir() -> PathBuf {
+    Path::new(env!("CARGO_MANIFEST_DIR")).join("../spec")
+}
+
+fn sources_dir() -> PathBuf {
+    Path::new(env!("CARGO_MANIFEST_DIR")).join("../../docs/spec/sources")
+}
+
+/// A rule's section as the text gives it.
+#[derive(Default, Debug)]
+struct Section {
+    file: String,
+    heading: String,
+    fields: BTreeMap<String, Vec<String>>,
+}
+
+/// Every `### BS-...` section of the area files, by its identifier.
+fn sections() -> BTreeMap<String, Section> {
+    let mut out = BTreeMap::new();
+    let mut files: Vec<PathBuf> = std::fs::read_dir(spec_dir())
+        .unwrap()
+        .map(|e| e.unwrap().path())
+        .filter(|p| p.extension().is_some_and(|x| x == "md"))
+        .collect();
+    files.sort();
+    for f in files {
+        let name = f.file_name().unwrap().to_string_lossy().into_owned();
+        let text = std::fs::read_to_string(&f).unwrap();
+        let mut current: Option<(String, Section)> = None;
+        let mut field = String::new();
+        for line in text.lines() {
+            if let Some(h) = line.strip_prefix("### BS-") {
+                if let Some((id, s)) = current.take() {
+                    assert!(out.insert(id.clone(), s).is_none(), "{id} twice");
+                }
+                let id = format!("BS-{}", h.split(':').next().unwrap());
+                current = Some((
+                    id,
+                    Section {
+                        file: name.clone(),
+                        heading: h.to_string(),
+                        ..Section::default()
+                    },
+                ));
+                continue;
+            }
+            let Some((_, s)) = current.as_mut() else {
+                continue;
+            };
+            if let Some(rest) = line.strip_prefix("- **") {
+                let (key, value) = rest.split_once(":**").expect("a field: - **Name:** ...");
+                field = key.to_string();
+                let e = s.fields.entry(field.clone()).or_default();
+                if !value.trim().is_empty() {
+                    e.push(value.trim().to_string());
+                }
+            } else if let Some(item) = line.strip_prefix("  - ") {
+                s.fields
+                    .entry(field.clone())
+                    .or_default()
+                    .push(item.to_string());
+            }
+        }
+        if let Some((id, s)) = current.take() {
+            assert!(out.insert(id.clone(), s).is_none(), "{id} twice");
+        }
+    }
+    out
+}
+
+fn one<'a>(s: &'a Section, id: &str, field: &str) -> &'a str {
+    let v = s
+        .fields
+        .get(field)
+        .unwrap_or_else(|| panic!("{id}: no {field}"));
+    assert_eq!(v.len(), 1, "{id}: {field} is one line");
+    &v[0]
+}
+
+/// Whitespace and typographic quotes made plain, so a pin copied from a
+/// wrapped or curly-quoted source still matches.
+fn squash(s: &str) -> String {
+    let plain = s
+        .replace(['\u{2019}', '\u{2018}'], "'")
+        .replace(['\u{201c}', '\u{201d}'], "\"");
+    plain.split_whitespace().collect::<Vec<_>>().join(" ")
+}
+
+fn backticked(s: &str) -> Vec<&str> {
+    s.split('`').skip(1).step_by(2).collect()
+}
+
+/// Every one of the 45 rules has one section, in the file of its area,
+/// headed with its identifier and B-number.
+#[test]
+fn every_rule_has_its_section() {
+    let sections = sections();
+    assert_eq!(sections.len(), 45, "one section per rule");
+    for rule in rules() {
+        let s = sections
+            .get(rule.id.as_str())
+            .unwrap_or_else(|| panic!("{}: no section", rule.id));
+        assert_eq!(s.file, format!("{}.md", rule.area.key()), "{}", rule.id);
+        assert!(
+            s.heading.ends_with(&format!("(B-{})", rule.b)),
+            "{}: heading {:?} names B-{}",
+            rule.id,
+            s.heading,
+            rule.b
+        );
+    }
+}
+
+/// A stated rule has a status the catalogue agrees with, a normative
+/// statement, a symbolic form and applicability; a reserved one says so.
+#[test]
+fn every_stated_rule_is_complete() {
+    let sections = sections();
+    for rule in rules() {
+        let s = &sections[rule.id.as_str()];
+        let id = rule.id.as_str();
+        let status = one(s, id, "Status");
+        match rule.status {
+            Some(st) => {
+                assert!(status.starts_with(st.key()), "{id}: status {status:?}");
+                let statement = one(s, id, "Statement");
+                assert!(
+                    ["MUST", "SHOULD", "MAY"]
+                        .iter()
+                        .any(|w| statement.contains(w)),
+                    "{id}: a statement says MUST, SHOULD or MAY"
+                );
+                for field in ["Symbolic form", "Applicability"] {
+                    assert!(
+                        one(s, id, field).len() > 10 && !one(s, id, field).starts_with("none"),
+                        "{id}: {field}"
+                    );
+                }
+            }
+            None => assert!(status.starts_with("reserved"), "{id}: reserved"),
+        }
+    }
+}
+
+/// A section's examples are the catalogue's, exactly; "none yet" says why.
+#[test]
+fn the_examples_are_the_catalogues() {
+    let sections = sections();
+    for rule in rules() {
+        let s = &sections[rule.id.as_str()];
+        let id = rule.id.as_str();
+        let line = one(s, id, "Examples");
+        let listed: BTreeSet<&str> = backticked(line)
+            .into_iter()
+            .filter(|b| *b != "none yet")
+            .collect();
+        let want: BTreeSet<&str> = rule.examples.iter().copied().collect();
+        if rule.examples.is_empty() {
+            assert!(line.starts_with("none yet"), "{id}: {line}");
+            if rule.status.is_some() {
+                assert!(
+                    line.len() > "none yet. ".len() + 20,
+                    "{id}: a stated rule with no example says why"
+                );
+            }
+        } else {
+            assert_eq!(listed, want, "{id}: examples");
+        }
+    }
+}
+
+/// Every citation resolves: a vendored source exists, and a verbatim
+/// pin appears in it; an external reference names its paragraph.
+#[test]
+fn every_citation_resolves() {
+    let sections = sections();
+    let mut vendored = 0;
+    let mut external = 0;
+    let mut bad: Vec<String> = Vec::new();
+    for rule in rules() {
+        let s = &sections[rule.id.as_str()];
+        let id = rule.id.as_str();
+        let sources = s
+            .fields
+            .get("Sources")
+            .unwrap_or_else(|| panic!("{id}: no Sources"));
+        if rule.status.is_none() {
+            assert_eq!(sources, &vec!["none yet".to_string()], "{id}");
+            continue;
+        }
+        assert!(!sources.is_empty(), "{id}: sourced");
+        for item in sources {
+            if let Some(rest) = item.strip_prefix("vendored `") {
+                let (file, rest) = rest
+                    .split_once("`:")
+                    .unwrap_or_else(|| panic!("{id}: {item}"));
+                let path = sources_dir().join(file.strip_prefix("sources/").unwrap_or(file));
+                let text = std::fs::read_to_string(&path)
+                    .unwrap_or_else(|_| panic!("{id}: {file} is not vendored"));
+                let hay = squash(&text);
+                // Every quoted pin is verbatim in the file.
+                let quoted: Vec<&str> = rest.split('"').skip(1).step_by(2).collect();
+                for q in &quoted {
+                    if !hay.contains(&squash(q)) {
+                        bad.push(format!("{id}: {q:?} is not in {file}"));
+                    }
+                }
+                if quoted.is_empty() {
+                    bad.push(format!("{id}: {item} has no verbatim pin"));
+                }
+                vendored += 1;
+            } else if let Some(rest) = item.strip_prefix("external:") {
+                assert!(
+                    rest.trim().len() > 20,
+                    "{id}: an external reference is exact: {item}"
+                );
+                external += 1;
+            } else {
+                panic!("{id}: a source is `vendored` or `external`: {item}");
+            }
+        }
+    }
+    assert!(bad.is_empty(), "pins not found:\n{}", bad.join("\n"));
+    assert!(vendored >= 30, "vendored citations: {vendored}");
+    assert!(external >= 15, "external citations: {external}");
+}
+
+/// The first edition's page budget: 60 pages of 55 lines.
+#[test]
+fn the_edition_fits_its_page_budget() {
+    let mut lines = 0;
+    for e in std::fs::read_dir(spec_dir()).unwrap() {
+        let p = e.unwrap().path();
+        if p.extension().is_some_and(|x| x == "md") {
+            lines += std::fs::read_to_string(p).unwrap().lines().count();
+        }
+    }
+    assert!(lines <= 60 * 55, "{lines} lines is over 60 pages");
+}
+
+/// A stated rule with no example is exactly one an engine cannot claim.
+#[test]
+fn rules_without_examples_are_not_claimable() {
+    let uncovered: Vec<&Rule> = rules().iter().filter(|r| !r.has_examples()).collect();
+    let claimable: BTreeSet<_> = bookspec_checker::covered_rules()
+        .into_iter()
+        .map(|r| r.b)
+        .collect();
+    for r in uncovered {
+        assert!(!claimable.contains(&r.b), "B-{}", r.b);
+    }
+}
diff --git a/bookspec/examples/entry-a-line-amount-is-positive.toml b/bookspec/examples/entry-a-line-amount-is-positive.toml
new file mode 100644
index 0000000..f6a8adf
--- /dev/null
+++ b/bookspec/examples/entry-a-line-amount-is-positive.toml
@@ -0,0 +1,75 @@
+id = "entry-a-line-amount-is-positive"
+title = "A negative or zero line amount is refused; the side gives the direction"
+rule = "A line's amount MUST be greater than zero, and its side, not its sign, MUST give the direction money moves; an entry with a negative or zero line MUST be refused."
+status = "CONVENTION"
+sources = [
+  "Pacioli, Summa (1494), ch. 36: debtors at the left, creditors at the right (docs/spec/sources/pacioli-1494.md)",
+  "CONVENTION, the owner, 2026-10-13 (docs/spec/rules.md B-2): no authority forbids a negative amount outright; one reading of every line is chosen",
+]
+tags = ["accrual", "book", "us", "entry"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+[[setup.accounts]]
+code = "3000"
+name = "Capital"
+type = "equity"
+
+[[setup.accounts]]
+code = "4000"
+name = "Sales"
+type = "revenue"
+tax_category = "gross_receipts"
+
+[[setup.accounts]]
+code = "6000"
+name = "Rent"
+type = "expense"
+tax_category = "rent_property"
+
+# A credit of minus 100.00 would be a debit of 100.00 written the other
+# way; the books keep one way to write it.
+[[events]]
+date = "2026-01-05"
+description = "A negative credit"
+refused = "negative_amount"
+lines = [
+  { account = "1000", side = "debit", amount = "100.00" },
+  { account = "4000", side = "credit", amount = "-100.00" },
+]
+
+[[events]]
+date = "2026-01-06"
+description = "A zero line"
+refused = "zero_amount"
+lines = [
+  { account = "1000", side = "debit", amount = "0.00" },
+  { account = "4000", side = "credit", amount = "0.00" },
+]
+
+# The same 100.00 written with the sides doing the work is accepted.
+[[events]]
+date = "2026-01-07"
+description = "A sale"
+lines = [
+  { account = "1000", side = "debit", amount = "100.00" },
+  { account = "4000", side = "credit", amount = "100.00" },
+]
+
+[[expect]]
+query = "trial_balance"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "100.00"
+"3000" = "0.00"
+"4000" = "-100.00"
+"6000" = "0.00"
diff --git a/bookspec/examples/entry-an-unbalanced-entry-is-refused.toml b/bookspec/examples/entry-an-unbalanced-entry-is-refused.toml
new file mode 100644
index 0000000..989baf1
--- /dev/null
+++ b/bookspec/examples/entry-an-unbalanced-entry-is-refused.toml
@@ -0,0 +1,76 @@
+id = "entry-an-unbalanced-entry-is-refused"
+title = "An entry whose debits and credits differ is refused and posts nothing"
+rule = "An entry MUST have debits equal to credits, exactly, and an entry that does not MUST be refused whole, leaving the books as they were."
+status = "AUTHORITY"
+sources = [
+  "Pacioli, Summa (1494), ch. 36: \"All entries made in the ledger have to be double entries\" (docs/spec/sources/pacioli-1494.md)",
+  "IRS Publication 583: \"the total debits must equal the total credits\" (docs/spec/sources/irs-records.md)",
+]
+tags = ["accrual", "book", "us", "entry", "double-entry"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+[[setup.accounts]]
+code = "3000"
+name = "Capital"
+type = "equity"
+
+[[setup.accounts]]
+code = "4000"
+name = "Sales"
+type = "revenue"
+tax_category = "gross_receipts"
+
+[[setup.accounts]]
+code = "6000"
+name = "Rent"
+type = "expense"
+tax_category = "rent_property"
+
+[[events]]
+date = "2026-01-02"
+description = "Opening contribution"
+lines = [
+  { account = "1000", side = "debit", amount = "1000.00" },
+  { account = "3000", side = "credit", amount = "1000.00" },
+]
+
+# Debits 100.00, credits 90.00: ten dollars short on the credit side.
+[[events]]
+date = "2026-01-05"
+description = "A sale that does not balance"
+refused = "unbalanced"
+lines = [
+  { account = "1000", side = "debit", amount = "100.00" },
+  { account = "4000", side = "credit", amount = "90.00" },
+]
+
+# One cent over is just as wrong: there is no epsilon.
+[[events]]
+date = "2026-01-06"
+description = "A sale a cent over"
+refused = "unbalanced"
+lines = [
+  { account = "1000", side = "debit", amount = "100.01" },
+  { account = "4000", side = "credit", amount = "100.00" },
+]
+
+# By hand: only event 1 posted, so cash holds 1,000.00 (a debit), capital
+# 1,000.00 (a credit, shown negative), and sales nothing.
+[[expect]]
+query = "trial_balance"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "1000.00"
+"3000" = "-1000.00"
+"4000" = "0.00"
+"6000" = "0.00"
diff --git a/bookspec/examples/entry-cents-add-exactly.toml b/bookspec/examples/entry-cents-add-exactly.toml
new file mode 100644
index 0000000..09ab2ef
--- /dev/null
+++ b/bookspec/examples/entry-cents-add-exactly.toml
@@ -0,0 +1,68 @@
+id = "entry-cents-add-exactly"
+title = "Amounts are kept exactly: ten cents and twenty cents make thirty"
+rule = "The books MUST keep every amount exactly and add exactly, so that no sum of cents differs from its true total by any amount, however small; rounding MUST NOT occur inside the books."
+status = "AUTHORITY"
+sources = [
+  "IRS Form 1065 instructions: \"include cents when adding the amounts and round off only the total\" (docs/spec/sources/irs-partnerships.md)",
+  "Pacioli, Summa (1494), ch. 36: the credits equal the debits, which no float sum guarantees (docs/spec/sources/pacioli-1494.md)",
+]
+tags = ["accrual", "book", "us", "entry", "exact"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+[[setup.accounts]]
+code = "2000"
+name = "Loan"
+type = "liability"
+
+[[setup.accounts]]
+code = "3000"
+name = "Capital"
+type = "equity"
+
+[[setup.accounts]]
+code = "4000"
+name = "Sales"
+type = "revenue"
+tax_category = "gross_receipts"
+
+[[setup.accounts]]
+code = "6000"
+name = "Rent"
+type = "expense"
+tax_category = "rent_property"
+
+# In binary floating point 0.1 + 0.2 is 0.30000000000000004. Two debits of
+# 0.10 and 0.20 against one credit of 0.30 balance exactly.
+[[events]]
+date = "2026-01-05"
+description = "Three small sales"
+lines = [
+  { account = "1000", side = "debit", amount = "0.10" },
+  { account = "1000", side = "debit", amount = "0.20" },
+  { account = "4000", side = "credit", amount = "0.30" },
+]
+
+[[events]]
+date = "2026-01-06"
+description = "A sale of a trillion and a cent"
+lines = [
+  { account = "1000", side = "debit", amount = "1000000000000.01" },
+  { account = "4000", side = "credit", amount = "1000000000000.01" },
+]
+
+[[expect]]
+query = "balances"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "1000000000000.31"
+"4000" = "1000000000000.31"
diff --git a/bookspec/examples/ledger-a-child-account-has-its-parents-type.toml b/bookspec/examples/ledger-a-child-account-has-its-parents-type.toml
new file mode 100644
index 0000000..c8adcae
--- /dev/null
+++ b/bookspec/examples/ledger-a-child-account-has-its-parents-type.toml
@@ -0,0 +1,55 @@
+events = []
+
+id = "ledger-a-child-account-has-its-parents-type"
+title = "An account under a parent has the parent's type"
+rule = "An account MUST be one of the five elements (asset, liability, equity, revenue, expense), and an account under a parent MUST have its parent's type, so a rollup never mixes elements."
+status = "AUTHORITY"
+sources = [
+  "FASB Concepts Statement 8, Ch. 4, E16, E37, E61, E80, E81: the five elements (docs/spec/sources/fasb-asc.md)",
+  "CHOICE, the owner, 2026-10-13 (docs/spec/rules.md B-4): a child takes its parent's type",
+]
+tags = ["accrual", "book", "us", "ledger", "chart"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "6000"
+name = "Operating"
+type = "expense"
+header = true
+
+[[setup.accounts]]
+code = "6150"
+name = "Software"
+type = "expense"
+parent = "6000"
+tax_category = "office_expense"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+# A revenue account under an expense header would mix two elements.
+[[expect]]
+query = "add_account"
+account = { code = "6200", name = "Refunds", type = "revenue", parent = "6000", tax_category = "gross_receipts" }
+refused = "parent_type_mismatch"
+
+# An expense under the expense header is a child of the same element.
+[[expect]]
+query = "add_account"
+account = { code = "6200", name = "Hosting", type = "expense", parent = "6000", tax_category = "office_expense" }
+accepted = true
+
+[[expect]]
+query = "trial_balance"
+as_of = "2026-12-31"
+[expect.values]
+"6000" = "0.00"
+"6150" = "0.00"
+"1000" = "0.00"
diff --git a/bookspec/examples/ledger-a-fraction-of-a-cent-is-refused.toml b/bookspec/examples/ledger-a-fraction-of-a-cent-is-refused.toml
new file mode 100644
index 0000000..896cd5c
--- /dev/null
+++ b/bookspec/examples/ledger-a-fraction-of-a-cent-is-refused.toml
@@ -0,0 +1,65 @@
+id = "ledger-a-fraction-of-a-cent-is-refused"
+title = "A line finer than the currency's smallest unit is refused"
+rule = "A ledger kept in one currency MUST hold amounts in whole units of that currency's smallest unit, so a line finer than it MUST be refused, never rounded silently."
+status = "CHOICE"
+sources = [
+  "Pacioli, Summa (1494), ch. 36: \"the money that you reckon by at the beginning should be the same all through the Ledger\" (docs/spec/sources/pacioli-1494.md)",
+  "ISO 4217: the US dollar has two minor-unit digits (docs/spec/sources/iso-4217.md)",
+  "CHOICE, the owner, 2026-10-13 (docs/spec/rules.md B-3): books in the smallest unit, so cash can match a bank statement",
+]
+tags = ["accrual", "book", "us", "ledger", "currency"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+[[setup.accounts]]
+code = "3000"
+name = "Capital"
+type = "equity"
+
+[[setup.accounts]]
+code = "4000"
+name = "Sales"
+type = "revenue"
+tax_category = "gross_receipts"
+
+[[setup.accounts]]
+code = "6000"
+name = "Rent"
+type = "expense"
+tax_category = "rent_property"
+
+# 10.005 dollars is no amount anyone can pay.
+[[events]]
+date = "2026-01-05"
+description = "Half a cent too fine"
+refused = "finer_than_minor_unit"
+lines = [
+  { account = "1000", side = "debit", amount = "10.005" },
+  { account = "4000", side = "credit", amount = "10.005" },
+]
+
+[[events]]
+date = "2026-01-06"
+description = "The same sale in cents"
+lines = [
+  { account = "1000", side = "debit", amount = "10.01" },
+  { account = "4000", side = "credit", amount = "10.01" },
+]
+
+[[expect]]
+query = "trial_balance"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "10.01"
+"3000" = "0.00"
+"4000" = "-10.01"
+"6000" = "0.00"
diff --git a/bookspec/examples/ledger-a-mistake-is-reversed-never-erased.toml b/bookspec/examples/ledger-a-mistake-is-reversed-never-erased.toml
new file mode 100644
index 0000000..48caf69
--- /dev/null
+++ b/bookspec/examples/ledger-a-mistake-is-reversed-never-erased.toml
@@ -0,0 +1,101 @@
+id = "ledger-a-mistake-is-reversed-never-erased"
+title = "A reversal cancels an entry and leaves the original standing, and an entry is reversed only once"
+rule = "A posted entry MUST NOT be changed or erased; a mistake MUST be corrected by an entry opposite to it, which MUST leave the original's lines as written, and an entry MUST be reversed at most once."
+status = "AUTHORITY"
+sources = [
+  "Pacioli, Summa (1494), ch. 31: \"make another entry opposite this one\"; ch. 36: \"You should not write backward, but always forward\" (docs/spec/sources/pacioli-1494.md)",
+  "Rev. Proc. 98-25 section 5.01: the audit trail (docs/spec/sources/irs-records.md)",
+  "CHOICE, the owner, 2026-10-13 (docs/spec/rules.md B-10): a correction corrects once",
+]
+tags = ["accrual", "book", "us", "ledger", "reversal"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+[[setup.accounts]]
+code = "2000"
+name = "Loan"
+type = "liability"
+
+[[setup.accounts]]
+code = "3000"
+name = "Capital"
+type = "equity"
+
+[[setup.accounts]]
+code = "4000"
+name = "Sales"
+type = "revenue"
+tax_category = "gross_receipts"
+
+[[setup.accounts]]
+code = "6000"
+name = "Rent"
+type = "expense"
+tax_category = "rent_property"
+
+[[events]]
+date = "2026-01-10"
+description = "Rent paid twice by mistake"
+lines = [
+  { account = "6000", side = "debit", amount = "800.00" },
+  { account = "1000", side = "credit", amount = "800.00" },
+]
+
+[[events]]
+date = "2026-01-12"
+description = "Reverse entry 1"
+reverses = 1
+
+# A second reversal of the same entry would take the 800.00 out twice.
+[[events]]
+date = "2026-01-13"
+description = "Reverse entry 1 again"
+refused = "already_reversed"
+reverses = 1
+
+# The original still reads as it was written: posted is forever.
+[[expect]]
+query = "entry"
+entry = 1
+[expect.values]
+"6000.debit" = "800.00"
+"1000.credit" = "800.00"
+
+# The reversal is the original with its sides flipped.
+[[expect]]
+query = "entry"
+entry = 2
+[expect.values]
+"6000.credit" = "800.00"
+"1000.debit" = "800.00"
+
+# Net of the two, nothing: as if nothing had been written (ch. 31).
+[[expect]]
+query = "trial_balance"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "0.00"
+"2000" = "0.00"
+"3000" = "0.00"
+"4000" = "0.00"
+"6000" = "0.00"
+
+# Before the reversal's date the original stands alone.
+[[expect]]
+query = "trial_balance"
+as_of = "2026-01-11"
+[expect.values]
+"1000" = "-800.00"
+"2000" = "0.00"
+"3000" = "0.00"
+"4000" = "0.00"
+"6000" = "800.00"
diff --git a/bookspec/examples/period-a-close-sweeps-the-year-into-capital.toml b/bookspec/examples/period-a-close-sweeps-the-year-into-capital.toml
new file mode 100644
index 0000000..32a0042
--- /dev/null
+++ b/bookspec/examples/period-a-close-sweeps-the-year-into-capital.toml
@@ -0,0 +1,108 @@
+id = "period-a-close-sweeps-the-year-into-capital"
+title = "A close zeroes revenue and expenses into equity, and the closed period takes no new postings"
+rule = "A close MUST zero every revenue and expense account through its last day and credit equity with exactly the net income; a period once closed MUST take no new postings."
+status = "AUTHORITY"
+sources = [
+  "Pacioli, Summa (1494), ch. 34: \"you shall close this account into the capital account\" (docs/spec/sources/pacioli-1494.md)",
+  "OpenStax, Principles of Accounting, Vol. 1, 5.1: temporary accounts are closed at the end of each period (docs/spec/rules.md B-11)",
+  "CONVENTION (docs/spec/rules.md B-12): a closed period is locked, which follows from posted-is-forever",
+]
+tags = ["accrual", "book", "us", "period", "close"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+[[setup.accounts]]
+code = "2000"
+name = "Loan"
+type = "liability"
+
+[[setup.accounts]]
+code = "3000"
+name = "Capital"
+type = "equity"
+
+[[setup.accounts]]
+code = "4000"
+name = "Sales"
+type = "revenue"
+tax_category = "gross_receipts"
+
+[[setup.accounts]]
+code = "6000"
+name = "Rent"
+type = "expense"
+tax_category = "rent_property"
+
+[[events]]
+date = "2026-01-02"
+description = "Members put in cash"
+lines = [
+  { account = "1000", side = "debit", amount = "5000.00" },
+  { account = "3000", side = "credit", amount = "5000.00" },
+]
+
+[[events]]
+date = "2026-02-10"
+description = "A sale"
+lines = [
+  { account = "1000", side = "debit", amount = "900.00" },
+  { account = "4000", side = "credit", amount = "900.00" },
+]
+
+[[events]]
+date = "2026-03-10"
+description = "Rent"
+lines = [
+  { account = "6000", side = "debit", amount = "350.00" },
+  { account = "1000", side = "credit", amount = "350.00" },
+]
+
+# Close January 1 through March 31 into capital.
+[[events]]
+date = "2026-03-31"
+description = "Close the quarter"
+close = { start = "2026-01-01", to = "retained_earnings" }
+
+# March 31 is closed: an entry dated inside the quarter is refused.
+[[events]]
+date = "2026-03-15"
+description = "A late sale"
+refused = "period_closed"
+lines = [
+  { account = "1000", side = "debit", amount = "50.00" },
+  { account = "4000", side = "credit", amount = "50.00" },
+]
+
+# By hand: net income = 900.00 - 350.00 = 550.00. Revenue and expense are
+# zero; the 550.00 lands in Retained Earnings (3999, the account the books
+# create for the close), so equity is 5000.00 + 550.00 = 5550.00; cash is
+# 5000 + 900 - 350 = 5550.00, so assets equal equity.
+[[expect]]
+query = "balances"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "5550.00"
+"3000" = "5000.00"
+"3999" = "550.00"
+"4000" = "0.00"
+"6000" = "0.00"
+
+# The statement for the quarter excludes the close: the year's income is
+# still reported.
+[[expect]]
+query = "profit_and_loss"
+from = "2026-01-01"
+to = "2026-03-31"
+[expect.values]
+"4000" = "900.00"
+"6000" = "350.00"
+net_income = "550.00"
diff --git a/bookspec/examples/statement-the-books-balance-and-the-equation-holds.toml b/bookspec/examples/statement-the-books-balance-and-the-equation-holds.toml
new file mode 100644
index 0000000..0e13e7c
--- /dev/null
+++ b/bookspec/examples/statement-the-books-balance-and-the-equation-holds.toml
@@ -0,0 +1,113 @@
+id = "statement-the-books-balance-and-the-equation-holds"
+title = "Normal balances, the trial balance and the accounting equation on one small book"
+rule = "An account MUST show its balance on its normal side (assets and expenses debit, liabilities, equity and revenue credit); the trial balance's debits MUST equal its credits; and assets MUST equal liabilities plus equity plus revenue less expenses."
+status = "AUTHORITY"
+sources = [
+  "Pacioli, Summa (1494), ch. 36: the total of the credits equals the total of the debits (docs/spec/sources/pacioli-1494.md)",
+  "FASB Concepts Statement 8, Ch. 4, E62: equity \"is the difference between the entity's assets and its liabilities\" (docs/spec/sources/fasb-asc.md)",
+  "OpenStax, Principles of Accounting, Vol. 1, 3.1: normal balances (CONVENTION; docs/spec/rules.md B-5)",
+]
+tags = ["accrual", "book", "us", "statement", "equation"]
+
+[setup]
+currency = "USD"
+fiscal_year_start = "01-01"
+basis = "accrual"
+rounding = "half-even"
+
+[[setup.accounts]]
+code = "1000"
+name = "Cash"
+type = "asset"
+
+[[setup.accounts]]
+code = "2000"
+name = "Loan"
+type = "liability"
+
+[[setup.accounts]]
+code = "3000"
+name = "Capital"
+type = "equity"
+
+[[setup.accounts]]
+code = "4000"
+name = "Sales"
+type = "revenue"
+tax_category = "gross_receipts"
+
+[[setup.accounts]]
+code = "6000"
+name = "Rent"
+type = "expense"
+tax_category = "rent_property"
+
+[[events]]
+date = "2026-01-02"
+description = "Members put in cash"
+lines = [
+  { account = "1000", side = "debit", amount = "5000.00" },
+  { account = "3000", side = "credit", amount = "5000.00" },
+]
+
+[[events]]
+date = "2026-01-03"
+description = "A loan"
+lines = [
+  { account = "1000", side = "debit", amount = "2000.00" },
+  { account = "2000", side = "credit", amount = "2000.00" },
+]
+
+[[events]]
+date = "2026-01-10"
+description = "A sale"
+lines = [
+  { account = "1000", side = "debit", amount = "750.50" },
+  { account = "4000", side = "credit", amount = "750.50" },
+]
+
+[[events]]
+date = "2026-01-15"
+description = "Rent"
+lines = [
+  { account = "6000", side = "debit", amount = "1200.25" },
+  { account = "1000", side = "credit", amount = "1200.25" },
+]
+
+# By hand. Cash: 5000.00 + 2000.00 + 750.50 - 1200.25 = 6550.25.
+# Debit side: cash 6550.25 + rent 1200.25 = 7750.50.
+# Credit side: loan 2000.00 + capital 5000.00 + sales 750.50 = 7750.50.
+[[expect]]
+query = "trial_balance"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "6550.25"
+"2000" = "-2000.00"
+"3000" = "-5000.00"
+"4000" = "-750.50"
+"6000" = "1200.25"
+
+# Each on its normal side, all positive here; the equation:
+# assets 6550.25 = liabilities 2000.00 + equity 5000.00
+#                  + (revenue 750.50 - expenses 1200.25) = 6550.25.
+[[expect]]
+query = "balances"
+as_of = "2026-12-31"
+[expect.values]
+"1000" = "6550.25"
+"2000" = "2000.00"
+"3000" = "5000.00"
+"4000" = "750.50"
+"6000" = "1200.25"
+
+# The trial balance as of an earlier day balances too: on January 9 there
+# is no sale and no rent.
+[[expect]]
+query = "trial_balance"
+as_of = "2026-01-09"
+[expect.values]
+"1000" = "7000.00"
+"2000" = "-2000.00"
+"3000" = "-5000.00"
+"4000" = "0.00"
+"6000" = "0.00"
diff --git a/bookspec/gnucash/Cargo.toml b/bookspec/gnucash/Cargo.toml
new file mode 100644
index 0000000..3361f32
--- /dev/null
+++ b/bookspec/gnucash/Cargo.toml
@@ -0,0 +1,18 @@
+[package]
+name = "bookspec-gnucash"
+version = "0.1.0"
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+description = "A second engine for bookspec: GnuCash, driven through the oracle container's files."
+
+[dependencies]
+bookspec-checker = { path = "../checker" }
+serde_json = "1"
+rust_decimal = "1"
+
+[dev-dependencies]
+bookspec-runner = { path = "../runner" }
+
+[lints]
+workspace = true
diff --git a/bookspec/gnucash/src/lib.rs b/bookspec/gnucash/src/lib.rs
new file mode 100644
index 0000000..078c9cc
--- /dev/null
+++ b/bookspec/gnucash/src/lib.rs
@@ -0,0 +1,250 @@
+//! GnuCash as a second bookspec engine (`plan/served.md` P13 step 5).
+//!
+//! The adapter keeps an example's chart and entries as the oracle's JSON
+//! books (`oracle/gnucash/books.py`: accounts, entries, as-of days) and
+//! asks GnuCash 5.10, in its pinned container, for each balance. GnuCash
+//! is a cross-check, never the authority (`docs/oracle.md`, "Who is
+//! right"): where it differs from an example, the difference is
+//! adjudicated from the sources and recorded, not conformed to.
+//!
+//! Only what GnuCash itself answers is claimed: the balance queries
+//! (`trial_balance`, `balances`), by the rules whose examples ask nothing
+//! else. GnuCash never refuses an entry (it books the difference to an
+//! `Imbalance` account), so a refused event is *accepted* here, as it
+//! would be by a GnuCash user, and the runner reports the difference.
+
+use std::collections::BTreeMap;
+use std::io::Write;
+use std::process::{Command, Stdio};
+use std::str::FromStr;
+
+use bookspec_checker::{
+    Area, ChangeSpec, Claims, Engine, Event, Query, Refusal, RuleId, Setup, fallback_refusal,
+};
+use rust_decimal::Decimal;
+use serde_json::{Value, json};
+
+/// The oracle container (`just oracle` builds it from `oracle/gnucash`).
+pub const IMAGE: &str = "wanderbooks-gnucash-oracle";
+
+/// The rules this adapter claims: those whose examples ask only for
+/// balances, which GnuCash answers itself.
+pub fn claimed() -> Vec<RuleId> {
+    vec![
+        RuleId::new(Area::Entry, 1),
+        RuleId::new(Area::Entry, 2),
+        RuleId::new(Area::Entry, 3),
+        RuleId::new(Area::Ledger, 1),
+        RuleId::new(Area::Ledger, 3),
+        RuleId::new(Area::Statement, 1),
+        RuleId::new(Area::Statement, 2),
+    ]
+}
+
+/// One account of the book handed to GnuCash.
+struct Account {
+    code: String,
+    kind: &'static str,
+    normal_debit: bool,
+}
+
+/// GnuCash, as bookspec's `Engine`.
+#[derive(Default)]
+pub struct GnuCash {
+    accounts: Vec<Account>,
+    entries: Vec<Value>,
+    /// Each event's entry, by event number (1-based), for reversals.
+    event_entries: BTreeMap<usize, usize>,
+    events: usize,
+}
+
+impl GnuCash {
+    /// An empty engine.
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    fn id(&self, code: &str) -> Option<usize> {
+        self.accounts
+            .iter()
+            .position(|a| a.code == code)
+            .map(|i| i + 1)
+    }
+
+    fn book(&self, as_of: &str) -> Value {
+        let accounts: Vec<Value> = self
+            .accounts
+            .iter()
+            .enumerate()
+            .map(|(i, a)| json!({"id": i + 1, "code": a.code, "name": a.code, "type": a.kind}))
+            .collect();
+        json!({"accounts": accounts, "entries": self.entries, "as_of": [as_of]})
+    }
+
+    /// GnuCash's own balance of every account as of a day: debits
+    /// positive, exact decimal strings, by account code.
+    fn balances(&self, as_of: &str) -> Result<BTreeMap<String, Decimal>, Refusal> {
+        let mut child = Command::new("docker")
+            .args(["run", "--rm", "-i", IMAGE])
+            .stdin(Stdio::piped())
+            .stdout(Stdio::piped())
+            .stderr(Stdio::null())
+            .spawn()
+            .map_err(|e| unavailable(format!("docker: {e}")))?;
+        let books = json!([self.book(as_of)]);
+        child
+            .stdin
+            .take()
+            .unwrap()
+            .write_all(books.to_string().as_bytes())
+            .map_err(|e| unavailable(format!("docker stdin: {e}")))?;
+        let out = child
+            .wait_with_output()
+            .map_err(|e| unavailable(format!("docker: {e}")))?;
+        if !out.status.success() {
+            return Err(unavailable(
+                "the GnuCash oracle failed; build it with `just oracle`".into(),
+            ));
+        }
+        let results: Value = serde_json::from_slice(&out.stdout)
+            .map_err(|e| unavailable(format!("oracle output: {e}")))?;
+        let at = &results[0]["balances"][as_of];
+        let mut map = BTreeMap::new();
+        for (i, a) in self.accounts.iter().enumerate() {
+            let v = at[(i + 1).to_string()]
+                .as_str()
+                .ok_or_else(|| unavailable(format!("no balance for {}", a.code)))?;
+            map.insert(
+                a.code.clone(),
+                Decimal::from_str(v).map_err(|e| unavailable(e.to_string()))?,
+            );
+        }
+        Ok(map)
+    }
+}
+
+fn unavailable(why: String) -> Refusal {
+    fallback_refusal(
+        RuleId::new(Area::Ledger, 1),
+        format!("the GnuCash oracle: {why}"),
+    )
+}
+
+fn not_supported(what: &str) -> Refusal {
+    fallback_refusal(
+        RuleId::new(Area::Ledger, 1),
+        format!("the GnuCash adapter does not take {what}"),
+    )
+}
+
+impl Engine for GnuCash {
+    fn load(&mut self, setup: &Setup) -> Result<(), Refusal> {
+        for a in &setup.accounts {
+            let (kind, normal_debit) = match a.kind.as_str() {
+                "asset" => ("Asset", true),
+                "liability" => ("Liability", false),
+                "equity" => ("Equity", false),
+                "revenue" => ("Revenue", false),
+                "expense" => ("Expense", true),
+                other => return Err(not_supported(&format!("account type {other}"))),
+            };
+            self.accounts.push(Account {
+                code: a.code.clone(),
+                kind,
+                normal_debit,
+            });
+        }
+        if setup.currency != "USD" {
+            return Err(not_supported("a currency other than USD"));
+        }
+        Ok(())
+    }
+
+    fn apply(&mut self, event: &Event) -> Result<(), Refusal> {
+        self.events += 1;
+        let n = self.events;
+        let date = event
+            .date
+            .clone()
+            .ok_or_else(|| not_supported("an undated event"))?;
+        let description = event.description.clone().unwrap_or_default();
+        if !event.lines.is_empty() {
+            let mut lines = Vec::new();
+            for l in &event.lines {
+                let account = self
+                    .id(&l.account)
+                    .ok_or_else(|| not_supported("an unknown account"))?;
+                lines.push(json!({"account": account, "side": l.side, "amount": l.amount}));
+            }
+            self.entries
+                .push(json!({"date": date, "description": description, "lines": lines}));
+            self.event_entries.insert(n, self.entries.len() - 1);
+            return Ok(());
+        }
+        if let Some(of) = event.reverses {
+            // GnuCash has no reversal link; a user reverses by writing the
+            // opposite transaction, which is what is done here.
+            let idx = *self
+                .event_entries
+                .get(&of)
+                .ok_or_else(|| not_supported("a reversal of an event that posted nothing"))?;
+            let original = self.entries[idx].clone();
+            let flipped: Vec<Value> = original["lines"]
+                .as_array()
+                .unwrap()
+                .iter()
+                .map(|l| {
+                    let side = if l["side"] == "debit" {
+                        "credit"
+                    } else {
+                        "debit"
+                    };
+                    json!({"account": l["account"], "side": side, "amount": l["amount"]})
+                })
+                .collect();
+            self.entries
+                .push(json!({"date": date, "description": description, "lines": flipped}));
+            self.event_entries.insert(n, self.entries.len() - 1);
+            return Ok(());
+        }
+        Err(not_supported("this kind of event"))
+    }
+
+    fn query(&self, q: &Query) -> Result<Value, Refusal> {
+        let as_of = q
+            .as_of
+            .clone()
+            .ok_or_else(|| not_supported("a query without as_of"))?;
+        match q.name.as_str() {
+            "trial_balance" | "balances" => {
+                let balances = self.balances(&as_of)?;
+                let mut out = serde_json::Map::new();
+                for a in &self.accounts {
+                    let b = balances[&a.code];
+                    let mut shown = if q.name == "balances" && !a.normal_debit {
+                        -b
+                    } else {
+                        b
+                    };
+                    if shown.is_zero() {
+                        shown = Decimal::ZERO;
+                    }
+                    if shown.scale() < 2 {
+                        shown.rescale(2);
+                    }
+                    out.insert(a.code.clone(), Value::String(shown.to_string()));
+                }
+                Ok(Value::Object(out))
+            }
+            other => Err(not_supported(&format!("the {other} query"))),
+        }
+    }
+
+    fn claims(&self) -> Claims {
+        Claims::new(claimed())
+    }
+
+    fn change(&mut self, _change: &ChangeSpec) -> Result<(), Refusal> {
+        Err(not_supported("a change"))
+    }
+}
diff --git a/bookspec/gnucash/tests/gnucash.rs b/bookspec/gnucash/tests/gnucash.rs
new file mode 100644
index 0000000..9db7d2b
--- /dev/null
+++ b/bookspec/gnucash/tests/gnucash.rs
@@ -0,0 +1,137 @@
+//! GnuCash, run through bookspec's examples (`just oracle` builds the
+//! container). Needs Docker, so the test is ignored by default:
+//! `cargo test -p bookspec-gnucash -- --ignored --nocapture`.
+
+use std::path::{Path, PathBuf};
+
+use bookspec_checker::{Example, rules};
+use bookspec_gnucash::{GnuCash, claimed};
+
+fn examples() -> Vec<Example> {
+    let dir = Path::new(env!("CARGO_MANIFEST_DIR")).join("../examples");
+    let mut files: Vec<PathBuf> = std::fs::read_dir(dir)
+        .unwrap()
+        .map(|e| e.unwrap().path())
+        .filter(|p| p.extension().is_some_and(|x| x == "toml"))
+        .collect();
+    files.sort();
+    files
+        .iter()
+        .map(|f| Example::from_toml(&std::fs::read_to_string(f).unwrap()).unwrap())
+        .collect()
+}
+
+/// The differences GnuCash shows, each settled from the sources
+/// (`bookspec/README.md`, "GnuCash, the second engine"). A new difference,
+/// or one that goes away, fails this test until it is adjudicated again.
+const ADJUDICATED: [(&str, &str); 3] = [
+    (
+        "entry-an-unbalanced-entry-is-refused",
+        "event 2: accepted, expected refused: unbalanced",
+    ),
+    (
+        "entry-a-line-amount-is-positive",
+        "event 1: accepted, expected refused: negative_amount",
+    ),
+    (
+        "ledger-a-fraction-of-a-cent-is-refused",
+        "event 1: accepted, expected refused: finer_than_minor_unit",
+    ),
+];
+
+fn run_claimed() -> bookspec_runner::Report {
+    let claimed = claimed();
+    let mut wanted = std::collections::BTreeSet::new();
+    for r in rules().iter().filter(|r| claimed.contains(&r.id)) {
+        wanted.extend(r.examples.iter().copied());
+    }
+    let examples: Vec<Example> = examples()
+        .into_iter()
+        .filter(|e| wanted.contains(e.id.as_str()))
+        .collect();
+    bookspec_runner::run(&examples, rules(), |_| GnuCash::new())
+}
+
+#[test]
+#[ignore = "needs Docker and the GnuCash image: `just oracle`"]
+fn gnucash_differs_only_where_it_was_adjudicated() {
+    let report = run_claimed();
+    let found: Vec<(&str, &str)> = report
+        .examples
+        .iter()
+        .filter_map(|e| e.failure.as_deref().map(|f| (e.id.as_str(), f)))
+        .collect();
+    let mut want: Vec<(&str, &str)> = ADJUDICATED.to_vec();
+    want.sort();
+    let mut got = found.clone();
+    got.sort();
+    assert_eq!(got, want, "GnuCash's differences changed: adjudicate again");
+    // The rules that every example passes are passed.
+    for rule in [
+        "BS-entry-3",
+        "BS-ledger-3",
+        "BS-statement-1",
+        "BS-statement-2",
+    ] {
+        let id = bookspec_checker::RuleId::parse(rule).unwrap();
+        assert_eq!(report.rules[&id], bookspec_runner::Outcome::Pass, "{rule}");
+    }
+}
+
+/// The evidence the adjudications rest on, from GnuCash's own answers:
+/// what it did with the entry it accepted.
+#[test]
+#[ignore = "needs Docker and the GnuCash image: `just oracle`"]
+fn what_gnucash_did_with_the_entries_the_specification_refuses() {
+    use bookspec_checker::Engine;
+    use std::str::FromStr;
+    let by_id = |id: &str| examples().into_iter().find(|e| e.id == id).unwrap();
+    let net = |id: &str, event: usize| -> rust_decimal::Decimal {
+        let ex = by_id(id);
+        let mut g = GnuCash::new();
+        g.load(&ex.setup).unwrap();
+        for e in ex.events.iter().take(event) {
+            g.apply(e).expect("GnuCash accepts it");
+        }
+        let q = ex
+            .expect
+            .iter()
+            .find(|x| x.query == "trial_balance")
+            .unwrap()
+            .query();
+        let answer = g.query(&q).unwrap();
+        answer
+            .as_object()
+            .unwrap()
+            .values()
+            .map(|v| rust_decimal::Decimal::from_str(v.as_str().unwrap()).unwrap())
+            .sum()
+    };
+    // Debits 100.00 against credits 90.00: the accounts GnuCash lists no
+    // longer net to zero; ten dollars sit where GnuCash parked them, in an
+    // Imbalance account of its own making.
+    assert_eq!(
+        net("entry-an-unbalanced-entry-is-refused", 2).to_string(),
+        "10.00"
+    );
+    // A credit of minus 100.00 is booked as a debit of 100.00: both lines
+    // are debits, and 200.00 sits in the Imbalance account.
+    assert_eq!(
+        net("entry-a-line-amount-is-positive", 1).to_string(),
+        "200.00"
+    );
+    // 10.005 on each side is rounded to the cent, silently: GnuCash's USD
+    // balance reads 10.01 (the choice rules.md B-3 records the owner took
+    // the other way, after the first cross-check found it).
+    let ex = by_id("ledger-a-fraction-of-a-cent-is-refused");
+    let mut g = GnuCash::new();
+    g.load(&ex.setup).unwrap();
+    g.apply(&ex.events[0]).unwrap();
+    let q = ex
+        .expect
+        .iter()
+        .find(|x| x.query == "trial_balance")
+        .unwrap()
+        .query();
+    assert_eq!(g.query(&q).unwrap()["1000"], "10.01");
+}
diff --git a/bookspec/lean/.gitignore b/bookspec/lean/.gitignore
new file mode 100644
index 0000000..01f8cdb
--- /dev/null
+++ b/bookspec/lean/.gitignore
@@ -0,0 +1 @@
+.lake/
diff --git a/bookspec/lean/Audit.lean b/bookspec/lean/Audit.lean
new file mode 100644
index 0000000..d528d73
--- /dev/null
+++ b/bookspec/lean/Audit.lean
@@ -0,0 +1,14 @@
+import Bookspec
+
+/-! Each of the five laws' axioms are printed, and must be only Lean's
+standard three (`propext`, `Quot.sound`, `Classical.choice`) or fewer. No
+`sorryAx`, nothing assumed. `bookspec/checker/tests/lean.rs` reads this
+file's output shape; run it with `lake env lean Audit.lean`. -/
+
+open Bookspec
+
+#print axioms law_debits_equal_credits
+#print axioms law_accounting_equation
+#print axioms law_trial_balance
+#print axioms law_net_income_articulates
+#print axioms law_cash_flow_is_change_in_cash
diff --git a/bookspec/lean/Bookspec.lean b/bookspec/lean/Bookspec.lean
new file mode 100644
index 0000000..14fd6c2
--- /dev/null
+++ b/bookspec/lean/Bookspec.lean
@@ -0,0 +1,2 @@
+import Bookspec.Laws
+import Bookspec.Ledger
diff --git a/bookspec/lean/Bookspec/Basic.lean b/bookspec/lean/Bookspec/Basic.lean
new file mode 100644
index 0000000..ce4becd
--- /dev/null
+++ b/bookspec/lean/Bookspec/Basic.lean
@@ -0,0 +1,165 @@
+/-!
+# Lines, sides, and nets
+
+The vocabulary of double entry. Money is `Int`: an exact count of the
+smallest unit the books use. Any finite set of exact decimals (what the
+engine stores) scales to integers without loss, and every law here is a
+law of addition, so `Int` is a faithful model.
+
+Mirrors `crates/ledger-core/src/kernel.rs` (`flip`, `signed`, `net`,
+`totals`) and `account.rs` (`Side`, `AccountType`, `normal_side`).
+-/
+
+namespace Bookspec
+
+/-- Debit or credit. -/
+inductive Side where
+  | debit
+  | credit
+  deriving DecidableEq, Repr
+
+/-- The other side (`kernel::flip`). -/
+def Side.flip : Side → Side
+  | .debit => .credit
+  | .credit => .debit
+
+@[simp] theorem Side.flip_flip (s : Side) : s.flip.flip = s := by
+  cases s <;> rfl
+
+theorem Side.flip_ne (s : Side) : s.flip ≠ s := by
+  cases s <;> simp [Side.flip]
+
+/-- The five account types. -/
+inductive AccountType where
+  | asset
+  | liability
+  | equity
+  | revenue
+  | expense
+  deriving DecidableEq, Repr
+
+/-- The side that increases an account (`AccountType::normal_side`). -/
+def AccountType.normal : AccountType → Side
+  | .asset | .expense => .debit
+  | .liability | .equity | .revenue => .credit
+
+/-- A line's signed amount: `+a` for a debit, `-a` for a credit
+(`kernel::signed`). -/
+def signed : Side → Int → Int
+  | .debit, a => a
+  | .credit, a => -a
+
+@[simp] theorem signed_debit (a : Int) : signed .debit a = a := rfl
+@[simp] theorem signed_credit (a : Int) : signed .credit a = -a := rfl
+
+theorem signed_flip (s : Side) (a : Int) : signed s.flip a = -signed s a := by
+  cases s <;> simp [Side.flip]
+
+/-- One journal line. -/
+structure Line where
+  account : Nat
+  side : Side
+  amount : Int
+  deriving DecidableEq, Repr
+
+/-- A line's signed amount. -/
+def Line.signed (l : Line) : Int := Bookspec.signed l.side l.amount
+
+/-- The net of some lines: debits minus credits (`kernel::net`). -/
+def net : List Line → Int
+  | [] => 0
+  | l :: ls => l.signed + net ls
+
+/-- Total debits. -/
+def debits : List Line → Int
+  | [] => 0
+  | l :: ls => (if l.side = .debit then l.amount else 0) + debits ls
+
+/-- Total credits. -/
+def credits : List Line → Int
+  | [] => 0
+  | l :: ls => (if l.side = .credit then l.amount else 0) + credits ls
+
+@[simp] theorem net_nil : net [] = 0 := rfl
+@[simp] theorem net_cons (l : Line) (ls : List Line) : net (l :: ls) = l.signed + net ls := rfl
+
+theorem net_append (xs ys : List Line) : net (xs ++ ys) = net xs + net ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, net_cons, ih]; omega
+
+/-- The net is debits minus credits. -/
+theorem net_eq_debits_sub_credits (ls : List Line) : net ls = debits ls - credits ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    obtain ⟨a, s, m⟩ := l
+    cases s <;> simp [net, debits, credits, Line.signed, signed, ih] <;> omega
+
+/-- A sum over a list of account codes. -/
+def sumOver (f : Nat → Int) : List Nat → Int
+  | [] => 0
+  | a :: as => f a + sumOver f as
+
+@[simp] theorem sumOver_nil (f : Nat → Int) : sumOver f [] = 0 := rfl
+@[simp] theorem sumOver_cons (f : Nat → Int) (a : Nat) (as : List Nat) :
+    sumOver f (a :: as) = f a + sumOver f as := rfl
+
+theorem sumOver_add (f g : Nat → Int) (as : List Nat) :
+    sumOver (fun a => f a + g a) as = sumOver f as + sumOver g as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp only [sumOver_cons, ih]; omega
+
+theorem sumOver_neg (f : Nat → Int) (as : List Nat) :
+    sumOver (fun a => -f a) as = -sumOver f as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp only [sumOver_cons, ih]; omega
+
+theorem sumOver_zero (as : List Nat) : sumOver (fun _ => 0) as = 0 := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp [ih]
+
+theorem sumOver_congr (f g : Nat → Int) (as : List Nat) (h : ∀ a ∈ as, f a = g a) :
+    sumOver f as = sumOver g as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [sumOver_cons]
+    rw [h a (by simp), ih (fun b hb => h b (by simp [hb]))]
+
+/-- No code repeats (a chart's codes are unique). -/
+def Distinct : List Nat → Prop
+  | [] => True
+  | a :: as => a ∉ as ∧ Distinct as
+
+/-- Summing an indicator over codes that do not include `k` gives zero. -/
+theorem sumOver_indicator_absent (k : Nat) (x : Int) (as : List Nat) (h : k ∉ as) :
+    sumOver (fun a => if k = a then x else 0) as = 0 := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    have hka : k ≠ a := fun e => h (e ▸ List.mem_cons_self ..)
+    have hk : k ∉ as := fun hm => h (List.mem_cons_of_mem _ hm)
+    simp [hka, ih hk]
+
+/-- Summing an indicator over distinct codes that include `k` picks out
+exactly one term. -/
+theorem sumOver_indicator (k : Nat) (x : Int) (as : List Nat) (hd : Distinct as)
+    (hk : k ∈ as) : sumOver (fun a => if k = a then x else 0) as = x := by
+  induction as with
+  | nil => simp at hk
+  | cons a as ih =>
+    obtain ⟨ha, hd⟩ := hd
+    by_cases e : k = a
+    · subst e
+      simp [sumOver_indicator_absent k x as ha]
+    · have : k ∈ as := by
+        cases hk with
+        | head => exact absurd rfl e
+        | tail _ h => exact h
+      simp [e, ih hd this]
+
+end Bookspec
diff --git a/bookspec/lean/Bookspec/Closing.lean b/bookspec/lean/Bookspec/Closing.lean
new file mode 100644
index 0000000..c9ffca5
--- /dev/null
+++ b/bookspec/lean/Bookspec/Closing.lean
@@ -0,0 +1,451 @@
+import Bookspec.Statements
+
+/-!
+# Closing a period, and splitting the net
+
+Mirrors `kernel::closing_line`, `kernel::credit_line`, `kernel::plug_last`,
+`periods::allocate`, and `Ledger::close_period_to` (income closing, net to
+one equity account or split among members).
+-/
+
+namespace Bookspec
+
+/-- The line that zeroes an account with movement `m`: the opposite side,
+same amount; nothing for zero (`kernel::closing_line`). It is also the
+line that credits `m` to an account (`kernel::credit_line`). -/
+def closingLine (a : Nat) (m : Int) : List Line :=
+  if 0 < m then [⟨a, .credit, m⟩] else if m < 0 then [⟨a, .debit, -m⟩] else []
+
+theorem net_closingLine (a : Nat) (m : Int) : net (closingLine a m) = -m := by
+  unfold closingLine
+  split
+  · simp [Line.signed]
+  · split <;> simp [Line.signed] <;> omega
+
+theorem movement_closingLine (b a : Nat) (m : Int) :
+    movement b (closingLine a m) = if b = a then -m else 0 := by
+  by_cases e : b = a
+  · subst e
+    rcases (by omega : 0 < m ∨ m < 0 ∨ m = 0) with h | h | h
+    · simp [closingLine, h, Line.signed]
+    · have : ¬ 0 < m := by omega
+      simp [closingLine, h, this, Line.signed]
+    · simp [closingLine, h]
+  · have e' : ¬ a = b := fun x => e x.symm
+    unfold closingLine
+    split <;> (try split) <;> simp [e']
+
+theorem closingLine_pos (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, 0 < l.amount := by
+  unfold closingLine
+  split
+  · simp; omega
+  · split
+    · simp; omega
+    · simp
+
+theorem closingLine_account (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, l.account = a := by
+  unfold closingLine
+  split
+  · simp
+  · split <;> simp
+
+theorem closingLine_eq_nil (a : Nat) (m : Int) : closingLine a m = [] ↔ m = 0 := by
+  unfold closingLine
+  split
+  · simp; omega
+  · split
+    · simp; omega
+    · simp; omega
+
+/-- The closing lines for some accounts: one per account with a nonzero
+movement. -/
+def closings (as : List Nat) (ls : List Line) : List Line :=
+  match as with
+  | [] => []
+  | a :: as => closingLine a (movement a ls) ++ closings as ls
+
+theorem net_closings (as : List Nat) (ls : List Line) :
+    net (closings as ls) = -sumOver (fun a => movement a ls) as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp only [closings, net_append, net_closingLine, ih, sumOver_cons]; omega
+
+theorem movement_closings (b : Nat) (as : List Nat) (ls : List Line) (hd : Distinct as) :
+    movement b (closings as ls) = if b ∈ as then -movement b ls else 0 := by
+  induction as with
+  | nil => simp [closings]
+  | cons a as ih =>
+    obtain ⟨ha, hd⟩ := hd
+    simp only [closings, movement_append, movement_closingLine, ih hd]
+    by_cases e : b = a
+    · subst e; simp [ha]
+    · simp [e]
+
+theorem closings_pos (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, 0 < l.amount := by
+  induction as with
+  | nil => simp [closings]
+  | cons a as ih =>
+    intro l hl
+    simp only [closings, List.mem_append] at hl
+    cases hl with
+    | inl h => exact closingLine_pos _ _ l h
+    | inr h => exact ih l h
+
+theorem closings_account (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, l.account ∈ as := by
+  induction as with
+  | nil => simp [closings]
+  | cons a as ih =>
+    intro l hl
+    simp only [closings, List.mem_append] at hl
+    cases hl with
+    | inl h => rw [closingLine_account _ _ l h]; simp
+    | inr h => exact List.mem_cons_of_mem _ (ih l h)
+
+/-- Nothing to close means every closed account was already at zero. -/
+theorem closings_eq_nil (as : List Nat) (ls : List Line) (h : closings as ls = []) :
+    ∀ a ∈ as, movement a ls = 0 := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    simp only [closings, List.append_eq_nil_iff] at h
+    intro b hb
+    cases hb with
+    | head => exact (closingLine_eq_nil _ _).1 h.1
+    | tail _ hb => exact ih h.2 b hb
+
+/-! ## The net to equity -/
+
+/-- The sum of some amounts. -/
+def total : List Int → Int
+  | [] => 0
+  | x :: xs => x + total xs
+
+/-- Lines crediting each target its part (`kernel::credit_line` per
+member). -/
+def equityLines : List (Nat × Int) → List Line
+  | [] => []
+  | (t, c) :: ts => closingLine t c ++ equityLines ts
+
+theorem net_equityLines (ts : List (Nat × Int)) :
+    net (equityLines ts) = -total (ts.map Prod.snd) := by
+  induction ts with
+  | nil => rfl
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    simp only [equityLines, net_append, net_closingLine, ih, List.map_cons, total]; omega
+
+theorem movement_equityLines_absent (b : Nat) (ts : List (Nat × Int))
+    (h : ∀ x ∈ ts, x.1 ≠ b) : movement b (equityLines ts) = 0 := by
+  induction ts with
+  | nil => rfl
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    have ht : b ≠ t := fun e => h (t, c) (by simp) e.symm
+    simp only [equityLines, movement_append, movement_closingLine, ht, ite_false,
+      ih (fun y hy => h y (List.mem_cons_of_mem _ hy))]
+    rfl
+
+theorem equityLines_pos (ts : List (Nat × Int)) : ∀ l ∈ equityLines ts, 0 < l.amount := by
+  induction ts with
+  | nil => simp [equityLines]
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    intro l hl
+    simp only [equityLines, List.mem_append] at hl
+    cases hl with
+    | inl h => exact closingLine_pos _ _ l h
+    | inr h => exact ih l h
+
+theorem equityLines_account (ts : List (Nat × Int)) :
+    ∀ l ∈ equityLines ts, ∃ x ∈ ts, l.account = x.1 := by
+  induction ts with
+  | nil => simp [equityLines]
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    intro l hl
+    simp only [equityLines, List.mem_append] at hl
+    cases hl with
+    | inl h => exact ⟨(t, c), by simp, closingLine_account _ _ l h⟩
+    | inr h =>
+      obtain ⟨y, hy, e⟩ := ih l h
+      exact ⟨y, List.mem_cons_of_mem _ hy, e⟩
+
+theorem equityLines_eq_nil (ts : List (Nat × Int)) (h : equityLines ts = []) :
+    total (ts.map Prod.snd) = 0 := by
+  induction ts with
+  | nil => rfl
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    simp only [equityLines, List.append_eq_nil_iff] at h
+    simp only [List.map_cons, total, (closingLine_eq_nil _ _).1 h.1, ih h.2]; rfl
+
+/-- The closing entry: zero the closed accounts, credit the net to the
+targets. -/
+def closingEntry (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) : List Line :=
+  closings as ls ++ equityLines ts
+
+/-- **A closing entry balances** when the targets' parts sum to the net
+of the closing lines (the net income), however that net was split. -/
+theorem closingEntry_net (as : List Nat) (ts : List (Nat × Int)) (ls : List Line)
+    (hsum : total (ts.map Prod.snd) = net (closings as ls)) :
+    net (closingEntry as ts ls) = 0 := by
+  rw [closingEntry, net_append, net_equityLines, hsum]; omega
+
+/-- **A closing entry zeroes every account it closes.** -/
+theorem closingEntry_zeroes (as : List Nat) (ts : List (Nat × Int)) (ls : List Line)
+    (hd : Distinct as) (b : Nat) (hb : b ∈ as) (ht : ∀ x ∈ ts, x.1 ≠ b) :
+    movement b (ls ++ closingEntry as ts ls) = 0 := by
+  rw [movement_append, closingEntry, movement_append, movement_closings b as ls hd,
+    movement_equityLines_absent b ts ht]
+  simp only [hb, ite_true]; omega
+
+/-- **A non-empty closing entry is acceptable**: two or more lines, every
+amount positive, debits equal to credits. -/
+theorem closingEntry_accepted (as : List Nat) (ts : List (Nat × Int)) (ls : List Line)
+    (hsum : total (ts.map Prod.snd) = net (closings as ls)) (hne : closings as ls ≠ []) :
+    Accepted (closingEntry as ts ls) := by
+  refine ⟨?_, ?_, ?_⟩
+  · rw [closingEntry, List.length_append]
+    match hc : closings as ls with
+    | [] => exact absurd hc hne
+    | [l] =>
+      have hl : 0 < l.amount := closings_pos as ls l (by rw [hc]; simp)
+      have hnet : net (closings as ls) ≠ 0 := by
+        rw [hc]; obtain ⟨a, s, m⟩ := l
+        cases s <;> simp [Line.signed] at hl ⊢ <;> omega
+      have : equityLines ts ≠ [] := fun h => hnet (hsum ▸ equityLines_eq_nil ts h)
+      have : 1 ≤ (equityLines ts).length := by
+        cases h : equityLines ts with
+        | nil => exact absurd h this
+        | cons _ _ => simp
+      simp; omega
+    | _ :: _ :: _ => simp; omega
+  · intro l hl
+    simp only [closingEntry, List.mem_append] at hl
+    cases hl with
+    | inl h => exact closings_pos as ls l h
+    | inr h => exact equityLines_pos ts l h
+  · have := closingEntry_net as ts ls hsum
+    rw [net_eq_debits_sub_credits] at this; omega
+
+/-! ## Net income -/
+
+/-- The chart's revenue and expense codes: what a close zeroes. -/
+def nominalCodes : Chart → List Nat
+  | [] => []
+  | (a, t) :: c => if t = .revenue ∨ t = .expense then a :: nominalCodes c else nominalCodes c
+
+theorem nominalCodes_sub (c : Chart) : ∀ a ∈ nominalCodes c, a ∈ codes c := by
+  induction c with
+  | nil => simp [nominalCodes]
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    intro b hb
+    simp only [nominalCodes] at hb
+    split at hb
+    · cases hb with
+      | head => simp
+      | tail _ h => exact List.mem_cons_of_mem _ (ih b h)
+    · exact List.mem_cons_of_mem _ (ih b hb)
+
+theorem nominalCodes_distinct (c : Chart) (hd : Distinct (codes c)) : Distinct (nominalCodes c) := by
+  induction c with
+  | nil => trivial
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    obtain ⟨ha, hd⟩ := hd
+    simp only [nominalCodes]
+    split
+    · exact ⟨fun h => ha (nominalCodes_sub c a h), ih hd⟩
+    · exact ih hd
+
+/-- **The net a close credits to equity is the period's net income**:
+revenue balances minus expense balances. -/
+theorem net_closings_is_net_income (c : Chart) (ls : List Line) :
+    net (closings (nominalCodes c) ls) = typeTotal .revenue ls c - typeTotal .expense ls c := by
+  rw [net_closings]
+  induction c with
+  | nil => rfl
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    cases t <;> simp [nominalCodes, typeTotal, balance, AccountType.normal, signed] at ih ⊢ <;> omega
+
+/-! ## Splitting among members -/
+
+/-- Make rounded parts sum to the whole: the last becomes the whole minus
+the others (`kernel::plug_last`). -/
+def plugLast (whole : Int) : List Int → List Int
+  | [] => []
+  | [_] => [whole]
+  | p :: q :: rest => p :: plugLast (whole - p) (q :: rest)
+
+/-- **An allocation's parts sum to the whole, exactly**, however the
+other parts were rounded. -/
+theorem plugLast_total (whole : Int) (ps : List Int) (h : ps ≠ []) :
+    total (plugLast whole ps) = whole := by
+  induction ps generalizing whole with
+  | nil => exact absurd rfl h
+  | cons p rest ih =>
+    match rest, ih with
+    | [], _ => show total [whole] = whole; simp [total]
+    | q :: rest, ih =>
+      simp only [plugLast, total]
+      have := ih (whole - p) (by simp)
+      omega
+
+theorem plugLast_length (whole : Int) (ps : List Int) : (plugLast whole ps).length = ps.length := by
+  induction ps generalizing whole with
+  | nil => rfl
+  | cons p rest ih =>
+    match rest, ih with
+    | [], _ => rfl
+    | q :: rest, ih => simp only [plugLast, List.length_cons]; rw [ih]; rfl
+
+/-- Only the last part changes. -/
+theorem plugLast_keeps (whole : Int) (ps : List Int) :
+    (plugLast whole ps).dropLast = ps.dropLast := by
+  induction ps generalizing whole with
+  | nil => rfl
+  | cons p rest ih =>
+    match rest, ih with
+    | [], _ => rfl
+    | q :: rest, ih =>
+      have hne : plugLast (whole - p) (q :: rest) ≠ [] := by
+        intro h
+        have := plugLast_length (whole - p) (q :: rest)
+        rw [h] at this; simp at this
+      rw [show plugLast whole (p :: q :: rest) = p :: plugLast (whole - p) (q :: rest) from rfl,
+        List.dropLast_cons_of_ne_nil hne, ih, List.dropLast_cons_cons]
+
+/-! ## Cumulative member closes
+
+A run of members closes under the run rule of 2026-10-13 to P3
+(`CloseTo::MembersRun`, journaled `"cumulative"`; rules.md B-13) gives each
+member, at each close, their allocation of the run's total so far minus
+their allocation of the total before it. `alloc` is any allocation of an
+amount to members (member `i` gets `alloc x i`), such as
+`periods::allocate`. -/
+
+/-- What one close gives member `i`: `before` is the run's total before
+it, `net` what it closes. -/
+def closePart (alloc : Int → Nat → Int) (before net : Int) (i : Nat) : Int :=
+  alloc (before + net) i - alloc before i
+
+/-- What a run of closes with these nets, starting after `before`, gives
+member `i` in all. -/
+def runPart (alloc : Int → Nat → Int) : Int → List Int → Nat → Int
+  | _, [], _ => 0
+  | before, net :: rest, i => closePart alloc before net i + runPart alloc (before + net) rest i
+
+/-- **A run telescopes**: member `i`'s total from a run is their allocation
+of everything the run closed, less their allocation of where it started.
+From an empty start (`alloc 0 = 0`), it is exactly their allocation of
+the run's total, so its rounding is one allocation's rounding, never a
+sum of them. -/
+theorem runPart_telescopes (alloc : Int → Nat → Int) (before : Int) (nets : List Int) (i : Nat) :
+    runPart alloc before nets i = alloc (before + nets.sum) i - alloc before i := by
+  induction nets generalizing before with
+  | nil => simp [runPart]
+  | cons n rest ih =>
+    simp only [runPart, closePart, ih, List.sum_cons]
+    rw [show before + n + rest.sum = before + (n + rest.sum) by omega]
+    omega
+
+/-- A sum of differences is the difference of the sums. -/
+theorem sum_map_sub (f g : Nat → Int) (ms : List Nat) :
+    (ms.map (fun i => f i - g i)).sum = (ms.map f).sum - (ms.map g).sum := by
+  induction ms with
+  | nil => simp
+  | cons m ms ih => simp only [List.map_cons, List.sum_cons, ih]; omega
+
+/-- **Each close hands out exactly its net** when every allocation sums
+to its amount (`periods::allocate` does: `kernel::apportion`). -/
+theorem closePart_total (alloc : Int → Nat → Int) (members : List Nat)
+    (sums : ∀ x, (members.map (alloc x)).sum = x) (before net : Int) :
+    (members.map (closePart alloc before net)).sum = net := by
+  have h := sum_map_sub (alloc (before + net)) (alloc before) members
+  unfold closePart
+  rw [h, sums, sums]
+  omega
+
+/-! ## Members closes counted from a count's start (P3)
+
+The rule since P3 (`CloseTo::Members`, rules.md B-13; D-10): a close gives
+member `i` their allocation of everything the count has closed (`closed`
+before it, plus its `net`), less what the count's earlier closes gave them
+(`given i`), whatever rule those closes were made under
+(`periods::allocate_cumulative`, `kernel::apportion_cumulative`). The run
+rule of 2026-10-13 (`CloseTo::MembersRun`, `closePart`) is the special case
+where the earlier closes gave exactly the allocation. -/
+
+/-- What a cumulative close gives member `i`. -/
+def trueUp (alloc : Int → Nat → Int) (closed net : Int) (given : Nat → Int) (i : Nat) : Int :=
+  alloc (closed + net) i - given i
+
+/-- **A cumulative close hands out exactly its net**, whatever rule the
+earlier closes used, as long as they handed out what they closed. -/
+theorem trueUp_total (alloc : Int → Nat → Int) (members : List Nat)
+    (sums : ∀ x, (members.map (alloc x)).sum = x) (closed net : Int) (given : Nat → Int)
+    (hg : (members.map given).sum = closed) :
+    (members.map (trueUp alloc closed net given)).sum = net := by
+  have h := sum_map_sub (alloc (closed + net)) given members
+  unfold trueUp
+  rw [h, sums, hg]
+  omega
+
+/-- **A running total is one allocation**: after the close, what the count
+has given member `i` is their allocation of everything it closed, so its
+rounding is one allocation's, never a sum of them. -/
+theorem trueUp_running (alloc : Int → Nat → Int) (closed net : Int) (given : Nat → Int)
+    (i : Nat) : given i + trueUp alloc closed net given i = alloc (closed + net) i := by
+  unfold trueUp
+  omega
+
+/-- The run rule is the special case `given = alloc closed`. -/
+theorem closePart_eq_trueUp (alloc : Int → Nat → Int) (before net : Int) (i : Nat) :
+    closePart alloc before net i = trueUp alloc before net (alloc before) i := rfl
+
+/-- **Bounded drift, for any history**: when every allocation is under one
+unit from exact (scaled by `W`, the shares being `w i / W`), so is every
+member's running total after a cumulative close, whatever the earlier
+closes gave (`Apportion.allocW_drift` supplies the hypothesis). -/
+theorem cumulative_drift (alloc : Int → Nat → Int) (w : Nat → Int) (W : Int)
+    (hd : ∀ x i, -W < alloc x i * W - x * w i ∧ alloc x i * W - x * w i < W)
+    (closed net : Int) (given : Nat → Int) (i : Nat) :
+    -W < (given i + trueUp alloc closed net given i) * W - (closed + net) * w i ∧
+    (given i + trueUp alloc closed net given i) * W - (closed + net) * w i < W := by
+  rw [trueUp_running]
+  exact hd _ _
+
+/-- The statement of members' equity's share of the earnings `U` not yet
+closed, as of a day: what the count's next close would give of them, its
+allocation of `closed + U` less its allocation of `closed` (D-38; P3 review
+R-1: never the true-up a close hasn't posted). -/
+def unclosedShare (alloc : Int → Nat → Int) (closed U : Int) (i : Nat) : Int :=
+  alloc (closed + U) i - alloc closed i
+
+/-- **Closing a period moves a member's capital on a day by exactly the
+true-up the close posts** (D-38, R-1): before, their capital `cap` plus
+their share of the unclosed `U`; after closing `net` of it, `cap` plus the
+close's part plus their share of the rest. The difference is
+`alloc closed i - given i`. -/
+theorem statement_after_close (alloc : Int → Nat → Int) (cap closed net U : Int)
+    (given : Nat → Int) (i : Nat) :
+    cap + trueUp alloc closed net given i + unclosedShare alloc (closed + net) (U - net) i
+      = cap + unclosedShare alloc closed U i + (alloc closed i - given i) := by
+  unfold trueUp unclosedShare
+  rw [show closed + net + (U - net) = closed + U by omega]
+  omega
+
+/-- **A member's capital on a day never moves when its period is closed**
+(D-38), once the count's closes gave what the cumulative rule gives
+(`given = alloc closed`: every count the rule began, and every count after
+its first close that posts). -/
+theorem statement_unmoved_by_close (alloc : Int → Nat → Int) (cap closed net U : Int)
+    (i : Nat) :
+    cap + trueUp alloc closed net (alloc closed) i + unclosedShare alloc (closed + net) (U - net) i
+      = cap + unclosedShare alloc closed U i := by
+  rw [statement_after_close]
+  omega
+
+end Bookspec
diff --git a/bookspec/lean/Bookspec/Entry.lean b/bookspec/lean/Bookspec/Entry.lean
new file mode 100644
index 0000000..8edb3f8
--- /dev/null
+++ b/bookspec/lean/Bookspec/Entry.lean
@@ -0,0 +1,117 @@
+import Bookspec.Basic
+
+/-!
+# Entries: acceptance, movements, reversals
+
+Mirrors `kernel::check_lines`, `kernel::movements`, `kernel::reversal`,
+and `JournalEntry::validate`.
+-/
+
+namespace Bookspec
+
+/-- What the engine accepts (the arithmetic of `JournalEntry::validate`,
+i.e. `kernel::check_lines`): two or more lines, every amount positive,
+debits equal to credits. (Range, account, and currency checks are not
+arithmetic laws and are left out of the model.) -/
+def Accepted (ls : List Line) : Prop :=
+  2 ≤ ls.length ∧ (∀ l ∈ ls, 0 < l.amount) ∧ debits ls = credits ls
+
+/-- **Every accepted entry nets to zero.** -/
+theorem Accepted.net_zero {ls : List Line} (h : Accepted ls) : net ls = 0 := by
+  rw [net_eq_debits_sub_credits]; have := h.2.2; omega
+
+/-- Net movement of account `a` over some lines. -/
+def movement (a : Nat) : List Line → Int
+  | [] => 0
+  | l :: ls => (if l.account = a then l.signed else 0) + movement a ls
+
+@[simp] theorem movement_nil (a : Nat) : movement a [] = 0 := rfl
+@[simp] theorem movement_cons (a : Nat) (l : Line) (ls : List Line) :
+    movement a (l :: ls) = (if l.account = a then l.signed else 0) + movement a ls := rfl
+
+theorem movement_append (a : Nat) (xs ys : List Line) :
+    movement a (xs ++ ys) = movement a xs + movement a ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, movement_cons, ih]; omega
+
+/-- **Movements partition the net.** Summed over a chart's distinct codes
+that cover every line's account, the per-account movements add up to the
+net of the lines: grouping by account loses and invents nothing. -/
+theorem sum_movements (as : List Nat) (hd : Distinct as) :
+    ∀ ls : List Line, (∀ l ∈ ls, l.account ∈ as) →
+      sumOver (fun a => movement a ls) as = net ls := by
+  intro ls
+  induction ls with
+  | nil => intro _; simpa using sumOver_zero as
+  | cons l ls ih =>
+    intro hcov
+    simp only [movement_cons, net_cons]
+    rw [sumOver_add, ih (fun m hm => hcov m (List.mem_cons_of_mem _ hm)),
+      sumOver_indicator l.account l.signed as hd (hcov l (List.mem_cons_self ..))]
+
+/-- So the movements of an accepted entry sum to zero. -/
+theorem Accepted.movements_sum_zero {ls : List Line} (h : Accepted ls) (as : List Nat)
+    (hd : Distinct as) (hcov : ∀ l ∈ ls, l.account ∈ as) :
+    sumOver (fun a => movement a ls) as = 0 := by
+  rw [sum_movements as hd ls hcov, h.net_zero]
+
+/-! ## Reversals -/
+
+/-- A line with its side flipped. -/
+def Line.reverse (l : Line) : Line := { l with side := l.side.flip }
+
+/-- A reversing entry's lines (`kernel::reversal`). -/
+def reversal (ls : List Line) : List Line := ls.map Line.reverse
+
+theorem Line.reverse_signed (l : Line) : l.reverse.signed = -l.signed := by
+  simp [Line.reverse, Line.signed, signed_flip]
+
+theorem net_reversal (ls : List Line) : net (reversal ls) = -net ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    simp only [net_cons, ih, Line.reverse_signed]; omega
+
+theorem movement_reversal (a : Nat) (ls : List Line) :
+    movement a (reversal ls) = -movement a ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    simp only [movement_cons, ih, Line.reverse_signed]
+    by_cases h : l.account = a <;> simp [Line.reverse, h] <;> omega
+
+/-- **An entry and its reversal net every account to zero.** -/
+theorem movement_with_reversal (a : Nat) (ls : List Line) :
+    movement a (ls ++ reversal ls) = 0 := by
+  rw [movement_append, movement_reversal]; omega
+
+theorem debits_reversal (ls : List Line) : debits (reversal ls) = credits ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    obtain ⟨a, s, m⟩ := l
+    cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih]
+
+theorem credits_reversal (ls : List Line) : credits (reversal ls) = debits ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    obtain ⟨a, s, m⟩ := l
+    cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih]
+
+/-- **A reversal is accepted exactly when the original is.** -/
+theorem accepted_reversal_iff (ls : List Line) : Accepted (reversal ls) ↔ Accepted ls := by
+  unfold Accepted
+  rw [debits_reversal, credits_reversal]
+  have hlen : (reversal ls).length = ls.length := List.length_map ..
+  have hpos : (∀ l ∈ reversal ls, 0 < l.amount) ↔ (∀ l ∈ ls, 0 < l.amount) := by
+    simp [reversal, Line.reverse]
+  rw [hlen, hpos]
+  constructor <;> rintro ⟨a, b, c⟩ <;> exact ⟨a, b, c.symm⟩
+
+end Bookspec
diff --git a/bookspec/lean/Bookspec/Laws.lean b/bookspec/lean/Bookspec/Laws.lean
new file mode 100644
index 0000000..9669a64
--- /dev/null
+++ b/bookspec/lean/Bookspec/Laws.lean
@@ -0,0 +1,62 @@
+import Bookspec.Ledger
+
+/-!
+# bookspec's five laws
+
+The five laws of the first edition (`bookspec/spec/00-model.md`, "The five
+laws"), each stated once, by name, as a theorem about *every* reachable
+state of the books, ported from `verify/lean` (P13 step 4). Money is `Int`,
+an exact count of the smallest unit; any finite set of exact decimals
+scales to integers without loss, and every law is a law of addition.
+
+1. Debits equal credits (BS-entry-1).
+2. Assets = Liabilities + Equity + (Revenue - Expenses) (BS-statement-2).
+3. The trial balance balances (BS-statement-1).
+4. Net income articulates to equity: a close credits equity with exactly
+   revenue less expenses (BS-period-1).
+5. The cash-flow sections sum to the change in cash (BS-statement-3).
+-/
+
+namespace Bookspec
+
+/-- Law 1. In every reachable state the posted lines' debits equal their
+credits (`net` is debits less credits). -/
+theorem law_debits_equal_credits {L : Ledger} (r : Reachable L) :
+    net (allLines L.posted) = 0 :=
+  r.books_net_zero
+
+/-- Law 2. The accounting equation, in every reachable state. -/
+theorem law_accounting_equation {L : Ledger} (r : Reachable L) :
+    let ls := allLines L.posted
+    typeTotal .asset ls L.chart
+      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
+        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
+  r.accounting_equation
+
+/-- Law 3. The trial balance balances, in every reachable state. -/
+theorem law_trial_balance {L : Ledger} (r : Reachable L) :
+    tbDebits (allLines L.posted) (codes L.chart)
+      = tbCredits (allLines L.posted) (codes L.chart) :=
+  r.trial_balance
+
+/-- Law 4. A close credits equity with exactly the period's net income. -/
+theorem law_net_income_articulates (L : Ledger) (p : Period) (ts : List (Nat × Int))
+    (hsum : total (ts.map Prod.snd)
+      = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) :
+    let ls := allLines (through p.stop L.posted)
+    total (ts.map Prod.snd) = typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart :=
+  close_credits_net_income L p ts hsum
+
+/-- Law 5. The three sections of the statement of cash flows sum to the
+change in the cash accounts. -/
+theorem law_cash_flow_is_change_in_cash {L : Ledger} (r : Reachable L) (b c : Nat)
+    (hbc : b ≤ c) (F : List Line → Line → Flow) (C : List Line → List Int)
+    (hC : ∀ e, sum3 (C e) = 0) (cash : List Nat) (hd : Distinct cash)
+    (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    let es := (between b c L.posted).map Entry.lines
+    sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es
+      = sumOver (fun a => movement a (allLines (through c L.posted))) cash
+        - sumOver (fun a => movement a (allLines (through b L.posted))) cash :=
+  r.cashflow_is_change_in_cash b c hbc F C hC cash hd hF
+
+end Bookspec
diff --git a/bookspec/lean/Bookspec/Ledger.lean b/bookspec/lean/Bookspec/Ledger.lean
new file mode 100644
index 0000000..d3ee8c7
--- /dev/null
+++ b/bookspec/lean/Bookspec/Ledger.lean
@@ -0,0 +1,562 @@
+import Bookspec.Closing
+
+/-!
+# The ledger as a state machine
+
+The engine's command surface (`Ledger`), modelled as the steps it allows:
+add an account, start a draft, post, reverse, open a period, close one.
+Each step carries the checks the engine makes before it mutates. The
+theorems below hold in *every* state reachable from empty books, by any
+sequence of commands, of any length.
+
+Mirrors `Ledger::add_account`, `try_create_entry`, `post_entry`,
+`reverse_entry`, `create_period`, and `close_period_to`; and, as one step
+`record`, everything the books keep about how they are kept: settings,
+conventions, decisions, open items and approvals (`apply_settings`,
+`apply_convention`, `apply_decision`, `apply_open_item`,
+`apply_approval`, and their retirements and resolutions), each a record
+the step adds and nothing else; and an account's rename
+(`rename_account`, `account.renamed`, rules.md B-31), since the model's
+chart is codes and types and a name is no part of it.
+-/
+
+namespace Bookspec
+
+/-- A journal entry: its id, its date (a day number), its lines. -/
+structure Entry where
+  id : Nat
+  date : Nat
+  lines : List Line
+  deriving DecidableEq
+
+/-- Every line of some entries, in order. -/
+def allLines : List Entry → List Line
+  | [] => []
+  | e :: es => e.lines ++ allLines es
+
+theorem allLines_append (xs ys : List Entry) : allLines (xs ++ ys) = allLines xs ++ allLines ys := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih => simp [allLines, ih]
+
+theorem mem_allLines {l : Line} {es : List Entry} : l ∈ allLines es ↔ ∃ e ∈ es, l ∈ e.lines := by
+  induction es with
+  | nil => simp [allLines]
+  | cons e es ih => simp [allLines, ih]
+
+/-- **Any collection of balanced entries nets to zero**: all of them, those
+dated through some day, those in some period, any filter at all. -/
+theorem net_allLines (es : List Entry) (h : ∀ e ∈ es, net e.lines = 0) : net (allLines es) = 0 := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [allLines, net_append, h e (by simp), ih (fun x hx => h x (by simp [hx]))]
+    rfl
+
+/-- An accounting period: inclusive day range, open or closed. -/
+structure Period where
+  id : Nat
+  start : Nat
+  stop : Nat
+  closed : Bool
+  deriving DecidableEq
+
+/-- Whether a day falls in a period. -/
+def Period.contains (p : Period) (d : Nat) : Bool := decide (p.start ≤ d ∧ d ≤ p.stop)
+
+/-- The books: chart, posted entries in posting order, drafts, periods,
+and the record of how they are kept (settings, conventions, decisions,
+open items, approvals), each record abstracted to a number. -/
+structure Ledger where
+  chart : Chart
+  posted : List Entry
+  drafts : List Entry
+  periods : List Period
+  records : List Nat
+
+/-- Empty books. -/
+def Ledger.empty : Ledger := ⟨[], [], [], [], []⟩
+
+/-- Whether a closed period contains a day. -/
+def Ledger.closedOn (L : Ledger) (d : Nat) : Prop :=
+  ∃ p ∈ L.periods, p.closed = true ∧ p.contains d = true
+
+/-- Entries dated on or before a day. -/
+def through (d : Nat) (es : List Entry) : List Entry := es.filter (fun e => decide (e.date ≤ d))
+
+/-- Mark one period closed. -/
+def closeIn (p : Period) (ps : List Period) : List Period :=
+  ps.map (fun q => if q = p then { q with closed := true } else q)
+
+/-- The closing entry for period `p` crediting targets `ts`, if there is
+anything to close. -/
+def closingFor (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) : List Entry :=
+  if closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) = [] then []
+  else [⟨id, p.stop, closingEntry (nominalCodes L.chart) ts (allLines (through p.stop L.posted))⟩]
+
+/-- What the engine allows. -/
+inductive Step : Ledger → Ledger → Prop
+  /-- `add_account`: codes are unique. -/
+  | addAccount (L : Ledger) (a : Nat) (t : AccountType) (h : a ∉ codes L.chart) :
+      Step L { L with chart := (a, t) :: L.chart }
+  /-- `try_create_entry` (and lines added to it): not in a closed period. -/
+  | draft (L : Ledger) (e : Entry) (h : ¬ L.closedOn e.date) :
+      Step L { L with drafts := e :: L.drafts }
+  /-- `post_entry`: a draft, acceptable, on known accounts, not in a closed
+  period. Appends to the log. -/
+  | post (L : Ledger) (e : Entry) (hd : e ∈ L.drafts) (ha : Accepted e.lines)
+      (hk : ∀ l ∈ e.lines, l.account ∈ codes L.chart) (hc : ¬ L.closedOn e.date) :
+      Step L { L with posted := L.posted ++ [e], drafts := L.drafts.filter (· ≠ e) }
+  /-- `reverse_entry`: a posted entry's lines, sides flipped, posted on a
+  day not in a closed period. -/
+  | reverse (L : Ledger) (e : Entry) (he : e ∈ L.posted) (r : Entry)
+      (hr : r.lines = reversal e.lines) (hc : ¬ L.closedOn r.date) :
+      Step L { L with posted := L.posted ++ [r] }
+  /-- `create_period`: periods open. -/
+  | openPeriod (L : Ledger) (p : Period) (h : p.closed = false) :
+      Step L { L with periods := p :: L.periods }
+  /-- `close_period_to`: an open period with no drafts in it, whose last day
+  is in no other closed period, with no later period closed, crediting the
+  net income to equity targets (not themselves revenue or expense) in
+  parts that sum to it. -/
+  | close (L : Ledger) (p : Period) (hp : p ∈ L.periods) (hopen : p.closed = false)
+      (hdrafts : ∀ d ∈ L.drafts, p.contains d.date = false)
+      (hother : ∀ q ∈ L.periods, q.closed = true → q.contains p.stop = false)
+      (hlater : ∀ q ∈ L.periods, q.closed = true → q.stop ≤ p.stop)
+      (ts : List (Nat × Int))
+      (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
+      (hsum : total (ts.map Prod.snd)
+        = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted))))
+      (id : Nat) :
+      Step L { L with posted := L.posted ++ closingFor L p ts id, periods := closeIn p L.periods }
+  /-- `apply_settings`, `apply_convention`, `apply_decision`,
+  `apply_open_item`, `apply_approval` and their retirements and
+  resolutions, and the 1099 records `set_vendor_1099`,
+  `set_vendor_w9_flag`, `add_instrument` and `set_entry_instrument`: a
+  record of how the books are kept, and nothing else. `rename_account`
+  too: a name is outside the chart the model keeps. -/
+  | record (L : Ledger) (r : Nat) : Step L { L with records := r :: L.records }
+
+/-- States reachable from empty books. -/
+inductive Reachable : Ledger → Prop
+  | empty : Reachable Ledger.empty
+  | step {L L' : Ledger} : Reachable L → Step L L' → Reachable L'
+
+/-- What holds in every reachable state. -/
+structure Inv (L : Ledger) : Prop where
+  distinct : Distinct (codes L.chart)
+  accepted : ∀ e ∈ L.posted, Accepted e.lines
+  known : ∀ e ∈ L.posted, ∀ l ∈ e.lines, l.account ∈ codes L.chart
+  draftsOpen : ∀ d ∈ L.drafts, ¬ L.closedOn d.date
+
+theorem closedOn_closeIn (L : Ledger) (p : Period) (d : Nat) :
+    ({ L with periods := closeIn p L.periods } : Ledger).closedOn d →
+      L.closedOn d ∨ (p ∈ L.periods ∧ p.contains d = true) := by
+  rintro ⟨q, hq, hc, hd⟩
+  simp only [closeIn, List.mem_map] at hq
+  obtain ⟨q', hq', rfl⟩ := hq
+  by_cases e : q' = p
+  · subst e; right; simp at hd; exact ⟨hq', by simpa [Period.contains] using hd⟩
+  · left; simp [e] at hc hd; exact ⟨q', hq', hc, hd⟩
+
+theorem closingFor_lines (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) :
+    ∀ e ∈ closingFor L p ts id,
+      e.date = p.stop ∧ e.lines = closingEntry (nominalCodes L.chart) ts
+        (allLines (through p.stop L.posted))
+      ∧ closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) ≠ [] := by
+  intro e he
+  unfold closingFor at he
+  split at he
+  · simp at he
+  · simp at he; subst he; exact ⟨rfl, rfl, by assumption⟩
+
+/-- **Every step preserves the invariant.** -/
+theorem Step.inv {L L' : Ledger} (s : Step L L') (h : Inv L) : Inv L' := by
+  cases s with
+  | addAccount a t ha =>
+    exact ⟨⟨ha, h.distinct⟩, h.accepted,
+      fun e he l hl => List.mem_cons_of_mem _ (h.known e he l hl), h.draftsOpen⟩
+  | draft e hc =>
+    refine ⟨h.distinct, h.accepted, h.known, ?_⟩
+    intro d hd
+    cases hd with
+    | head => exact hc
+    | tail _ hd => exact h.draftsOpen d hd
+  | post e hd ha hk hc =>
+    refine ⟨h.distinct, ?_, ?_, ?_⟩
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.accepted x hx
+      · exact ha
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.known x hx
+      · exact hk
+    · intro d hd
+      exact h.draftsOpen d ((List.mem_filter.1 hd).1)
+  | reverse e he r hr hc =>
+    refine ⟨h.distinct, ?_, ?_, h.draftsOpen⟩
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.accepted x hx
+      · rw [hr, accepted_reversal_iff]; exact h.accepted e he
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.known x hx
+      · intro l hl
+        rw [hr] at hl
+        simp only [reversal, List.mem_map] at hl
+        obtain ⟨l', hl', rfl⟩ := hl
+        exact h.known e he l' hl'
+  | openPeriod p hp =>
+    refine ⟨h.distinct, h.accepted, h.known, ?_⟩
+    rintro d hd ⟨q, hq, hc, hdq⟩
+    cases hq with
+    | head => simp [hp] at hc
+    | tail _ hq => exact h.draftsOpen d hd ⟨q, hq, hc, hdq⟩
+  | close p hp hopen hdrafts hother hlater ts hts hsum id =>
+    refine ⟨h.distinct, ?_, ?_, ?_⟩
+    · intro x hx
+      simp only [List.mem_append] at hx
+      rcases hx with hx | hx
+      · exact h.accepted x hx
+      · obtain ⟨-, hl, hne⟩ := closingFor_lines L p ts id x hx
+        rw [hl]; exact closingEntry_accepted _ _ _ hsum hne
+    · intro x hx
+      simp only [List.mem_append] at hx
+      rcases hx with hx | hx
+      · exact h.known x hx
+      · obtain ⟨-, hl, -⟩ := closingFor_lines L p ts id x hx
+        intro l hl'
+        rw [hl] at hl'
+        simp only [closingEntry, List.mem_append] at hl'
+        rcases hl' with hl' | hl'
+        · exact nominalCodes_sub _ _ (closings_account _ _ l hl')
+        · obtain ⟨y, hy, e⟩ := equityLines_account ts l hl'
+          rw [e]; exact (hts y hy).1
+    · intro d hd hcl
+      rcases closedOn_closeIn L p d.date hcl with hcl | ⟨-, hc⟩
+      · exact h.draftsOpen d hd hcl
+      · simp [hdrafts d hd] at hc
+  | record r => exact ⟨h.distinct, h.accepted, h.known, h.draftsOpen⟩
+
+/-- **The invariant holds in every reachable state.** -/
+theorem Reachable.inv {L : Ledger} (r : Reachable L) : Inv L := by
+  induction r with
+  | empty => exact ⟨trivial, by simp [Ledger.empty], by simp [Ledger.empty], by simp [Ledger.empty]⟩
+  | step _ s ih => exact s.inv ih
+
+/-! ## The books always balance -/
+
+/-- **The books net to zero**: in every reachable state, the posted lines'
+debits equal their credits. -/
+theorem Reachable.books_net_zero {L : Ledger} (r : Reachable L) : net (allLines L.posted) = 0 :=
+  net_allLines _ (fun e he => (r.inv.accepted e he).net_zero)
+
+/-- The same through any day: the books as of any date balance too. -/
+theorem Reachable.net_zero_through {L : Ledger} (r : Reachable L) (d : Nat) :
+    net (allLines (through d L.posted)) = 0 :=
+  net_allLines _ (fun e he => (r.inv.accepted e ((List.mem_filter.1 he).1)).net_zero)
+
+theorem Reachable.covers {L : Ledger} (r : Reachable L) (es : List Entry)
+    (hs : ∀ e ∈ es, e ∈ L.posted) : ∀ l ∈ allLines es, l.account ∈ codes L.chart := by
+  intro l hl
+  obtain ⟨e, he, hl⟩ := mem_allLines.1 hl
+  exact r.inv.known e (hs e he) l hl
+
+/-- **The trial balance balances**, in every reachable state. -/
+theorem Reachable.trial_balance {L : Ledger} (r : Reachable L) :
+    tbDebits (allLines L.posted) (codes L.chart) = tbCredits (allLines L.posted) (codes L.chart) :=
+  trial_balance_balances _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero
+
+/-- **The trial balance as of any date balances.** -/
+theorem Reachable.trial_balance_through {L : Ledger} (r : Reachable L) (d : Nat) :
+    tbDebits (allLines (through d L.posted)) (codes L.chart)
+      = tbCredits (allLines (through d L.posted)) (codes L.chart) :=
+  trial_balance_balances _ _ r.inv.distinct
+    (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)
+
+/-- **The accounting equation holds**, in every reachable state:
+Assets = Liabilities + Equity + (Revenue - Expenses). -/
+theorem Reachable.accounting_equation {L : Ledger} (r : Reachable L) :
+    let ls := allLines L.posted
+    typeTotal .asset ls L.chart
+      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
+        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
+  Bookspec.accounting_equation _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero
+
+/-- **The balance sheet as of any date balances.** -/
+theorem Reachable.accounting_equation_through {L : Ledger} (r : Reachable L) (d : Nat) :
+    let ls := allLines (through d L.posted)
+    typeTotal .asset ls L.chart
+      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
+        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
+  Bookspec.accounting_equation _ _ r.inv.distinct
+    (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)
+
+/-! ## Posted is forever -/
+
+/-- **Posting only appends.** No step edits, reorders, or removes a posted
+entry. -/
+theorem Step.extends {L L' : Ledger} (s : Step L L') : ∃ t, L'.posted = L.posted ++ t := by
+  cases s with
+  | addAccount => exact ⟨[], by simp⟩
+  | draft => exact ⟨[], by simp⟩
+  | post e => exact ⟨[e], rfl⟩
+  | reverse e _ r => exact ⟨[r], rfl⟩
+  | openPeriod => exact ⟨[], by simp⟩
+  | close p _ _ _ _ _ ts _ _ id => exact ⟨closingFor L p ts id, rfl⟩
+  | record => exact ⟨[], by simp⟩
+
+/-- Any number of steps. -/
+inductive Steps : Ledger → Ledger → Prop
+  | refl (L : Ledger) : Steps L L
+  | tail {L M N : Ledger} : Steps L M → Step M N → Steps L N
+
+/-- **Posted is forever**: after any sequence of commands, the old log is
+a prefix of the new one. Every posted entry keeps its place and its
+lines. -/
+theorem Steps.extends {L L' : Ledger} (s : Steps L L') : ∃ t, L'.posted = L.posted ++ t := by
+  induction s with
+  | refl => exact ⟨[], by simp⟩
+  | tail _ s ih =>
+    obtain ⟨t, ht⟩ := ih
+    obtain ⟨u, hu⟩ := s.extends
+    exact ⟨t ++ u, by rw [hu, ht, List.append_assoc]⟩
+
+/-! ## Closed periods are frozen -/
+
+/-- Entries dated in a period. -/
+def within (p : Period) (es : List Entry) : List Entry := es.filter (fun e => p.contains e.date)
+
+theorem within_append (p : Period) (xs ys : List Entry) :
+    within p (xs ++ ys) = within p xs ++ within p ys := List.filter_append ..
+
+/-- A closed period stays closed. -/
+theorem Step.keeps_closed {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
+    (hc : q.closed = true) : q ∈ L'.periods := by
+  cases s with
+  | openPeriod p _ => exact List.mem_cons_of_mem _ hq
+  | close p _ hopen =>
+    have : q ≠ p := fun e => by subst e; simp [hopen] at hc
+    exact List.mem_map.2 ⟨q, hq, by simp [this]⟩
+  | _ => exact hq
+
+/-- **A step never changes what a closed period contains.** -/
+theorem Step.frozen {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
+    (hc : q.closed = true) : within q L'.posted = within q L.posted := by
+  have nothing : ∀ e : Entry, ¬ L.closedOn e.date → within q [e] = [] := by
+    intro e he
+    simp only [within, List.filter_cons, List.filter_nil]
+    split
+    · exact absurd ⟨q, hq, hc, by assumption⟩ he
+    · rfl
+  cases s with
+  | post e _ _ _ hcl => rw [within_append, nothing e hcl, List.append_nil]
+  | reverse e _ r _ hcl => rw [within_append, nothing r hcl, List.append_nil]
+  | close p hp hopen hdrafts hother hlater ts hts hsum id =>
+    rw [within_append]
+    have : within q (closingFor L p ts id) = [] := by
+      unfold closingFor
+      split
+      · rfl
+      · simp only [within, List.filter_cons, List.filter_nil]
+        rw [hother q hq hc]; rfl
+    rw [this, List.append_nil]
+  | _ => rfl
+
+/-- **Closed periods are frozen**: once a period is closed, no sequence of
+commands adds, removes, or changes an entry dated in it. -/
+theorem Steps.frozen {L L' : Ledger} (s : Steps L L') (q : Period) (hq : q ∈ L.periods)
+    (hc : q.closed = true) : within q L'.posted = within q L.posted ∧ q ∈ L'.periods := by
+  induction s with
+  | refl => exact ⟨rfl, hq⟩
+  | tail _ s ih =>
+    obtain ⟨h1, h2⟩ := ih
+    exact ⟨(s.frozen q h2 hc).trans h1, s.keeps_closed q h2 hc⟩
+
+/-! ## Closing -/
+
+/-- **After a close, every revenue and expense account is zero through the
+period's last day.** (The trial balance still balances: the close is a
+step, and `Reachable.trial_balance` covers every step.) -/
+theorem close_zeroes {L : Ledger} (r : Reachable L) (p : Period)
+    (ts : List (Nat × Int)) (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
+    (id : Nat) (a : Nat) (ha : a ∈ nominalCodes L.chart) :
+    movement a (allLines (through p.stop (L.posted ++ closingFor L p ts id))) = 0 := by
+  have hd := nominalCodes_distinct _ r.inv.distinct
+  have hta : ∀ x ∈ ts, x.1 ≠ a := fun x hx e => (hts x hx).2 (e ▸ ha)
+  rw [through, List.filter_append, ← through, allLines_append]
+  unfold closingFor
+  split
+  · rename_i hnil
+    simp only [List.filter_nil, allLines, List.append_nil]
+    exact closings_eq_nil _ _ hnil a ha
+  · simp only [List.filter_cons, Nat.le_refl, decide_true, ite_true, List.filter_nil, allLines,
+      List.append_nil]
+    exact closingEntry_zeroes _ ts _ hd a ha hta
+
+/-- **A close credits equity with exactly the period's net income**:
+revenue minus expenses through its last day, split among the targets. -/
+theorem close_credits_net_income (L : Ledger) (p : Period) (ts : List (Nat × Int))
+    (hsum : total (ts.map Prod.snd)
+      = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) :
+    let ls := allLines (through p.stop L.posted)
+    total (ts.map Prod.snd) = typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart := by
+  intro ls
+  rw [hsum, net_closings_is_net_income]
+
+/-! ## Period statements add up -/
+
+/-- Entries dated after day `b`, through day `c`. -/
+def between (b c : Nat) (es : List Entry) : List Entry :=
+  es.filter (fun e => decide (b < e.date ∧ e.date ≤ c))
+
+theorem movement_split (a b c : Nat) (h : b ≤ c) (es : List Entry) :
+    movement a (allLines (through c es))
+      = movement a (allLines (through b es)) + movement a (allLines (between b c es)) := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [through, between] at ih ⊢
+    by_cases h1 : e.date ≤ b
+    · have h2 : e.date ≤ c := by omega
+      have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
+      rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_pos (by simpa using h1),
+        List.filter_cons_of_neg (by simpa using h3)]
+      simp only [allLines, movement_append, ih]; omega
+    · by_cases h2 : e.date ≤ c
+      · have h3 : b < e.date ∧ e.date ≤ c := by omega
+        rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
+          List.filter_cons_of_pos (by simpa using h3)]
+        simp only [allLines, movement_append, ih]; omega
+      · have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
+        rw [List.filter_cons_of_neg (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
+          List.filter_cons_of_neg (by simpa using h3)]
+        exact ih
+
+theorem typeTotal_split (t : AccountType) (x y z : List Line)
+    (h : ∀ a, movement a x = movement a y + movement a z) (c : Chart) :
+    typeTotal t x c = typeTotal t y c + typeTotal t z c := by
+  induction c with
+  | nil => rfl
+  | cons p c ih =>
+    obtain ⟨a, t'⟩ := p
+    simp only [typeTotal, h a, ih]
+    split
+    · cases t' <;> simp [balance, AccountType.normal, signed] <;> omega
+    · omega
+
+/-- **Period statements add up**: every account type's total (so revenue,
+expenses, and net income) through day `c` is its total through day `b`
+plus its total for the days after `b` through `c`. A year's P&L is the sum
+of its months'. -/
+theorem statements_add_up (t : AccountType) (b c : Nat) (h : b ≤ c) (es : List Entry)
+    (chart : Chart) :
+    typeTotal t (allLines (through c es)) chart
+      = typeTotal t (allLines (through b es)) chart
+        + typeTotal t (allLines (between b c es)) chart :=
+  typeTotal_split t _ _ _ (fun a => movement_split a b c h es) chart
+
+/-! ## The statement of cash flows foots (rules.md B-14 rule 9) -/
+
+/-- Some entries' cash, summed, is the movement of the cash accounts over
+their lines, when the cash tag follows the account. -/
+theorem cashTotal_is_movement (F : List Line → Line → Flow) (cash : List Nat)
+    (hd : Distinct cash) (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    ∀ xs : List Entry,
+      cashTotal F (xs.map Entry.lines) = sumOver (fun a => movement a (allLines xs)) cash := by
+  intro xs
+  induction xs with
+  | nil => simpa [cashTotal, allLines] using (sumOver_zero cash).symm
+  | cons x xs ih =>
+    simp only [List.map_cons, cashTotal, allLines, movement_append]
+    rw [sumOver_add, ← ih, cashOf, secNet_cash_is_movement (F x.lines) cash hd (hF x.lines)]
+
+/-- **The statement of cash flows foots**, in every reachable state: over
+the posted entries dated after day `b` through day `c` (any selection of
+them, `p`: the engine leaves out closing entries), operating + investing +
+financing is the movement of the cash accounts over the same entries, for
+any tagging whose cash tag follows the account, and whatever a member or
+lender handled for each entry (`C`, rule 11) as long as it nets to zero
+(`constructive_nets`). Every posted entry is accepted (`Reachable.inv`),
+so each nets to zero. -/
+theorem Reachable.cashflow_foots {L : Ledger} (r : Reachable L) (b c : Nat) (p : Entry → Bool)
+    (F : List Line → Line → Flow) (C : List Line → List Int) (hC : ∀ e, sum3 (C e) = 0)
+    (cash : List Nat) (hd : Distinct cash)
+    (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    let xs := (between b c L.posted).filter p
+    sectionTotal F C 0 (xs.map Entry.lines) + sectionTotal F C 1 (xs.map Entry.lines)
+        + sectionTotal F C 2 (xs.map Entry.lines)
+      = sumOver (fun a => movement a (allLines xs)) cash := by
+  intro xs
+  rw [cashflow_sections_sum_to_cash_change, cashTotal_is_movement F cash hd hF]
+  · intro e he
+    obtain ⟨x, hx, rfl⟩ := List.mem_map.1 he
+    have hb := (List.mem_filter.1 hx).1
+    exact (r.inv.accepted x (List.mem_filter.1 hb).1).net_zero
+  · exact fun e _ => hC e
+
+/-- **The sections are the change in the cash accounts' balances**: with
+every entry between `b` and `c` counted, the three sections sum to the
+cash accounts' movement through `c` less their movement through `b`
+(their ending balance less their beginning balance). -/
+theorem Reachable.cashflow_is_change_in_cash {L : Ledger} (r : Reachable L) (b c : Nat)
+    (hbc : b ≤ c) (F : List Line → Line → Flow) (C : List Line → List Int)
+    (hC : ∀ e, sum3 (C e) = 0) (cash : List Nat) (hd : Distinct cash)
+    (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    let es := (between b c L.posted).map Entry.lines
+    sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es
+      = sumOver (fun a => movement a (allLines (through c L.posted))) cash
+        - sumOver (fun a => movement a (allLines (through b L.posted))) cash := by
+  intro es
+  have h := r.cashflow_foots b c (fun _ => true) F C hC cash hd hF
+  have hall : (between b c L.posted).filter (fun _ => true) = between b c L.posted :=
+    List.filter_eq_self.2 (fun _ _ => rfl)
+  simp only [hall] at h
+  rw [h]
+  have hs : ∀ a, movement a (allLines (through c L.posted))
+      = movement a (allLines (through b L.posted)) + movement a (allLines (between b c L.posted)) :=
+    fun a => movement_split a b c hbc L.posted
+  rw [sumOver_congr _ _ cash (fun a _ => hs a), sumOver_add]
+  omega
+
+/-- **A reversal and its original in one period drop out together**: for
+an entry and its reversal (lines flipped, tagged as the original's, and
+what was handled for it mirrored, `constructive_neg`), the sum of their
+flows in each section is zero. -/
+theorem cashflow_reversal_nets (F : List Line → Line → Flow) (C : List Line → List Int)
+    (e : List Line) (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l)
+    (hC : C (reversal e) = (C e).map (fun x => -x)) (k : Nat) :
+    sectionTotal F C k [e, reversal e] = 0 := by
+  simp only [sectionTotal, stmt_flows_reversal F C e hF hC, getD_neg]
+  omega
+
+/-! ## How the books are kept changes no figure -/
+
+/-- **A record changes nothing the books hold**: a settings change, a
+convention, a decision, an open item or an approval leaves the chart, every
+posted entry, every draft and every period exactly as they were. (The
+`record` step touches only `records` by definition: this pins the model.
+The engine's side is checked in Rust by `settings_replay_is_pure`.
+Settings that change how the same entries are presented, such as the
+fiscal year, are outside the model.) -/
+theorem Step.record_changes_no_figure (L : Ledger) (r : Nat) :
+    let L' : Ledger := { L with records := r :: L.records }
+    L'.chart = L.chart ∧ L'.posted = L.posted ∧ L'.drafts = L.drafts ∧ L'.periods = L.periods :=
+  ⟨rfl, rfl, rfl, rfl⟩
+
+/-- **Any number of records changes no figure**, and they keep the
+invariant: a reachable state plus records is reachable, with the same
+books. -/
+theorem Reachable.records {L : Ledger} (h : Reachable L) (rs : List Nat) :
+    Reachable { L with records := rs ++ L.records } := by
+  induction rs with
+  | nil => simpa using h
+  | cons r rs ih => exact Reachable.step ih (Step.record _ r)
+
+end Bookspec
diff --git a/bookspec/lean/Bookspec/Statements.lean b/bookspec/lean/Bookspec/Statements.lean
new file mode 100644
index 0000000..011e4a3
--- /dev/null
+++ b/bookspec/lean/Bookspec/Statements.lean
@@ -0,0 +1,683 @@
+import Bookspec.Entry
+
+/-!
+# Balances and statements
+
+Mirrors `kernel::normal_balance`, `kernel::columns`,
+`Ledger::account_balance`, and `reports::trial_balance`; and the statement
+of cash flows (`kernel::take`, `kernel::apply_cash`, `kernel::entry_flows`,
+`kernel::constructive`, `cashflow::cash_flow`'s footing and reconciliation
+checks).
+-/
+
+namespace Bookspec
+
+/-- A chart of accounts: each account's code and type. -/
+abbrev Chart := List (Nat × AccountType)
+
+/-- The chart's codes. -/
+def codes (c : Chart) : List Nat := c.map Prod.fst
+
+@[simp] theorem codes_nil : codes [] = [] := rfl
+@[simp] theorem codes_cons (a : Nat) (t : AccountType) (c : Chart) :
+    codes ((a, t) :: c) = a :: codes c := rfl
+
+/-- An account's balance on its normal side (`kernel::normal_balance`). -/
+def balance (t : AccountType) (m : Int) : Int := signed t.normal m
+
+/-- **A normal-side line raises a balance by its amount; an opposite-side
+line lowers it.** -/
+theorem balance_after_line (t : AccountType) (m : Int) (s : Side) (a : Int) :
+    balance t (m + signed s a) = balance t m + (if s = t.normal then a else -a) := by
+  cases t <;> cases s <;> simp [balance, AccountType.normal, signed] <;> omega
+
+/-- The total balance of every account of type `t`. -/
+def typeTotal (t : AccountType) (ls : List Line) : Chart → Int
+  | [] => 0
+  | (a, t') :: rest => (if t' = t then balance t' (movement a ls) else 0) + typeTotal t ls rest
+
+/-- The accounting equation's two sides differ by the net movement of the
+chart's accounts. -/
+theorem equation_gap (ls : List Line) (c : Chart) :
+    typeTotal .asset ls c + typeTotal .expense ls c
+      - typeTotal .liability ls c - typeTotal .equity ls c - typeTotal .revenue ls c
+      = sumOver (fun a => movement a ls) (codes c) := by
+  induction c with
+  | nil => rfl
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    cases t <;> simp [typeTotal, balance, AccountType.normal, signed] <;> omega
+
+/-- **The accounting equation.** For lines that net to zero, over a chart
+with distinct codes covering every line's account:
+Assets = Liabilities + Equity + (Revenue - Expenses). -/
+theorem accounting_equation (ls : List Line) (c : Chart) (hd : Distinct (codes c))
+    (hcov : ∀ l ∈ ls, l.account ∈ codes c) (hnet : net ls = 0) :
+    typeTotal .asset ls c
+      = typeTotal .liability ls c + typeTotal .equity ls c
+        + (typeTotal .revenue ls c - typeTotal .expense ls c) := by
+  have := equation_gap ls c
+  rw [sum_movements _ hd ls hcov, hnet] at this
+  omega
+
+/-! ## Trial balance -/
+
+/-- The debit column for a movement (`kernel::columns`). -/
+def colDebit (m : Int) : Int := if 0 < m then m else 0
+/-- The credit column for a movement (`kernel::columns`). -/
+def colCredit (m : Int) : Int := if 0 < m then 0 else -m
+
+theorem columns_spec (m : Int) :
+    0 ≤ colDebit m ∧ 0 ≤ colCredit m ∧ (colDebit m = 0 ∨ colCredit m = 0)
+      ∧ colDebit m - colCredit m = m := by
+  unfold colDebit colCredit; split <;> omega
+
+/-- The trial balance's debit column total. -/
+def tbDebits (ls : List Line) (as : List Nat) : Int := sumOver (fun a => colDebit (movement a ls)) as
+/-- The trial balance's credit column total. -/
+def tbCredits (ls : List Line) (as : List Nat) : Int :=
+  sumOver (fun a => colCredit (movement a ls)) as
+
+theorem tb_gap (ls : List Line) (as : List Nat) :
+    tbDebits ls as - tbCredits ls as = sumOver (fun a => movement a ls) as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [tbDebits, tbCredits, sumOver_cons] at ih ⊢
+    have := (columns_spec (movement a ls)).2.2.2
+    omega
+
+/-- **The trial balance balances** for lines that net to zero. -/
+theorem trial_balance_balances (ls : List Line) (as : List Nat) (hd : Distinct as)
+    (hcov : ∀ l ∈ ls, l.account ∈ as) (hnet : net ls = 0) :
+    tbDebits ls as = tbCredits ls as := by
+  have := tb_gap ls as
+  rw [sum_movements as hd ls hcov, hnet] at this
+  omega
+
+/-- And conversely: a balanced trial balance means the lines net to zero.
+The trial balance is a complete check of the books' arithmetic. -/
+theorem trial_balance_iff (ls : List Line) (as : List Nat) (hd : Distinct as)
+    (hcov : ∀ l ∈ ls, l.account ∈ as) :
+    tbDebits ls as = tbCredits ls as ↔ net ls = 0 := by
+  have := tb_gap ls as
+  rw [sum_movements as hd ls hcov] at this
+  omega
+
+/-! ## The statement of cash flows (rules.md B-14)
+
+Mirrors `kernel::Flow`, `kernel::take`, `kernel::apply_cash` and
+`kernel::entry_flows`, and the identities `cashflow::cash_flow` checks at
+runtime: the sections sum to the cash accounts' change, a reversal's flows
+are its original's negated, and net income reconciles to operating cash.
+
+Lines are tagged per entry (`F : List Line → Line → Flow`), as the engine
+tags them: a revenue or expense line is operating in one entry and
+investing in another (rule 4), and a reversal is tagged by its chain's
+root. The theorems hold for every such tagging; their hypotheses say what
+the engine guarantees (the cash tag follows the account; revenue and
+expense lines are operating or investing; a reversal's lines take its
+original's tags). A line the engine splits between two sections (the bill
+split, rule 12) is two lines here; a split keeps the entry's net. -/
+
+/-- Where a line falls on the statement of cash flows (`kernel::Flow`). -/
+inductive Flow where
+  | cash
+  | operating
+  | investing
+  | financing
+  deriving DecidableEq, Repr
+
+/-- The net movement of the lines `f` tags `k`. -/
+def secNet (f : Line → Flow) (k : Flow) : List Line → Int
+  | [] => 0
+  | l :: ls => (if f l = k then l.signed else 0) + secNet f k ls
+
+@[simp] theorem secNet_nil (f : Line → Flow) (k : Flow) : secNet f k [] = 0 := rfl
+@[simp] theorem secNet_cons (f : Line → Flow) (k : Flow) (l : Line) (ls : List Line) :
+    secNet f k (l :: ls) = (if f l = k then l.signed else 0) + secNet f k ls := rfl
+
+/-- **Every line is in exactly one place**: an entry's net is its cash plus
+its three sections' movements. -/
+theorem net_splits_by_flow (f : Line → Flow) (ls : List Line) :
+    net ls = secNet f .cash ls + secNet f .operating ls + secNet f .investing ls
+      + secNet f .financing ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [net_cons, secNet_cons, ih]
+    cases f l <;> simp <;> omega
+
+/-- The cash one section takes from what is left (`kernel::take`): only a
+section moving against the cash, never more than its own movement. -/
+def take (rem n : Int) : Int :=
+  if 0 < rem ∧ n < 0 then min rem (-n) else if rem < 0 ∧ 0 < n then max rem (-n) else 0
+
+/-- `kernel::apply_cash`: the cash applied to each movement in order, and
+what is left. -/
+def applyCash : Int → List Int → List Int × Int
+  | rem, [] => ([], rem)
+  | rem, n :: ns => (take rem n :: (applyCash (rem - take rem n) ns).1,
+      (applyCash (rem - take rem n) ns).2)
+
+/-- A sum of integers. -/
+def isum : List Int → Int
+  | [] => 0
+  | x :: xs => x + isum xs
+
+@[simp] theorem isum_nil : isum [] = 0 := rfl
+@[simp] theorem isum_cons (x : Int) (xs : List Int) : isum (x :: xs) = x + isum xs := rfl
+
+theorem isum_append (xs ys : List Int) : isum (xs ++ ys) = isum xs + isum ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, isum_cons, ih]; omega
+
+theorem isum_neg (xs : List Int) : isum (xs.map (fun x => -x)) = -isum xs := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih => simp only [List.map_cons, isum_cons, ih]; omega
+
+/-- Applying cash invents and loses nothing: the parts and what is left
+sum to the cash. -/
+theorem applyCash_conserves (rem : Int) (ns : List Int) :
+    isum (applyCash rem ns).1 + (applyCash rem ns).2 = rem := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash]
+  | cons n ns ih =>
+    simp only [applyCash, isum_cons]
+    have := ih (rem - take rem n)
+    omega
+
+theorem applyCash_length (rem : Int) (ns : List Int) :
+    (applyCash rem ns).1.length = ns.length := by
+  induction ns generalizing rem with
+  | nil => rfl
+  | cons n ns ih => simp [applyCash, ih]
+
+theorem take_zero (n : Int) : take 0 n = 0 := by
+  simp [take]
+
+/-- With no cash, nothing is applied and nothing is left. -/
+theorem applyCash_zero (ns : List Int) : (applyCash 0 ns).2 = 0 := by
+  induction ns with
+  | nil => rfl
+  | cons n ns ih => simp [applyCash, take_zero, ih]
+
+/-- Cash in is used up when the movements against it cover it. -/
+theorem applyCash_exhausts_pos (rem : Int) (ns : List Int) (h0 : 0 ≤ rem)
+    (h : rem + isum ns ≤ 0) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [isum_cons] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : n < 0
+      · by_cases hle : -n ≤ rem
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- Cash out is used up when the movements against it cover it. -/
+theorem applyCash_exhausts_neg (rem : Int) (ns : List Int) (h0 : rem ≤ 0)
+    (h : 0 ≤ rem + isum ns) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [isum_cons] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : 0 < n
+      · by_cases hle : rem ≤ -n
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- **Balanced, the cash is used up**: when the cash and the movements sum
+to zero, nothing is left over. -/
+theorem applyCash_exhausts (rem : Int) (ns : List Int) (h : rem + isum ns = 0) :
+    (applyCash rem ns).2 = 0 := by
+  rcases Int.le_total 0 rem with h0 | h0
+  · exact applyCash_exhausts_pos rem ns h0 (by omega)
+  · exact applyCash_exhausts_neg rem ns h0 (by omega)
+
+theorem take_neg (r n : Int) : take (-r) (-n) = -take r n := by
+  simp only [take]
+  by_cases h1 : 0 < r ∧ n < 0
+  · rw [ite_eq_right (by omega), ite_eq_left (by omega), ite_eq_left h1]; omega
+  · by_cases h2 : r < 0 ∧ 0 < n
+    · rw [ite_eq_left (by omega), ite_eq_right h1, ite_eq_left h2]; omega
+    · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right h1, ite_eq_right h2]; omega
+
+/-- Applying minus the cash to minus the movements gives minus the parts:
+what lets a reversal mirror its original. -/
+theorem applyCash_neg (rem : Int) (ns : List Int) :
+    applyCash (-rem) (ns.map (fun x => -x))
+      = ((applyCash rem ns).1.map (fun x => -x), -(applyCash rem ns).2) := by
+  induction ns generalizing rem with
+  | nil => rfl
+  | cons n ns ih =>
+    simp only [List.map_cons, applyCash, take_neg]
+    have : -rem - -take rem n = -(rem - take rem n) := by omega
+    rw [this, ih]
+
+/-- An entry's cash: the net of the lines tagged cash. -/
+def cashOf (F : List Line → Line → Flow) (e : List Line) : Int := secNet (F e) .cash e
+
+/-- An entry's section movements, `[operating, investing, financing]`. -/
+def moves (F : List Line → Line → Flow) (e : List Line) : List Int :=
+  [secNet (F e) .operating e, secNet (F e) .investing e, secNet (F e) .financing e]
+
+/-- An entry's cash flows per section (`kernel::entry_flows`). -/
+def flows (F : List Line → Line → Flow) (e : List Line) : List Int :=
+  (applyCash (cashOf F e) (moves F e)).1
+
+/-- **An entry's cash flows sum to its cash** (`entry_flows_sum`): for a
+balanced entry, the sections' cash is exactly the cash that moved. -/
+theorem entry_flows_sum (F : List Line → Line → Flow) (e : List Line) (h : net e = 0) :
+    isum (flows F e) = cashOf F e := by
+  have hb := net_splits_by_flow (F e) e
+  have hx : (applyCash (cashOf F e) (moves F e)).2 = 0 := by
+    apply applyCash_exhausts
+    simp only [moves, cashOf, isum_cons, isum_nil]
+    omega
+  have := applyCash_conserves (cashOf F e) (moves F e)
+  simp only [flows]
+  omega
+
+theorem flows_length (F : List Line → Line → Flow) (e : List Line) : (flows F e).length = 3 := by
+  simp [flows, applyCash_length, moves]
+
+theorem secNet_reversal (f g : Line → Flow) (k : Flow) (ls : List Line)
+    (h : ∀ l ∈ ls, g l.reverse = f l) : secNet g k (reversal ls) = -secNet f k ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    simp only [secNet_cons, h l (by simp), Line.reverse_signed,
+      ih (fun m hm => h m (by simp [hm]))]
+    split <;> omega
+
+/-- **A reversal's flows are its original's, negated** (`flows_reversal`),
+when its lines take its original's tags: what lets an entry and its
+reversal drop out of the statement together (rules.md B-14 rule 6). -/
+theorem flows_reversal (F : List Line → Line → Flow) (e : List Line)
+    (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l) :
+    flows F (reversal e) = (flows F e).map (fun x => -x) := by
+  simp only [flows, cashOf, moves]
+  rw [secNet_reversal (F e) (F (reversal e)) .cash e hF,
+    secNet_reversal (F e) (F (reversal e)) .operating e hF,
+    secNet_reversal (F e) (F (reversal e)) .investing e hF,
+    secNet_reversal (F e) (F (reversal e)) .financing e hF]
+  have := applyCash_neg (secNet (F e) .cash e)
+    [secNet (F e) .operating e, secNet (F e) .investing e, secNet (F e) .financing e]
+  simp only [List.map_cons, List.map_nil] at this
+  rw [this]
+
+theorem isum_three (xs : List Int) (h : xs.length = 3) :
+    isum xs = xs.getD 0 0 + xs.getD 1 0 + xs.getD 2 0 := by
+  match xs, h with
+  | [a, b, c], _ => simp; omega
+
+/-! ### What a member or lender pays or receives for the company (rule 11)
+
+`kernel::constructive` (D-42): what is left unsettled of an entry's
+kinds that can pay or receive for the company (`s`, a financing liability
+or a member's capital) settles what is left of the kinds they pay or
+receive for (`u`), as if through the cash accounts. The engine sums the
+parts by section into an entry's constructive triple; the entry theorems
+below take any triple that nets to zero (and, for reversals, mirrors),
+which `constructive_nets` and `constructive_neg` give the kernel's. -/
+
+/-- The credits among some movements, `Σ max(-m, 0)`: what cash in can
+settle. -/
+def creditTotal : List Int → Int
+  | [] => 0
+  | m :: ms => max (-m) 0 + creditTotal ms
+
+/-- The debits among some movements, `Σ max(m, 0)`: what cash out can
+settle. -/
+def debitTotal : List Int → Int
+  | [] => 0
+  | m :: ms => max m 0 + debitTotal ms
+
+theorem creditTotal_nonneg (ms : List Int) : 0 ≤ creditTotal ms := by
+  induction ms with
+  | nil => simp [creditTotal]
+  | cons m ms ih => simp only [creditTotal]; omega
+
+theorem debitTotal_nonneg (ms : List Int) : 0 ≤ debitTotal ms := by
+  induction ms with
+  | nil => simp [debitTotal]
+  | cons m ms ih => simp only [debitTotal]; omega
+
+theorem creditTotal_neg (ms : List Int) :
+    creditTotal (ms.map (fun x => -x)) = debitTotal ms := by
+  induction ms with
+  | nil => rfl
+  | cons m ms ih => simp only [List.map_cons, creditTotal, debitTotal, ih]; omega
+
+theorem debitTotal_neg (ms : List Int) :
+    debitTotal (ms.map (fun x => -x)) = creditTotal ms := by
+  induction ms with
+  | nil => rfl
+  | cons m ms ih =>
+    simp only [List.map_cons, creditTotal, debitTotal, ih]
+
+/-- Cash in is used up when the credits cover it (whatever the debits). -/
+theorem applyCash_exhausts_in (rem : Int) (ns : List Int) (h0 : 0 ≤ rem)
+    (h : rem ≤ creditTotal ns) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash, creditTotal] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [creditTotal] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : n < 0
+      · by_cases hle : -n ≤ rem
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- Cash out is used up when the debits cover it (whatever the credits). -/
+theorem applyCash_exhausts_out (rem : Int) (ns : List Int) (h0 : rem ≤ 0)
+    (h : -rem ≤ debitTotal ns) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash, debitTotal] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [debitTotal] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : 0 < n
+      · by_cases hle : rem ≤ -n
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- Which way the money went (`kernel::OnBehalf`). -/
+inductive OnBehalf where
+  | paid
+  | received
+  deriving DecidableEq, Repr
+
+/-- The other way: what a reversal does. -/
+def OnBehalf.mirror : OnBehalf → OnBehalf
+  | .paid => .received
+  | .received => .paid
+
+/-- The cash the sources take, + in (`kernel::constructive`): paid, the
+smaller of the sources' credits and the uses' debits; received, minus the
+smaller of the sources' debits and the uses' credits. -/
+def onBehalfCash : OnBehalf → List Int → List Int → Int
+  | .paid, s, u => min (creditTotal s) (debitTotal u)
+  | .received, s, u => -min (debitTotal s) (creditTotal u)
+
+/-- `kernel::constructive`: the sources' parts and the uses' parts. -/
+def constructive (w : OnBehalf) (s u : List Int) : List Int × List Int :=
+  ((applyCash (onBehalfCash w s u) s).1, (applyCash (-onBehalfCash w s u) u).1)
+
+/-- **What a member or lender handled for the company nets to zero**
+(`constructive_nets`; Kani `constructive_nets_to_zero`): the sources take
+exactly what the uses give, so an entry's flows still sum to its cash. -/
+theorem constructive_nets (w : OnBehalf) (s u : List Int) :
+    isum (constructive w s u).1 + isum (constructive w s u).2 = 0 := by
+  have hs := applyCash_conserves (onBehalfCash w s u) s
+  have hu := applyCash_conserves (-onBehalfCash w s u) u
+  have cs := creditTotal_nonneg s
+  have ds := debitTotal_nonneg s
+  have cu := creditTotal_nonneg u
+  have du := debitTotal_nonneg u
+  have ⟨xs, xu⟩ : (applyCash (onBehalfCash w s u) s).2 = 0 ∧
+      (applyCash (-onBehalfCash w s u) u).2 = 0 := by
+    cases w with
+    | paid =>
+      simp only [onBehalfCash]
+      exact ⟨applyCash_exhausts_in _ _ (by omega) (by omega),
+        applyCash_exhausts_out _ _ (by omega) (by omega)⟩
+    | received =>
+      simp only [onBehalfCash]
+      exact ⟨applyCash_exhausts_out _ _ (by omega) (by omega),
+        applyCash_exhausts_in _ _ (by omega) (by omega)⟩
+  simp only [constructive]
+  omega
+
+theorem onBehalfCash_mirror (w : OnBehalf) (s u : List Int) :
+    onBehalfCash w.mirror (s.map (fun x => -x)) (u.map (fun x => -x))
+      = -onBehalfCash w s u := by
+  cases w <;> simp only [OnBehalf.mirror, onBehalfCash, creditTotal_neg, debitTotal_neg] <;> omega
+
+/-- **The other way, minus the sources and uses give minus the parts**
+(`constructive_neg`; Kani `constructive_mirrors`): a payment made for the
+company and its reversal drop out together. -/
+theorem constructive_neg (w : OnBehalf) (s u : List Int) :
+    constructive w.mirror (s.map (fun x => -x)) (u.map (fun x => -x))
+      = ((constructive w s u).1.map (fun x => -x), (constructive w s u).2.map (fun x => -x)) := by
+  simp only [constructive, onBehalfCash_mirror]
+  rw [applyCash_neg (onBehalfCash w s u) s, applyCash_neg (-onBehalfCash w s u) u]
+
+/-- Three sections' figures, summed. -/
+def sum3 (xs : List Int) : Int := xs.getD 0 0 + xs.getD 1 0 + xs.getD 2 0
+
+@[simp] theorem sum3_cons (a b c : Int) : sum3 [a, b, c] = a + b + c := by
+  simp [sum3]
+
+/-- **The kernel's parts, by section, net to zero**: split the uses into
+operating ones then investing ones (`kernel::constructive` takes them in
+that order), and the triple (operating, investing, financing = the
+sources) the engine adds to an entry's flows sums to zero. -/
+theorem constructive_sections_net (w : OnBehalf) (s uo ui : List Int) :
+    sum3 [isum ((constructive w s (uo ++ ui)).2.take uo.length),
+      isum ((constructive w s (uo ++ ui)).2.drop uo.length),
+      isum (constructive w s (uo ++ ui)).1] = 0 := by
+  have h := constructive_nets w s (uo ++ ui)
+  have hs := isum_append ((constructive w s (uo ++ ui)).2.take uo.length)
+    ((constructive w s (uo ++ ui)).2.drop uo.length)
+  rw [List.take_append_drop] at hs
+  rw [sum3_cons]
+  omega
+
+/-- Passes add: two triples that net to zero add to one that does. -/
+theorem sum3_add (xs ys : List Int) (hx : sum3 xs = 0) (hy : sum3 ys = 0) :
+    sum3 [xs.getD 0 0 + ys.getD 0 0, xs.getD 1 0 + ys.getD 1 0, xs.getD 2 0 + ys.getD 2 0] = 0 := by
+  rw [sum3_cons]
+  simp only [sum3] at hx hy
+  omega
+
+/-- Two triples, added section by section. -/
+def add3 (xs ys : List Int) : List Int :=
+  [xs.getD 0 0 + ys.getD 0 0, xs.getD 1 0 + ys.getD 1 0, xs.getD 2 0 + ys.getD 2 0]
+
+/-- An entry's flows on the statement: its cash flows, plus `C e`, what a
+member or lender paid or received for it, by section (rule 11). -/
+def stmtFlows (F : List Line → Line → Flow) (C : List Line → List Int) (e : List Line) :
+    List Int :=
+  add3 (flows F e) (C e)
+
+/-- **An entry's statement flows sum to its cash** when what was handled
+for it nets to zero: rule 11 moves no cash (`stmt_flows_sum`). -/
+theorem stmt_flows_sum (F : List Line → Line → Flow) (C : List Line → List Int)
+    (e : List Line) (h : net e = 0) (hC : sum3 (C e) = 0) :
+    sum3 (stmtFlows F C e) = cashOf F e := by
+  have he := entry_flows_sum F e h
+  rw [isum_three _ (flows_length F e)] at he
+  simp only [stmtFlows, add3, sum3_cons]
+  simp only [sum3] at hC
+  omega
+
+theorem getD_neg (xs : List Int) (k : Nat) :
+    (xs.map (fun x => -x)).getD k 0 = -xs.getD k 0 := by
+  induction xs generalizing k with
+  | nil => simp
+  | cons x xs ih => cases k with
+    | zero => simp
+    | succ k => simp only [List.map_cons, List.getD_cons_succ, ih]
+
+/-- **A reversal's statement flows are its original's, negated**, when its
+lines take the original's tags and what was handled for it mirrors
+(`constructive_neg`). -/
+theorem stmt_flows_reversal (F : List Line → Line → Flow) (C : List Line → List Int)
+    (e : List Line) (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l)
+    (hC : C (reversal e) = (C e).map (fun x => -x)) :
+    stmtFlows F C (reversal e) = (stmtFlows F C e).map (fun x => -x) := by
+  simp only [stmtFlows, add3, flows_reversal F e hF, hC, getD_neg, List.map_cons,
+    List.map_nil, List.cons.injEq, and_true]
+  refine ⟨?_, ?_, ?_⟩ <;> omega
+
+/-- A section's total over some entries: the sum of each entry's cash in
+it (`k` = 0 operating, 1 investing, 2 financing), what a member or lender
+handled for it included. -/
+def sectionTotal (F : List Line → Line → Flow) (C : List Line → List Int) (k : Nat) :
+    List (List Line) → Int
+  | [] => 0
+  | e :: es => (stmtFlows F C e).getD k 0 + sectionTotal F C k es
+
+/-- The entries' cash, summed. -/
+def cashTotal (F : List Line → Line → Flow) : List (List Line) → Int
+  | [] => 0
+  | e :: es => cashOf F e + cashTotal F es
+
+/-- **The sections sum to the change in cash** (plan P3): over any balanced
+entries, operating + investing + financing is the entries' cash, exactly,
+whatever a member or lender handled for them as long as it nets to zero
+within each entry (rule 11, `constructive_nets`). The statement's footing
+(rules.md B-14 rule 9) can't fail on posted entries. -/
+theorem cashflow_sections_sum_to_cash_change (F : List Line → Line → Flow)
+    (C : List Line → List Int) (es : List (List Line)) (h : ∀ e ∈ es, net e = 0)
+    (hC : ∀ e ∈ es, sum3 (C e) = 0) :
+    sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es = cashTotal F es := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [sectionTotal, cashTotal]
+    have he := stmt_flows_sum F C e (h e (by simp)) (hC e (by simp))
+    simp only [sum3] at he
+    have := ih (fun x hx => h x (by simp [hx])) (fun x hx => hC x (by simp [hx]))
+    omega
+
+/-- When the cash tag follows the account (a line is cash exactly when
+its account is a cash account), an entry's cash is the movement of the
+cash accounts. -/
+theorem secNet_cash_is_movement (f : Line → Flow) (cash : List Nat) (hd : Distinct cash)
+    (hf : ∀ l, f l = .cash ↔ l.account ∈ cash) (ls : List Line) :
+    secNet f .cash ls = sumOver (fun a => movement a ls) cash := by
+  induction ls with
+  | nil => simpa using (sumOver_zero cash).symm
+  | cons l ls ih =>
+    simp only [secNet_cons, movement_cons]
+    rw [sumOver_add, ← ih]
+    by_cases hc : l.account ∈ cash
+    · rw [ite_eq_left ((hf l).2 hc), sumOver_indicator l.account l.signed cash hd hc]
+    · rw [ite_eq_right (fun e => hc ((hf l).1 e)), sumOver_indicator_absent l.account l.signed cash hc]
+
+/-! ### Net income reconciled to operating cash (rules.md B-14 rule 8) -/
+
+/-- Net movement of the lines on revenue and expense accounts (`pl`)
+tagged `k` (`sel = true`), or on balance-sheet accounts (`sel = false`). -/
+def plNet (pl : Nat → Bool) (sel : Bool) (f : Line → Flow) (k : Flow) : List Line → Int
+  | [] => 0
+  | l :: ls => (if pl l.account = sel ∧ f l = k then l.signed else 0) + plNet pl sel f k ls
+
+/-- Net movement of every revenue and expense line. -/
+def plAll (pl : Nat → Bool) : List Line → Int
+  | [] => 0
+  | l :: ls => (if pl l.account = true then l.signed else 0) + plAll pl ls
+
+/-- Net income: revenue less expenses, `-(net of the P&L lines)`. -/
+def netIncome (pl : Nat → Bool) (e : List Line) : Int := -plAll pl e
+
+/-- G: the P&L lines rule 4 puts in investing (gains and losses). -/
+def gainLoss (pl : Nat → Bool) (F : List Line → Line → Flow) (e : List Line) : Int :=
+  plNet pl true (F e) .investing e
+
+/-- W: minus the movement of the operating balance-sheet lines. -/
+def balanceChange (pl : Nat → Bool) (F : List Line → Line → Flow) (e : List Line) : Int :=
+  -plNet pl false (F e) .operating e
+
+/-- X: what no cash, real or handled for the company, settled of the
+operating movement. -/
+def noncashOp (F : List Line → Line → Flow) (C : List Line → List Int) (e : List Line) : Int :=
+  secNet (F e) .operating e + (stmtFlows F C e).getD 0 0
+
+theorem secNet_split (pl : Nat → Bool) (f : Line → Flow) (k : Flow) (ls : List Line) :
+    secNet f k ls = plNet pl true f k ls + plNet pl false f k ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [secNet_cons, plNet, ih]
+    cases pl l.account <;> by_cases h : f l = k <;> simp [h] <;> omega
+
+theorem plAll_split (pl : Nat → Bool) (f : Line → Flow) (ls : List Line)
+    (h : ∀ l ∈ ls, pl l.account = true → f l = .operating ∨ f l = .investing) :
+    plAll pl ls = plNet pl true f .operating ls + plNet pl true f .investing ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [plAll, plNet, ih (fun m hm => h m (by simp [hm]))]
+    cases hp : pl l.account
+    · simp
+    · rcases h l (by simp) hp with hk | hk <;> simp [hk] <;> omega
+
+/-- **Net income reconciles to operating cash**, entry by entry:
+operating cash = NI + G + X + W, when revenue and expense lines are only
+ever operating or investing (rules.md B-14 rule 8; ASC 230-10-45-28 to
+45-30), whatever a member or lender handled for it (rule 11). -/
+theorem operating_reconciliation_ties (pl : Nat → Bool) (F : List Line → Line → Flow)
+    (C : List Line → List Int) (e : List Line)
+    (h : ∀ l ∈ e, pl l.account = true → F e l = .operating ∨ F e l = .investing) :
+    (stmtFlows F C e).getD 0 0
+      = netIncome pl e + gainLoss pl F e + noncashOp F C e + balanceChange pl F e := by
+  have hs := secNet_split pl (F e) .operating e
+  have hp := plAll_split pl (F e) e h
+  simp only [netIncome, gainLoss, noncashOp, balanceChange]
+  omega
+
+/-- The operating section's total over some entries. -/
+def opTotal (pl : Nat → Bool) (F : List Line → Line → Flow) (C : List Line → List Int) :
+    List (List Line) → Int
+  | [] => 0
+  | e :: es => netIncome pl e + gainLoss pl F e + noncashOp F C e + balanceChange pl F e
+      + opTotal pl F C es
+
+/-- **The reconciliation schedule ties to the operating section** over any
+entries: the section's total is NI + G + X + W summed. -/
+theorem operating_reconciliation_ties_all (pl : Nat → Bool) (F : List Line → Line → Flow)
+    (C : List Line → List Int) (es : List (List Line))
+    (h : ∀ e ∈ es, ∀ l ∈ e, pl l.account = true → F e l = .operating ∨ F e l = .investing) :
+    sectionTotal F C 0 es = opTotal pl F C es := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [sectionTotal, opTotal]
+    rw [operating_reconciliation_ties pl F C e (h e (by simp)),
+      ih (fun x hx => h x (by simp [hx]))]
+
+end Bookspec
diff --git a/bookspec/lean/lake-manifest.json b/bookspec/lean/lake-manifest.json
new file mode 100644
index 0000000..16bbf3f
--- /dev/null
+++ b/bookspec/lean/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.3.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "bookspec",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/bookspec/lean/lakefile.toml b/bookspec/lean/lakefile.toml
new file mode 100644
index 0000000..a16dbc4
--- /dev/null
+++ b/bookspec/lean/lakefile.toml
@@ -0,0 +1,5 @@
+name = "bookspec"
+defaultTargets = ["Bookspec"]
+
+[[lean_lib]]
+name = "Bookspec"
diff --git a/bookspec/lean/lean-toolchain b/bookspec/lean/lean-toolchain
new file mode 100644
index 0000000..ba8ebf2
--- /dev/null
+++ b/bookspec/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1
diff --git a/bookspec/spec/00-model.md b/bookspec/spec/00-model.md
new file mode 100644
index 0000000..767d15f
--- /dev/null
+++ b/bookspec/spec/00-model.md
@@ -0,0 +1,101 @@
+# bookspec, first edition: definitions and the model
+
+bookspec is a specification of double-entry bookkeeping that stands apart
+from any program. Each rule is stated normatively, sourced to an authority
+(or marked as a convention or a choice), written symbolically, and shown
+by concrete examples (`bookspec/examples/*.toml`) that any engine can be
+run against (`bookspec/runner`). wanderbooks is the first engine checked;
+the GnuCash oracle is the second (`bookspec/gnucash`).
+
+## Reading the rules
+
+The words MUST, MUST NOT and MAY are RFC 2119's. A rule has
+
+- an **identifier**, `BS-<area>-<n>`, stable and never reused; the table
+  from the wanderbooks catalogue's `B-1` to `B-45` is `rules-index.md`;
+- a **status**: `AUTHORITY` (a source states it), `CONVENTION` (common
+  practice no authority states; the best reference is given), or `CHOICE`
+  (a person decided; the specification names the options and an engine
+  declares which it picks, `Claims::choices`);
+- a **statement** (what MUST hold), its **sources** (each pinned exactly:
+  a vendored source with a verbatim quotation the build checks, or an
+  external reference to a paragraph, never a paraphrase of memory), its
+  **symbolic form**, its **examples** (ids of the TOML files) and its
+  **applicability** (which entities, bases and jurisdictions).
+
+A rule with no example is stated and not claimable: an engine can only
+claim a rule an example demonstrates (`covered_rules`). The first edition
+says plainly which rules those are (`rules-index.md`, "—").
+
+Sources are US GAAP (the FASB Codification: cited, never copied, and read
+only in the Foundation's own view or a publisher that reproduces it) and
+US federal tax (the Internal Revenue Code, Treasury Regulations, IRS
+publications and form instructions, which are public domain), then older
+or general authorities (Pacioli, OpenStax, ISO 4217). The large firms'
+guides are never a source.
+
+## The model
+
+- **Currency and money.** A ledger has one **base currency**. An
+  **amount** is an exact decimal, a whole number of the currency's
+  smallest unit (ISO 4217 minor units). Arithmetic on amounts is exact;
+  it never uses binary floating point, and it rounds only where a rule
+  says so, and then by the rounding mode the rule names.
+- **Account.** A code, a name and one of five **types**: asset,
+  liability, equity, revenue, expense. An account may have a parent of
+  its own type; an account may be a **header** (it groups, and takes no
+  posting). Assets and expenses have a **normal balance** on the debit
+  side; liabilities, equity and revenue on the credit side.
+- **Line.** `(account, side, amount)`: `side` is debit or credit,
+  `amount > 0`. Its **signed value** is `+amount` for a debit and
+  `-amount` for a credit.
+- **Entry.** A dated, described list of at least two lines. An entry is
+  **posted** or not; the ledger holds the posted ones. A **reversal** of
+  an entry is a new entry with the same accounts and amounts and the
+  sides flipped, linked to it.
+- **Ledger.** The sequence of posted entries, written only forward. The
+  **balance** of an account through a day is the sum of its lines' signed
+  values dated on or before the day; shown on its normal side it is that
+  sum, negated for a credit-normal account.
+- **Period and close.** A **period** is a range of days. **Closing** it
+  posts an entry that brings every revenue and expense account's balance
+  through the period's last day to zero against equity.
+- **Document.** An invoice or a bill: a receivable or payable the ledger
+  carries as lines tagged with the document; control accounts equal the
+  documents behind them.
+
+## The five laws
+
+Every other rule serves these, and each is a theorem in `bookspec/lean`
+(`Bookspec.law_*`), true of every state the ledger can reach by any
+sequence of its commands:
+
+1. **Debits equal credits.** `sum over all posted lines of signed value = 0`
+   (`law_debits_equal_credits`; BS-entry-1).
+2. **The accounting equation.** `A = L + E + (R - X)`, with each term the
+   sum of the balances of that type's accounts on their normal side
+   (`law_accounting_equation`; BS-statement-2).
+3. **The trial balance balances.** The debit balances sum to the credit
+   balances (`law_trial_balance`; BS-statement-1).
+4. **Net income articulates to equity.** Closing a period credits equity
+   with exactly `R - X` through its last day
+   (`law_net_income_articulates`; BS-period-1).
+5. **The cash flow articulates to cash.** The three sections of the
+   statement of cash flows sum to the change in the cash accounts'
+   balances (`law_cash_flow_is_change_in_cash`; BS-statement-3).
+
+Money in the proofs is `Int`, a count of the smallest unit; every law is
+a law of addition, and any finite set of exact decimals scales to
+integers without loss.
+
+## How an example is checked
+
+An example is a TOML file: a setup, a sequence of events, and
+expectations asked of the books, with every expected figure worked by
+hand from the rule and its sources (`bookspec/README.md` has the shape).
+Two checks stand behind each: **conformance** (the runner drives an
+engine through it and compares the engine's answers with the expected
+figures) and **derivation** (the checker computes the expected figures
+from the rule's symbolic form, independent of any engine, and fails the
+specification's own build when the example's figure disagrees; see
+`bookspec/checker/src/derive.rs`).
diff --git a/bookspec/spec/1099.md b/bookspec/spec/1099.md
new file mode 100644
index 0000000..7929408
--- /dev/null
+++ b/bookspec/spec/1099.md
@@ -0,0 +1,14 @@
+# Area: 1099
+
+Information returns for payments to contractors and landlords.
+
+### BS-1099-1: 1099 reporting thresholds, payment methods, and decisions (B-19)
+
+- **Status:** AUTHORITY, with the CHOICEs recorded in `docs/spec/rules.md` B-19
+- **Statement:** A payee's payments made in a calendar year in the course of the payor's trade or business MUST be reportable when they reach the threshold (600 dollars through 2025; 2,000 dollars for payments made after December 31, 2025; indexed after 2026). Payments by payment card or third-party network MUST be excluded (they are reported on Form 1099-K by the settlement entity); payments through a financing account whose method is unrecorded MUST be undetermined, not counted; a payee's decision (reportable, not reportable with a reason, undetermined) applies by the payment's date; money between the company's own accounts pays no one.
+- **Sources:**
+  - vendored `sources/irs-1099-thresholds.md`: "6041(a)"
+  - vendored `sources/irs-1099-payment-method.md`: "1099-K"
+- **Symbolic form:** `reportable(p, y) iff sum{pay : payee = p, year = y, method not card/network} >= threshold(y)`; `threshold(y) = 600 if y <= 2025 else 2000`.
+- **Examples:** `1099-a-dated-status-applies-by-payment-date`, `1099-a-members-check-through-financing-counts`, `1099-and-party-totals-for-a-members-payment`, `1099-card-payments-are-excluded`, `1099-money-between-own-accounts-pays-no-one`, `1099-money-from-a-payee-is-netted-only-as-a-refund`, `1099-the-threshold-is-the-years`, `1099-worksheet-through-as-of`
+- **Applicability:** US payors; royalties (10 dollars) and attorney gross proceeds (600 dollars) are not modelled.
diff --git a/bookspec/spec/arap.md b/bookspec/spec/arap.md
new file mode 100644
index 0000000..9cae2ca
--- /dev/null
+++ b/bookspec/spec/arap.md
@@ -0,0 +1,64 @@
+# Area: arap
+
+Receivables and payables: documents, aging, terms, write-offs and
+settlements.
+
+### BS-arap-1: Aging buckets: Current, 1-30, 31-60, 61-90, 90+ days past due (B-18)
+
+- **Status:** CONVENTION (bucket edges); CHOICE (a document due today is Current; aging as of a day shows only documents issued by then, less payments made by then; a payment never predates its document)
+- **Statement:** An aging as of a day MUST place each open document in exactly one of the buckets Current (not yet past due, including due today), 1-30, 31-60, 61-90 and 90+ days past due, and the buckets MUST partition what the documents owe, exactly. A void document is in no bucket; a payment reversed by the day no longer counts.
+- **Sources:**
+  - external: ASC 326-20-55-37 and 326-20-55-38, an illustrative aging of trade receivables
+- **Symbolic form:** `d = as_of - due`; bucket `Current` if `d <= 0`, `1-30` if `1 <= d <= 30`, `31-60`, `61-90`, `90+` if `d >= 91`; `sum_b owed(b) = sum of open balances`.
+- **Examples:** none yet. The schema has no aging query; the example for it waits on one (a document-level query is owed by this edition's successor).
+- **Applicability:** accrual-basis entities with receivables or payables.
+
+### BS-arap-2: A document's figures are its ledger lines that stand; a control account is its documents (B-38)
+
+- **Status:** CHOICE (the owner, 2026-10-23); CONVENTION (a control account agrees with its subledger)
+- **Statement:** Every ledger line on a receivables or payables control account MUST carry the document it belongs to; a document's total, paid and owed MUST be derived from its tagged lines that stand (a reversed line no longer counts); a control account's balance MUST equal the sum of its documents'. A hand line on a control account MUST be refused.
+- **Sources:**
+  - external: ASC 310-10 (receivables); ASC 405-20-40-1 (a liability is removed only when paid or released); ASC 606-10-45-4 (a receivable is a right to consideration that is unconditional)
+- **Symbolic form:** `bal(1200) = sum_{doc} owed(doc)` and `owed(doc) = sum{signed tagged lines that stand}`.
+- **Examples:** `arap-hand-control-posting-refused`
+- **Applicability:** engines with invoices and bills.
+
+### BS-arap-3: Terms: when a document is due (B-39)
+
+- **Status:** reserved
+- **Statement:** Reserved: allocated in the wanderbooks plan (8.0.3) for payment terms and due dates, not yet stated in `docs/spec/rules.md`.
+- **Sources:**
+  - none yet
+- **Symbolic form:** none yet.
+- **Examples:** none yet
+- **Applicability:** none yet.
+
+### BS-arap-4: Numbers and the issued copy (B-40)
+
+- **Status:** reserved
+- **Statement:** Reserved: allocated in the wanderbooks plan (8.0.3) for document numbers and the issued copy, not yet stated in `docs/spec/rules.md`.
+- **Sources:**
+  - none yet
+- **Symbolic form:** none yet.
+- **Examples:** none yet
+- **Applicability:** none yet.
+
+### BS-arap-5: A debt that will not be collected is written off, and a recovery is income (B-41)
+
+- **Status:** CHOICE (direct write-off, the owner, 2026-10-23); options: direct write-off, allowance method
+- **Statement:** On the direct method, an invoice that will not be collected MUST be written off by debiting bad debt expense and crediting receivables, the receivable line tagged with the invoice; a partial write-off is the amount charged off; a write-off MUST be refused on cash-basis books and for more than is owed; a later recovery is income.
+- **Sources:**
+  - external: 26 U.S.C. section 166(a); Treas. Reg. sections 1.166-1(e), 1.166-2(a), 1.166-3(a); 26 U.S.C. section 111 (recovery); ASC 326-20 (the allowance method, not applied)
+- **Symbolic form:** `Dr 6990 amount; Cr 1200 amount` tagged with the invoice; `0 < amount <= owed`.
+- **Examples:** `bad-debt-direct-write-off`
+- **Applicability:** accrual-basis taxpayers.
+
+### BS-arap-6: A settlement is exact, one party, and names its lines; the gross discount and the gross fee (B-42)
+
+- **Status:** CONVENTION; CHOICE (the gross method for an early-payment discount, the owner A-8; the processor's fee posted gross, A-4)
+- **Statement:** A settlement MUST apply to documents of one party and one kind, never the same document twice; sum of cash plus sum of discounts MUST equal what it applies to the documents, and the deposit MUST equal cash less fee, exactly; no application may exceed what its document owes on any day from the payment's date on; a discount MUST be at most the terms allow and be dated within the discount period, or carry a reason; a processor's fee posts gross (expense debited, deposit the net, receivables credited the gross).
+- **Sources:**
+  - external: ASC 606-10-32-5 to 32-9 (the strict treatment of an expected discount, simplified here by the gross method)
+- **Symbolic form:** `sum cash + sum discount = sum applied`; `deposit = sum cash - fee`; `owed_after >= 0` on every day.
+- **Examples:** none yet. The schema has no payment or settlement event (`arap-settlement-exact` and `processor-fee-gross-presentation` are the names the plan allocates; they wait on that event).
+- **Applicability:** engines with documents and settlements.
diff --git a/bookspec/spec/asset.md b/bookspec/spec/asset.md
new file mode 100644
index 0000000..82b8084
--- /dev/null
+++ b/bookspec/spec/asset.md
@@ -0,0 +1,45 @@
+# Area: asset
+
+Fixed assets, depreciation, the register and capitalization.
+
+### BS-asset-1: Depreciation: straight line, salvage never depreciated, partial months by days (B-15)
+
+- **Status:** CONVENTION (the book method); AUTHORITY for tax conventions, which an engine need not apply
+- **Statement:** Depreciation MUST spread cost less salvage over the useful life in a systematic and rational manner: straight line, full months equal, the first and last partial months by their days, the last month taking what the others leave so the total is exactly cost less salvage. Salvage MUST NOT be depreciated. A run MUST post what the schedule says is due through the month and the books do not carry (a skipped month caught up); a disposal MUST post any depreciation still due through its day, then the disposal entry with its gain or loss; depreciation past a disposal MUST be refused.
+- **Sources:**
+  - vendored `sources/fasb-asc.md`: "360-10-35-4"
+  - external: OpenStax, Principles of Accounting, Volume 1, section 11.3, straight-line depreciation
+- **Symbolic form:** `dep_m = round((cost - salvage) * days_m / days_total)` for the partial months; `sum_m dep_m = cost - salvage`.
+- **Examples:** `assets-acquired-before-in-service`, `assets-a-reversed-run-is-not-posted`, `assets-book-value-is-what-the-books-carry`, `depreciation-catch-up-month`, `depreciation-disposal-after-a-late-change-undone`, `depreciation-disposal-before-a-later-run`, `depreciation-disposal-in-final-month`, `depreciation-disposal-inside-a-posted-month`, `depreciation-disposal-mid-month`, `depreciation-final-month-by-days`, `depreciation-final-month-drift`, `depreciation-reversal-before-its-run-is-refused`, `depreciation-run-reversed-after-its-month`
+- **Applicability:** entities with fixed assets; tax conventions (half-year, mid-month) are IRS Pub. 946's and are not applied.
+
+### BS-asset-2: Expense or capitalize (book policy, mirrors tax) (B-22)
+
+- **Status:** AUTHORITY
+- **Statement:** An item costing no more than the de minimis safe harbor (500 dollars per invoice or item without an applicable financial statement; 2,500 dollars from taxable years beginning in 2016 under Notice 2015-82) MAY be expensed; a larger one SHOULD be capitalized and depreciated, and amounts paid for benefits lasting no more than twelve months MAY be expensed under the 12-month rule.
+- **Sources:**
+  - vendored `sources/irs-capitalization.md`: "1.263(a)-1(f)"
+  - vendored `sources/irs-capitalization.md`: "1.263(a)-4(f)"
+- **Symbolic form:** `cost <= safe_harbor implies expense MAY`; the election is made yearly on the return.
+- **Examples:** none yet. This is a policy the bookkeeper applies; no engine enforces it, so no engine-neutral behaviour can be demonstrated.
+- **Applicability:** US taxpayers; thresholds as of 2026.
+
+### BS-asset-3: Asset tags: one label per asset, never reused (B-24)
+
+- **Status:** CHOICE (the owner, 2026-10-15)
+- **Statement:** An asset tag (1 to 32 ASCII letters, digits and `- _ . /`) MUST be unique ignoring case and MUST NOT be reused by another asset, even after a retag or a disposal. The fixed asset register MUST reconcile to the cost and accumulated depreciation accounts, showing unregistered cost, unposted depreciation and unattributed accumulated depreciation.
+- **Sources:**
+  - external: CHOICE only: the owner, 2026-10-15 (docs/spec/rules.md B-24); no authority governs a label
+- **Symbolic form:** `tag(a) = tag(b) implies a = b` (case folded), through the asset's whole life.
+- **Examples:** none yet. The schema registers assets without tags; the register-row and register-totals queries demonstrate the reconciliation under BS-asset-1.
+- **Applicability:** engines with an asset register; an engine declares its pick.
+
+### BS-asset-4: Tax figures beside book value: the section 723 basis, the depreciable basis, the section 704(c) built-in gain (B-25)
+
+- **Status:** AUTHORITY; CHOICE (the register carries tax basis; D-41)
+- **Statement:** For property a member contributes, the partnership's basis MUST be the member's adjusted basis (carryover, section 723); book value is its fair market value; the difference at contribution is the section 704(c) built-in gain, fixed at contribution; the depreciable basis of property converted from personal use is the lesser of fair market value and adjusted basis.
+- **Sources:**
+  - vendored `sources/irs-partnership-basis.md`: "723"
+- **Symbolic form:** `basis_723 = adjusted_basis`; `built_in = fmv - basis_723` at contribution; `depreciable = min(fmv, adjusted_basis)` for personal-use conversion.
+- **Examples:** `assets-723-basis-apart-from-depreciable-basis`, `assets-built-in-gain-fixed-at-contribution`, `assets-four-contributed-devices`
+- **Applicability:** partnerships receiving contributed property.
diff --git a/bookspec/spec/entry.md b/bookspec/spec/entry.md
new file mode 100644
index 0000000..1103aa0
--- /dev/null
+++ b/bookspec/spec/entry.md
@@ -0,0 +1,54 @@
+# Area: entry
+
+The mechanics of one entry: its lines, their sides and amounts.
+
+### BS-entry-1: Every entry is a double entry: debits equal credits (B-1)
+
+- **Status:** AUTHORITY
+- **Statement:** An entry MUST have at least two lines, and the sum of its debit lines MUST equal the sum of its credit lines exactly, with no tolerance. An entry that does not MUST be refused whole: it posts nothing, and leaves no partial entry behind.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "All entries made in the ledger have to be double entries"
+  - vendored `sources/irs-records.md`: "the total debits must equal the total credits"
+- **Symbolic form:** for an entry with lines `(s_i, a_i)`, `a_i > 0`: `n >= 2` and `sum{a_i : s_i = debit} = sum{a_i : s_i = credit}`.
+- **Examples:** `entry-an-unbalanced-entry-is-refused`, `statement-the-books-balance-and-the-equation-holds`
+- **Applicability:** every entity, basis and jurisdiction.
+
+### BS-entry-2: A line's amount is positive; its side gives the direction (B-2)
+
+- **Status:** CONVENTION
+- **Statement:** A line's amount MUST be greater than zero, and its side, never its sign, MUST give the direction money moves. A line with a negative or zero amount MUST be refused.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "All the creditors must appear in the Ledger at the right hand side, and all the debtors at the left."
+- **Symbolic form:** `a_i > 0`; `signed(i) = +a_i` if `s_i = debit`, `-a_i` if `s_i = credit`.
+- **Examples:** `entry-a-line-amount-is-positive`
+- **Applicability:** every engine. No authority forbids a negative amount outright; one way to write each line is chosen so every line reads one way.
+
+### BS-entry-3: Exact amounts in the books; rounding only on returns (B-21)
+
+- **Status:** AUTHORITY
+- **Statement:** The books MUST keep every amount exactly, and a sum of amounts MUST be their exact sum. Rounding MUST NOT occur inside the books; where a rule needs a rounded figure (an allocation, a return line), it names the rounding mode and rounds only the total.
+- **Sources:**
+  - vendored `sources/irs-partnerships.md`: "include cents when adding the amounts and round off only the total"
+- **Symbolic form:** amounts are elements of `Z * u` (`u` the currency's smallest unit); `+` is exact on them.
+- **Examples:** `entry-cents-add-exactly`
+- **Applicability:** every engine. Binary floating point is not an implementation of this rule.
+
+### BS-entry-4: What new commands take: four-digit years, amounts a line can carry (B-28)
+
+- **Status:** CONVENTION
+- **Statement:** A command MUST take only dates in 0001-01-01 through 9999-12-31 written `YYYY-MM-DD`, and amounts no larger than one quadrillion with at most ten decimal places; anything else MUST be refused, never wrapped or truncated. Replaying books already written MUST NOT apply these bounds.
+- **Sources:**
+  - external: ISO 8601-1:2019 section 5.2.2.1, calendar dates with four-digit years in the basic profile
+- **Symbolic form:** `date in [0001-01-01, 9999-12-31]`; `|amount| <= 10^15`; `scale(amount) <= 10`.
+- **Examples:** none yet. The example schema writes dates as `YYYY-MM-DD` already (a malformed date fails the schema), so a refusal example needs a command whose input can be out of range; the first edition has none.
+- **Applicability:** commands only; replay of existing books is exempt (posted is forever).
+
+### BS-entry-5: Drafts and evidence (B-43)
+
+- **Status:** reserved
+- **Statement:** Reserved: allocated in the wanderbooks plan (8.0.3) for the draft states of unit P4, not yet stated in `docs/spec/rules.md`. Its identifier and area are fixed so a later edition fills it in without moving another number.
+- **Sources:**
+  - none yet
+- **Symbolic form:** none yet.
+- **Examples:** none yet
+- **Applicability:** none yet.
diff --git a/bookspec/spec/format.md b/bookspec/spec/format.md
new file mode 100644
index 0000000..1dc5680
--- /dev/null
+++ b/bookspec/spec/format.md
@@ -0,0 +1,23 @@
+# Area: format
+
+Interchange formats and the journal's format gate.
+
+### BS-format-1: The journal format gate: newer is not corrupt (B-27)
+
+- **Status:** CHOICE (the owner, 2026-10-16; D-39, 2026-10-20)
+- **Statement:** A reader MUST distinguish a journal line it does not know because it is newer from one that is corrupt: a line's own hash is checked before it is called newer; a reader stops at the first line it cannot read and says the journal is newer; older books move to a newer format only with the owner's go-ahead.
+- **Sources:**
+  - external: CHOICE only: the owner, 2026-10-16 (docs/spec/rules.md B-27); no authority governs a file format's evolution
+- **Symbolic form:** `hash_ok(line) and type(line) unknown implies newer`; `not hash_ok(line) implies corrupt`.
+- **Examples:** none yet. The example schema has no journal-file event; the gate is checked by wanderbooks' store tests.
+- **Applicability:** engines that persist a journal.
+
+### BS-format-2: The QuickBooks Desktop file (IIF): plain ASCII, every entry through as_of, closes left out, classes carried (B-34)
+
+- **Status:** AUTHORITY
+- **Statement:** An IIF file MUST be plain ASCII, tab-separated, with each line ending CR LF; lists (accounts, classes) MUST come before the transactions that use them; an account is identified by its name, a subaccount's name its path joined by colons; every entry through the as-of day MUST be in the file and closing entries left out; classes MUST be carried; text the file must write differently from the books (a name past 31 characters, a memo past 4,095) MUST be reported as a change.
+- **Sources:**
+  - vendored `sources/intuit-iif.md`: "Accounts are identified by NAME"
+- **Symbolic form:** `file = header lists transactions`, `forall line: ascii(line) and tabs(line)`.
+- **Examples:** `iif-quickbooks-journal-file`
+- **Applicability:** exports to QuickBooks Desktop.
diff --git a/bookspec/spec/ledger.md b/bookspec/spec/ledger.md
new file mode 100644
index 0000000..dfee2ae
--- /dev/null
+++ b/bookspec/spec/ledger.md
@@ -0,0 +1,141 @@
+# Area: ledger
+
+The chart, the journal, posted-is-forever, corrections, control roles and
+how the books are kept.
+
+### BS-ledger-1: One money through the ledger; foreign amounts at the transaction-date rate (B-3)
+
+- **Status:** AUTHORITY (the single money, the rate); CHOICE (booking in the smallest unit, the owner, 2026-10-13)
+- **Statement:** A ledger MUST be kept in one base currency. A foreign amount MUST be booked at the rate in effect on the transaction date, rounded half away from zero to the base currency's smallest unit, and the original amount and rate kept. A line finer than the smallest unit MUST be refused, never rounded silently.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "the money that you reckon by at the beginning should be the same all through the Ledger"
+  - vendored `sources/iso-4217.md`: "Minor units" (the table of currencies by minor-unit digits; two for the US dollar)
+  - external: ASC 830-20-30-1, initial measurement in the functional currency at the rate in effect at the transaction date
+- **Symbolic form:** `base = round_half_away(foreign * rate, u)`; every booked amount `in Z * u`.
+- **Examples:** `ledger-a-fraction-of-a-cent-is-refused`
+- **Applicability:** every engine. The single-currency refusal is demonstrated; the foreign-currency booking has no example in the first edition (the schema has no foreign line).
+
+### BS-ledger-2: Five elements, closed list (B-4)
+
+- **Status:** AUTHORITY (the definitions); CONVENTION (the five-type chart); CHOICE (a child has its parent's type, the owner, 2026-10-13)
+- **Statement:** Every account MUST be exactly one of asset, liability, equity, revenue, expense. An account under a parent MUST have its parent's type.
+- **Sources:**
+  - external: FASB Concepts Statement No. 8, Chapter 4, paragraphs E16 (asset), E37 (liability), E61 (equity), E80 (revenue), E81 (expense)
+- **Symbolic form:** `type(a) in {asset, liability, equity, revenue, expense}`; `parent(a) = p implies type(a) = type(p)`.
+- **Examples:** `ledger-a-child-account-has-its-parents-type`
+- **Applicability:** every engine; engines with a finer chart (contra accounts, memo accounts) map onto the five.
+
+### BS-ledger-3: Normal balances (B-5)
+
+- **Status:** CONVENTION
+- **Statement:** An asset or expense account's balance MUST be shown as debits less credits, a liability, equity or revenue account's as credits less debits.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "This capital must always be placed as creditor"
+  - external: OpenStax, Principles of Accounting, Volume 1, section 3.1
+- **Symbolic form:** `bal(a) = D(a) - C(a)` if `type(a) in {asset, expense}`, else `C(a) - D(a)`.
+- **Examples:** `statement-the-books-balance-and-the-equation-holds`
+- **Applicability:** every engine.
+
+### BS-ledger-4: Posted is forever: the book is written only forward (B-8)
+
+- **Status:** AUTHORITY
+- **Statement:** A posted entry MUST NOT be changed or deleted. The ledger at a later time MUST contain every earlier posted entry unchanged, and a change to a record MUST leave the audit trail intact.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "You should not write backward, but always forward"
+  - vendored `sources/irs-records.md`: "A taxpayer establishes this reconciliation by demonstrating the relationship"
+  - external: Handelsgesetzbuch (HGB) section 239(3), official English translation: an entry may not be modified such that its original content can no longer be established
+- **Symbolic form:** for ledger states `S_t` and `t <= t'`: `posted(S_t)` is a prefix of `posted(S_t')`.
+- **Examples:** `ledger-a-mistake-is-reversed-never-erased`
+- **Applicability:** every engine.
+
+### BS-ledger-5: A mistake is corrected by an opposite entry, never erased (B-9)
+
+- **Status:** AUTHORITY
+- **Statement:** A mistaken entry MUST be corrected by a reversal: a new entry with the same accounts and amounts and the sides flipped, linked to the original. The original MUST remain as it was written, and the pair MUST net to zero on every account.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "entry opposite this one in the credit for the same amount"
+- **Symbolic form:** `reverse(E) = {(flip(s_i), a_i)}`; per account `signed(E) + signed(reverse(E)) = 0`.
+- **Examples:** `ledger-a-mistake-is-reversed-never-erased`
+- **Applicability:** every engine.
+
+### BS-ledger-6: An entry is reversed at most once; a closing entry never (B-10)
+
+- **Status:** CHOICE (the owner, 2026-10-13); options: reversible once, reversible repeatedly; a close never reversible
+- **Statement:** An entry MUST be reversed at most once; a second reversal of it MUST be refused. A closing entry MUST NOT be reversed, because a closed period stays closed. To restore a reversed entry, post a new entry.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "entry opposite this one in the credit for the same amount"
+- **Symbolic form:** `|{R : reversal_of(R) = E}| <= 1`; `closing(E) implies no R with reversal_of(R) = E`.
+- **Examples:** `ledger-a-mistake-is-reversed-never-erased`
+- **Applicability:** an engine declares its pick (`claims.choices`).
+
+### BS-ledger-7: Every transaction has supporting documents; records are kept (B-20)
+
+- **Status:** AUTHORITY
+- **Statement:** Every entry MUST have supporting documents, kept for the period of limitations of the return it supports (three years generally; seven for a bad debt). Evidence the books file with an entry MUST stay with it; a reversal needs none of its own.
+- **Sources:**
+  - vendored `sources/irs-records.md`: "In addition, you must keep supporting documents"
+- **Symbolic form:** `forall posted E, not reversal(E): |documents(E)| >= 1`.
+- **Examples:** none yet. The example schema has no evidence event, and wanderbooks enforces this at its tool layer, not in the ledger core; a first-edition example would assert a policy of the tool surface, which is not engine-neutral.
+- **Applicability:** a US taxpayer keeping records for a return.
+
+### BS-ledger-8: Control roles: one account each, of the right kind, moved only when empty (B-23)
+
+- **Status:** CONVENTION (a control account agrees with the records it controls); CHOICE (default codes, the owner, 2026-10-13 and 2026-10-15)
+- **Statement:** An engine that posts by role (receivables, payables, revenue, and the like) MUST give each role exactly one account, postable and of the role's type, and MUST refuse to move a role to another account while the old one holds a balance. A control account's lines MUST each belong to the document that put them there; a hand line on one MUST be refused.
+- **Sources:**
+  - external: ASC 310-10 (receivables) and ASC 405-20-40-1 (a liability is removed only when paid or released)
+- **Symbolic form:** `role` is an injective partial map from roles to accounts; `bal(control(r)) = sum of open documents of r`.
+- **Examples:** `arap-hand-control-posting-refused`
+- **Applicability:** engines with documents (invoices, bills).
+
+### BS-ledger-9: The books keep how they are kept (B-29)
+
+- **Status:** CHOICE (the owner, 2026-10-16)
+- **Statement:** The settings, conventions, decisions and open items that govern the books MUST be facts in the books, each with who decided it and when, so that replaying the books gives the same results without any state held elsewhere.
+- **Sources:**
+  - external: IRS Publication 538, Accounting Periods and Methods, "Accounting Method": the method is a matter of the books
+- **Symbolic form:** `state = fold(apply, empty, journal)`.
+- **Examples:** none yet. The schema's setup is the example's own, not a journal; replay equivalence is checked by the wanderbooks adapter (`Store::verify`) after every example, not stated as an engine-neutral expectation.
+- **Applicability:** engines that keep a journal.
+
+### BS-ledger-10: Renaming an account changes its label, nothing else (B-31)
+
+- **Status:** CHOICE (the owner, 2026-10-20)
+- **Statement:** An account MUST be renamed without changing any entry, line, balance or statement amount; every report, past periods included, prints the new name. A blank name, an unchanged name, a sibling's name (ignoring capitals and surrounding space), a name holding a nine-digit number and a name that is not one line MUST be refused.
+- **Sources:**
+  - vendored `sources/irs-records.md`: "A taxpayer establishes this reconciliation by demonstrating the relationship"
+  - vendored `sources/intuit-iif.md`: "Accounts are identified by NAME"
+- **Symbolic form:** `rename(a, n)` leaves `lines`, `bal` unchanged; `name(a) = n`.
+- **Examples:** `rename-changes-no-amount`
+- **Applicability:** every engine.
+
+### BS-ledger-11: Every revenue and expense account maps to a line of the return (B-32)
+
+- **Status:** AUTHORITY (why it matters); CHOICE (warn versus refuse, the owner, 2026-10-20); options: warn, refuse
+- **Statement:** A revenue or expense account (not a header) SHOULD carry a tax category linking it to a line of the return; under the refuse policy an engine MUST refuse to create one without a category or to clear one. A header needs none.
+- **Sources:**
+  - vendored `sources/irs-records.md`: "Your books must show your gross income, as well as your deductions and credits."
+- **Symbolic form:** `policy = refuse implies forall a in nominal, not header(a): category(a) defined`.
+- **Examples:** `tax-category-required`
+- **Applicability:** a US business filing a return.
+
+### BS-ledger-12: Evidence: extraction, dedup, annotations, settlements (B-44)
+
+- **Status:** CONVENTION
+- **Statement:** Text and facts read off a receipt MUST be derived records the books can re-make, the file's bytes staying the authority; identical bytes MUST be one file wherever they are evidence; an annotation MUST change no amount; a payment's settlements MUST be named, never guessed.
+- **Sources:**
+  - external: Revenue Procedure 98-25, section 5.01, machine-sensible records with an audit trail
+  - vendored `sources/irs-records.md`: "In addition, you must keep supporting documents"
+- **Symbolic form:** `text(file) = f(bytes(file), extractor, version)`; `bytes(a) = bytes(b) implies file(a) = file(b)`.
+- **Examples:** none yet. The example schema has no attachment or file event; an evidence example waits on a schema extension (the unit's step 5 names it as owed).
+- **Applicability:** engines that hold receipts.
+
+### BS-ledger-13: Audits and attestations (B-45)
+
+- **Status:** reserved
+- **Statement:** Reserved: allocated in the wanderbooks plan (8.0.3), not yet stated in `docs/spec/rules.md`.
+- **Sources:**
+  - none yet
+- **Symbolic form:** none yet.
+- **Examples:** none yet
+- **Applicability:** none yet.
diff --git a/bookspec/spec/partner.md b/bookspec/spec/partner.md
new file mode 100644
index 0000000..d73360f
--- /dev/null
+++ b/bookspec/spec/partner.md
@@ -0,0 +1,48 @@
+# Area: partner
+
+Members of a partnership or LLC taxed as one, and the parties the books
+deal with.
+
+### BS-partner-1: Partners share income by the partnership agreement; capital accounts carry it (B-13)
+
+- **Status:** AUTHORITY (shares, capital accounts); CHOICE (cent rounding, 2026-10-13; counting from the first close, 2026-10-16; the statement splits unclosed earnings the same running way, 2026-10-20)
+- **Statement:** A partner's distributive share of income MUST be determined by the partnership agreement. Each member's capital account MUST be one running balance of contributions, allocations and distributions; a close MUST allocate the period's net income among members by their shares, the shares summing to one. An allocation MUST sum to exactly the net, each member's share rounded to the currency's smallest unit by the largest-remainder rule and a running split carrying what earlier closes gave.
+- **Sources:**
+  - vendored `sources/irs-partnerships.md`: "A partner's distributive share of income, gain, loss, deduction, or credit shall, except as otherwise provided in this chapter, be determined by the partnership agreement."
+  - vendored `sources/irs-capital-accounts.md`: "capital account"
+- **Symbolic form:** `sum_k share_k = 1`; `part_k(t) = round_LR(share_k * N(t)) - sum_{s<t} part_k(s)` with `sum_k part_k(t) = N(t) - N(t-1)`.
+- **Examples:** `members-close.odd-cent-across-closes`, `members-close.statement-before-and-after-a-close`, `members-close.thirds-over-twelve-months`, `members-close.true-up-of-a-per-close-split`, `p3-party-members-equity-and-k1`
+- **Applicability:** entities taxed as partnerships; a count ends where the members or shares change.
+
+### BS-partner-2: Parties: one directory, no full TIN in the books (B-26)
+
+- **Status:** AUTHORITY (truncated TINs); CHOICE (the owner, 2026-10-15)
+- **Statement:** Everyone the company deals with MUST be a party with roles. Names MUST be unique among live parties, ignoring capitals and surrounding space. A party record MUST hold at most the last four digits of a TIN; the books MUST NOT hold a nine-digit number in any party field, and a full TIN lives only in a vault outside the ledger.
+- **Sources:**
+  - vendored `sources/irs-truncated-tin.md`: "truncated"
+  - vendored `sources/irs-tin-formats.md`: "taxpayer identification number"
+- **Symbolic form:** `tin_last4(p) in [0-9]{4}`; no field of a party matches `[0-9]{9}`.
+- **Examples:** `p3-party-tin-last4`
+- **Applicability:** US persons with TINs.
+
+### BS-partner-3: A party's part of an entry, and a party's totals (B-35)
+
+- **Status:** CONVENTION (the sign); CHOICE (what counts as money, the owner, 2026-10-15 and 2026-10-20); AUTHORITY (what a member's capital counts; a promise is not payment)
+- **Statement:** An entry's part for a party MUST be signed as a line on the party's own account would be (paid or given positive, received negative); money paid down on a liability counts once; an accrual counts once; a liability credit MUST NOT count as paying that liability's own creditor; a promise MUST NOT count as payment.
+- **Sources:**
+  - vendored `sources/helvering-v-price-1940.md`: "Helvering v. Price"
+  - vendored `sources/irs-capital-accounts.md`: "capital account"
+- **Symbolic form:** `part(E, p) = sum{signed lines of E on the accounts that are p's money}`; totals are sums over entries on each entry's first original's side.
+- **Examples:** `p3-party-accrual-counts-once`, `p3-party-distribution-still-owed`, `p3-party-gift-card-is-a-promise`, `p3-party-members-equity-and-k1`, `p3-party-own-liability-never-pays`, `p3-party-reversed-card-payment`, `p3-party-signs-and-reversals`
+- **Applicability:** every engine with parties.
+
+### BS-partner-4: The K-1 worksheet reports tax-basis capital beside book capital (B-36)
+
+- **Status:** AUTHORITY; CHOICE (D-41, the owner, 2026-10-20)
+- **Statement:** The K-1 worksheet MUST report each member's capital on the tax basis (beginning, contributions at adjusted tax basis, share of income for tax purposes, other changes, distributions, ending) beside the book figures; a line the books cannot know MUST be shown open, never guessed.
+- **Sources:**
+  - vendored `sources/irs-partnerships.md`: "Tax-basis method"
+  - vendored `sources/irs-partnership-basis.md`: "723"
+- **Symbolic form:** `ending = beginning + contributions + income + other - distributions`, per member, on each basis.
+- **Examples:** `partnership-k1-tax-basis-capital`, `partnership-k1-tax-basis-odd-cents`
+- **Applicability:** partnerships filing Form 1065.
diff --git a/bookspec/spec/period.md b/bookspec/spec/period.md
new file mode 100644
index 0000000..2c1a617
--- /dev/null
+++ b/bookspec/spec/period.md
@@ -0,0 +1,34 @@
+# Area: period
+
+Periods and closes, and what an omitted date means.
+
+### BS-period-1: Revenue and expenses close into profit and loss, and that into capital (B-11)
+
+- **Status:** AUTHORITY (the mechanics); the account the net lands in depends on the entity
+- **Statement:** Closing a period MUST post an entry that brings every revenue and expense account's balance through the period's last day to zero and credits equity with exactly revenue less expenses; the entry MUST balance. A corporation closes into retained earnings, a partnership into each partner's capital (BS-partner-1).
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "must then be transferred for its closing (saldo) into the capital account"
+  - external: OpenStax, Principles of Accounting, Volume 1, section 5.1: temporary accounts are closed at the end of each accounting period
+- **Symbolic form:** for nominal `n`: `bal_n(close) = 0`; `E' = E + (R - X)` (`Bookspec.law_net_income_articulates`).
+- **Examples:** `period-a-close-sweeps-the-year-into-capital`
+- **Applicability:** every entity; the target account differs by entity type.
+
+### BS-period-2: A closed period takes no new postings; periods close in order (B-12)
+
+- **Status:** CONVENTION
+- **Statement:** An entry dated within a closed period MUST be refused. Periods MUST close in order, and MUST nest (a month in a quarter in a year) and never partially overlap.
+- **Sources:**
+  - vendored `sources/irs-periods-and-methods.md`: "A tax year is an annual accounting period for keeping records and reporting income and expenses"
+- **Symbolic form:** `date(E) in closed(P) implies post(E)` is refused; `P, Q` periods: nested or disjoint.
+- **Examples:** `period-a-close-sweeps-the-year-into-capital`
+- **Applicability:** every engine that closes.
+
+### BS-period-3: A report asked for without dates covers this fiscal year so far (B-30)
+
+- **Status:** AUTHORITY (the period); CHOICE (the default, the owner, 2026-10-20)
+- **Statement:** A report asked for with no dates MUST cover the fiscal year containing today, from its first day through today; an omitted start is the first day of the fiscal year holding the end; a start after today with no end MUST be refused; an end before the start MUST be refused.
+- **Sources:**
+  - vendored `sources/irs-periods-and-methods.md`: "A tax year is an annual accounting period for keeping records and reporting income and expenses"
+- **Symbolic form:** `to = today`; `from = fiscal_year_start(to)`; `from <= to`.
+- **Examples:** `default-period-fiscal-year-to-date`
+- **Applicability:** every engine with a fiscal-year setting.
diff --git a/bookspec/spec/prepaid.md b/bookspec/spec/prepaid.md
new file mode 100644
index 0000000..9f644e5
--- /dev/null
+++ b/bookspec/spec/prepaid.md
@@ -0,0 +1,14 @@
+# Area: prepaid
+
+Prepaid expenses and deferred revenue.
+
+### BS-prepaid-1: Prepaid expenses and deferred revenue are recognized over the period benefited or earned (B-16)
+
+- **Status:** AUTHORITY (revenue); CONVENTION (prepaids)
+- **Statement:** A payment received before a good or service is transferred MUST be a contract liability, recognized as revenue as the performance obligation is satisfied; a prepaid expense MUST be an asset recognized as the benefit is used. A schedule MUST recognize exactly its total over its months: by the day (first and last partial months by their days, the last taking the remainder) or in equal months from the first.
+- **Sources:**
+  - external: ASC 606-10-45-2 (contract liability); ASC 606-10-25-23 (recognize revenue when a performance obligation is satisfied); ASC 340-10-05-4 and ASC 210-10-45-1(g)
+  - vendored `sources/irs-capitalization.md`: "1.263(a)-4(f)"
+- **Symbolic form:** `sum_m recognized_m = total`; `recognized_m >= 0`.
+- **Examples:** `schedule-daily-deferred-revenue`, `schedule-daily-small-first-and-last-month`, `schedule-equal-months-start-on-the-first`
+- **Applicability:** accrual-basis entities.
diff --git a/bookspec/spec/revenue.md b/bookspec/spec/revenue.md
new file mode 100644
index 0000000..3077542
--- /dev/null
+++ b/bookspec/spec/revenue.md
@@ -0,0 +1,13 @@
+# Area: revenue
+
+How revenue is presented.
+
+### BS-revenue-1: Platform payouts are recorded gross when the business is the principal (B-17)
+
+- **Status:** AUTHORITY
+- **Statement:** When the business controls the good or service before it is transferred to the customer (is the principal), a payout from a platform MUST be recorded as revenue in the gross amount of consideration, the platform's fee as an expense, and the deposit as gross less fee. An agent records only its fee or commission.
+- **Sources:**
+  - external: ASC 606-10-55-37, 55-37A and 55-37B (principal: gross amount of consideration); ASC 606-10-55-38 (agent: the fee or commission); ASC 606-10-55-39 (indicators)
+- **Symbolic form:** `revenue = gross`; `expense = fee`; `deposit = gross - fee`.
+- **Examples:** none yet. The schema has no payout event; the example for a settlement through a processor (BS-arap-6) shows the same gross presentation for a customer payment.
+- **Applicability:** principal versus agent is a judgment under 55-39; the CPA confirms.
diff --git a/bookspec/spec/rules-index.md b/bookspec/spec/rules-index.md
index aec30a6..8d30d5f 100644
--- a/bookspec/spec/rules-index.md
+++ b/bookspec/spec/rules-index.md
@@ -6,36 +6,36 @@ what its statement rests on and the examples that demonstrate it.
 
 A rule whose only source is a human choice carries rules.md's **CHOICE**, bookspec's status of the same name:
 the specification names the options, an engine declares its pick
-(`claims.choices`, `bookspec_checker::Claims`). Rules B-39, B-40 and B-43
-to B-45 are allocated in `plan/served.md` 8.0.3 and not yet stated: their
+(`claims.choices`, `bookspec_checker::Claims`). Rules B-39, B-40, B-43
+and B-45 are allocated in `plan/served.md` 8.0.3 and not yet stated: their
 identifier and area are fixed here so a later unit fills them in
 without moving anyone else's number.
 
 | B | bookspec id | area | status | rule | examples |
 |---|---|---|---|---|---|
-| B-1 | `BS-entry-1` | entry | AUTHORITY | Every entry is a double entry: debits equal credits | — |
-| B-2 | `BS-entry-2` | entry | CONVENTION | A line's amount is positive; its side gives the direction | — |
-| B-3 | `BS-ledger-1` | ledger | AUTHORITY | One money through the ledger; foreign amounts at the transaction-date rate | — |
-| B-4 | `BS-ledger-2` | ledger | AUTHORITY | Five elements, closed list | — |
-| B-5 | `BS-ledger-3` | ledger | CONVENTION | Normal balances | — |
-| B-6 | `BS-statement-1` | statement | AUTHORITY | The trial balance balances | — |
-| B-7 | `BS-statement-2` | statement | AUTHORITY | The accounting equation | — |
-| B-8 | `BS-ledger-4` | ledger | AUTHORITY | Posted is forever: the book is written only forward | — |
-| B-9 | `BS-ledger-5` | ledger | AUTHORITY | A mistake is corrected by an opposite entry, never erased | — |
-| B-10 | `BS-ledger-6` | ledger | CHOICE | An entry is reversed at most once; a closing entry never | — |
-| B-11 | `BS-period-1` | period | AUTHORITY | Revenue and expenses close into profit and loss, and that into capital | — |
-| B-12 | `BS-period-2` | period | CONVENTION | A closed period takes no new postings; periods close in order | — |
+| B-1 | `BS-entry-1` | entry | AUTHORITY | Every entry is a double entry: debits equal credits | `entry-an-unbalanced-entry-is-refused`, `statement-the-books-balance-and-the-equation-holds` |
+| B-2 | `BS-entry-2` | entry | CONVENTION | A line's amount is positive; its side gives the direction | `entry-a-line-amount-is-positive` |
+| B-3 | `BS-ledger-1` | ledger | AUTHORITY | One money through the ledger; foreign amounts at the transaction-date rate | `ledger-a-fraction-of-a-cent-is-refused` |
+| B-4 | `BS-ledger-2` | ledger | AUTHORITY | Five elements, closed list | `ledger-a-child-account-has-its-parents-type` |
+| B-5 | `BS-ledger-3` | ledger | CONVENTION | Normal balances | `statement-the-books-balance-and-the-equation-holds` |
+| B-6 | `BS-statement-1` | statement | AUTHORITY | The trial balance balances | `statement-the-books-balance-and-the-equation-holds` |
+| B-7 | `BS-statement-2` | statement | AUTHORITY | The accounting equation | `statement-the-books-balance-and-the-equation-holds` |
+| B-8 | `BS-ledger-4` | ledger | AUTHORITY | Posted is forever: the book is written only forward | `ledger-a-mistake-is-reversed-never-erased` |
+| B-9 | `BS-ledger-5` | ledger | AUTHORITY | A mistake is corrected by an opposite entry, never erased | `ledger-a-mistake-is-reversed-never-erased` |
+| B-10 | `BS-ledger-6` | ledger | CHOICE | An entry is reversed at most once; a closing entry never | `ledger-a-mistake-is-reversed-never-erased` |
+| B-11 | `BS-period-1` | period | AUTHORITY | Revenue and expenses close into profit and loss, and that into capital | `period-a-close-sweeps-the-year-into-capital` |
+| B-12 | `BS-period-2` | period | CONVENTION | A closed period takes no new postings; periods close in order | `period-a-close-sweeps-the-year-into-capital` |
 | B-13 | `BS-partner-1` | partner | AUTHORITY | Partners share income by the partnership agreement; capital accounts carry it | `members-close.odd-cent-across-closes`, `members-close.statement-before-and-after-a-close`, `members-close.thirds-over-twelve-months`, `members-close.true-up-of-a-per-close-split`, `p3-party-members-equity-and-k1` |
-| B-14 | `BS-statement-3` | statement | AUTHORITY | Statements: P&L for a period; cash flows by the direct method | `cash-flow.debt-to-equity`, `cash-flow.government-fees`, `cash-flow.paid-on-the-companys-behalf`, `cash-flow.part-cash-purchase`, `cash-flow.reversal-of-a-reversal`, `cash-flow.reversed-property-contribution`, `cash-flow.two-member-llc-first-year` |
+| B-14 | `BS-statement-3` | statement | AUTHORITY | Statements: P&L for a period; cash flows by the direct method | `cash-flow.debt-to-equity`, `cash-flow.government-fees`, `cash-flow.paid-on-the-companys-behalf`, `cash-flow.part-cash-purchase`, `cash-flow.reversal-of-a-reversal`, `cash-flow.reversed-property-contribution`, `cash-flow.two-member-llc-first-year`, `period-a-close-sweeps-the-year-into-capital` |
 | B-15 | `BS-asset-1` | asset | CONVENTION | Depreciation: straight line, salvage never depreciated, partial months by days | `assets-acquired-before-in-service`, `assets-a-reversed-run-is-not-posted`, `assets-book-value-is-what-the-books-carry`, `depreciation-catch-up-month`, `depreciation-disposal-after-a-late-change-undone`, `depreciation-disposal-before-a-later-run`, `depreciation-disposal-in-final-month`, `depreciation-disposal-inside-a-posted-month`, `depreciation-disposal-mid-month`, `depreciation-final-month-by-days`, `depreciation-final-month-drift`, `depreciation-reversal-before-its-run-is-refused`, `depreciation-run-reversed-after-its-month` |
 | B-16 | `BS-prepaid-1` | prepaid | AUTHORITY | Prepaid expenses and deferred revenue are recognized over the period benefited or earned | `schedule-daily-deferred-revenue`, `schedule-daily-small-first-and-last-month`, `schedule-equal-months-start-on-the-first` |
 | B-17 | `BS-revenue-1` | revenue | AUTHORITY | Platform payouts are recorded gross when the business is the principal | — |
 | B-18 | `BS-arap-1` | arap | CONVENTION | Aging buckets: Current, 1-30, 31-60, 61-90, 90+ days past due | — |
 | B-19 | `BS-1099-1` | 1099 | AUTHORITY | 1099 reporting thresholds, payment methods, and decisions | `1099-a-dated-status-applies-by-payment-date`, `1099-a-members-check-through-financing-counts`, `1099-and-party-totals-for-a-members-payment`, `1099-card-payments-are-excluded`, `1099-money-between-own-accounts-pays-no-one`, `1099-money-from-a-payee-is-netted-only-as-a-refund`, `1099-the-threshold-is-the-years`, `1099-worksheet-through-as-of` |
 | B-20 | `BS-ledger-7` | ledger | AUTHORITY | Every transaction has supporting documents; records are kept | — |
-| B-21 | `BS-entry-3` | entry | AUTHORITY | Exact amounts in the books; rounding only on returns | — |
+| B-21 | `BS-entry-3` | entry | AUTHORITY | Exact amounts in the books; rounding only on returns | `entry-cents-add-exactly` |
 | B-22 | `BS-asset-2` | asset | AUTHORITY | Expense or capitalize (book policy, mirrors tax) | — |
-| B-23 | `BS-ledger-8` | ledger | CONVENTION | Control roles: one account each, of the right kind, moved only when empty | — |
+| B-23 | `BS-ledger-8` | ledger | CONVENTION | Control roles: one account each, of the right kind, moved only when empty | `arap-hand-control-posting-refused` |
 | B-24 | `BS-asset-3` | asset | CHOICE | Asset tags: one label per asset, never reused | — |
 | B-25 | `BS-asset-4` | asset | AUTHORITY | Tax figures beside book value: the section 723 basis, the depreciable basis, the section 704(c) built-in gain | `assets-723-basis-apart-from-depreciable-basis`, `assets-built-in-gain-fixed-at-contribution`, `assets-four-contributed-devices` |
 | B-26 | `BS-partner-2` | partner | AUTHORITY | Parties: one directory, no full TIN in the books | `p3-party-tin-last4` |
@@ -56,5 +56,5 @@ without moving anyone else's number.
 | B-41 | `BS-arap-5` | arap | CHOICE | A debt that will not be collected is written off, and a recovery is income | `bad-debt-direct-write-off` |
 | B-42 | `BS-arap-6` | arap | CONVENTION | A settlement is exact, one party, and names its lines; the gross discount and the gross fee | — |
 | B-43 | `BS-entry-5` | entry | — | Drafts and evidence (allocated, not yet stated) | — |
-| B-44 | `BS-ledger-12` | ledger | — | Evidence: extraction, dedup, annotations, settlements (stated in rules.md; its bookspec example comes with P13 step 5) | — |
+| B-44 | `BS-ledger-12` | ledger | CONVENTION | Evidence is read from the bytes, never trusted over them; identical files are kept once | — |
 | B-45 | `BS-ledger-13` | ledger | — | Audits and attestations (allocated, not yet stated) | — |
diff --git a/bookspec/spec/statement.md b/bookspec/spec/statement.md
new file mode 100644
index 0000000..887a559
--- /dev/null
+++ b/bookspec/spec/statement.md
@@ -0,0 +1,56 @@
+# Area: statement
+
+Reports: the trial balance, the accounting equation, the period
+statements, the package as of a day, the project.
+
+### BS-statement-1: The trial balance balances (B-6)
+
+- **Status:** AUTHORITY
+- **Statement:** The trial balance MUST list each account's balance as a debit or a credit, and the sum of the debits MUST equal the sum of the credits, as of every day.
+- **Sources:**
+  - vendored `sources/pacioli-1494.md`: "should be equal to the total of the debits"
+  - vendored `sources/irs-records.md`: "the total debits must equal the total credits"
+- **Symbolic form:** `sum{max(0, D_a - C_a)} = sum{max(0, C_a - D_a)}`, equivalently `sum_a (D_a - C_a) = 0` (`Bookspec.law_trial_balance`).
+- **Examples:** `statement-the-books-balance-and-the-equation-holds`
+- **Applicability:** every engine.
+
+### BS-statement-2: The accounting equation (B-7)
+
+- **Status:** AUTHORITY
+- **Statement:** At every date, assets MUST equal liabilities plus equity plus revenue less expenses, each on its normal side. Income not yet closed is part of equity.
+- **Sources:**
+  - external: FASB Concepts Statement No. 8, Chapter 4, paragraph E62: equity is the difference between the entity's assets and its liabilities
+- **Symbolic form:** `A = L + E + (R - X)` (`Bookspec.law_accounting_equation`).
+- **Examples:** `statement-the-books-balance-and-the-equation-holds`
+- **Applicability:** every engine.
+
+### BS-statement-3: Statements: P&L for a period; cash flows by the direct method (B-14)
+
+- **Status:** AUTHORITY, except where marked CONVENTION or CHOICE
+- **Statement:** The profit and loss for a period MUST report revenue and expense activity within it and MUST exclude closing entries. The statement of cash flows MUST report the cash receipts and payments of the period by operating, investing and financing activity (the direct method); transfers among cash accounts MUST NOT be flows; the three sections MUST sum to the change in the cash accounts' balances; noncash investing and financing MUST be disclosed apart.
+- **Sources:**
+  - external: ASC 230-10-45-1 (cash effects of operating, investing and financing); 230-10-45-4 and 45-5 (cash and cash equivalents; transfers among them are not cash flows); 230-10-45-14 (cash receipts and payments from operating activities); 230-10-45-25 (classes of operating cash payments); 230-10-50-3 (noncash investing and financing)
+  - vendored `sources/fasb-asc.md`: "230-10-45"
+- **Symbolic form:** `operating + investing + financing = cash_end - cash_begin` (`Bookspec.law_cash_flow_is_change_in_cash`); an entry contributes its net movement of the cash accounts only.
+- **Examples:** `cash-flow.debt-to-equity`, `cash-flow.government-fees`, `cash-flow.paid-on-the-companys-behalf`, `cash-flow.part-cash-purchase`, `cash-flow.reversal-of-a-reversal`, `cash-flow.reversed-property-contribution`, `cash-flow.two-member-llc-first-year`, `period-a-close-sweeps-the-year-into-capital`
+- **Applicability:** accrual and cash basis entities reporting under US GAAP.
+
+### BS-statement-4: A package as of a day shows the books through that day (B-33)
+
+- **Status:** CONVENTION; CHOICE for the 1099 worksheet (the owner, 2026-10-20)
+- **Statement:** A report or package made as of a day MUST reflect nothing dated after it: no figure, entry, receipt or worksheet row. Balances run through the day; a period's activity from the period's start through it.
+- **Sources:**
+  - vendored `sources/irs-periods-and-methods.md`: "A tax year is an annual accounting period for keeping records and reporting income and expenses"
+- **Symbolic form:** `report(as_of) = report(books restricted to date <= as_of)`.
+- **Examples:** `as-of-package-stops-at-as-of`
+- **Applicability:** every engine that produces a package.
+
+### BS-statement-5: A project is a class with its facts; its figures are its tagged lines (B-37)
+
+- **Status:** CHOICE (the owner, 2026-10-21); CONVENTION (job costing); AUTHORITY (costs of work on spec are expensed)
+- **Statement:** A project's revenue, expenses and net MUST be exactly the revenue and expense lines tagged with it, closes left out; its to-date figures MUST be every tagged line through the date; an on-spec project's unrecovered cost MUST be its expenses less its revenue to date, never below zero.
+- **Sources:**
+  - external: ASC 340-40-25-5 and 340-40-25-7 (costs to fulfil a contract); ASC 450-30-25-1 (gain contingencies)
+- **Symbolic form:** `net(p) = sum{signed credit-normal value of tagged revenue and expense lines of p}`.
+- **Examples:** `projects-invoice-and-bill-lines-count-by-project`, `projects-net-is-its-tagged-lines`, `projects-on-spec-costs-are-expenses`
+- **Applicability:** engines with classes or projects.
diff --git a/crates/ledger-core/tests/bookspec.rs b/crates/ledger-core/tests/bookspec.rs
index d49942a..624b82e 100644
--- a/crates/ledger-core/tests/bookspec.rs
+++ b/crates/ledger-core/tests/bookspec.rs
@@ -192,6 +192,14 @@ fn refusal(e: &LedgerError) -> String {
         LedgerError::InvalidDepreciationPeriod(_) => "invalid_depreciation_period",
         LedgerError::InvalidSchedule(_) => "invalid_schedule",
         LedgerError::UntaggedControlLine { .. } => "untagged_control_line",
+        LedgerError::UnbalancedEntry { .. } => "unbalanced",
+        LedgerError::TooFewLines => "too_few_lines",
+        LedgerError::NegativeAmountLine => "negative_amount",
+        LedgerError::ZeroAmountLine => "zero_amount",
+        LedgerError::FinerThanMinorUnit { .. } => "finer_than_minor_unit",
+        LedgerError::ParentTypeMismatch { .. } => "parent_type_mismatch",
+        LedgerError::EntryAlreadyReversed(..) => "already_reversed",
+        LedgerError::ClosedPeriod(..) => "period_closed",
         other => return format!("another refusal: {other}"),
     }
     .to_string()
@@ -1029,7 +1037,12 @@ impl<'a> Books<'a> {
     ) -> Result<(), StoreError> {
         let money = |s: &str| {
             let amount = exact(s, what);
-            assert!(amount > Decimal::ZERO, "{what}: amounts are positive");
+            // Only a refused entry carries an amount the books refuse
+            // (the schema checks it).
+            assert!(
+                amount > Decimal::ZERO || e.refused.is_some(),
+                "{what}: amounts are positive"
+            );
             amount
         };
         let day = || when.expect("checked: dated");
diff --git a/docs/spec/rules.md b/docs/spec/rules.md
index dfe63e8..4e279d2 100644
--- a/docs/spec/rules.md
+++ b/docs/spec/rules.md
@@ -3429,6 +3429,11 @@ The Lean step is `Documents.Step.document` with every control line tagged
 
 ## B-44 Evidence is read from the bytes, never trusted over them; identical files are kept once
 
+**bookspec:** `BS-ledger-12`
+
+**Status:** CONVENTION (the SOURCE block below; Rev. Proc. 98-25 and Pub. 583 for
+the audit trail)
+
 ```text
 GOAL: a receipt's text and the facts read off it are derived records the
       books can re-make; the file's bytes stay the authority; the same
diff --git a/docs/testing.md b/docs/testing.md
index 108bd8d..49a67b2 100644
--- a/docs/testing.md
+++ b/docs/testing.md
@@ -2917,6 +2917,71 @@ span (acquisition through as-of, 0.00 where the schedule reaches no month)
 and every `answer_*` figure against the loader's same check (the two must
 agree on all 56 examples).
 
+## P13 steps 4 and 5: the specification text, the laws, the derivation, GnuCash (2026-10-29)
+
+Step 4 writes the first edition (`bookspec/spec/*.md`, 667 lines of the 3,300
+its 60 pages allow), puts the five laws in Lean (`bookspec/lean`, ported from
+`verify/lean`: debits equal credits, the accounting equation, the trial
+balance balances, net income articulates to equity, the cash-flow sections
+sum to the change in cash) and adds eight examples for the laws that had
+none (`entry-an-unbalanced-entry-is-refused`,
+`entry-a-line-amount-is-positive`, `entry-cents-add-exactly`,
+`ledger-a-fraction-of-a-cent-is-refused`,
+`ledger-a-child-account-has-its-parents-type`,
+`ledger-a-mistake-is-reversed-never-erased`,
+`statement-the-books-balance-and-the-equation-holds`,
+`period-a-close-sweeps-the-year-into-capital`); every figure is worked by
+hand in the file and the adapter checks the engine against it. Step 5 adds
+the checker's own derivation (`bookspec/checker/src/derive.rs`) and GnuCash
+as a second engine (`bookspec/gnucash`). Not done: step 6 (the repository of
+its own), and the examples for rules whose events or queries the schema does
+not have (BS-entry-4, BS-ledger-7, -9, -12, BS-asset-2, -3, BS-revenue-1,
+BS-arap-1, -6, BS-format-1); each says so in its section.
+
+- **`bookspec/checker` `tests/spec.rs`:** `every_rule_has_its_section` (45
+  sections, in the file of their area, headed with the B-number),
+  `every_stated_rule_is_complete` (status agrees with the catalogue, MUST /
+  SHOULD / MAY, a symbolic form, applicability; a reserved rule says so),
+  `the_examples_are_the_catalogues` (a section lists exactly the catalogue's
+  examples; "none yet" says why), `every_citation_resolves` (every vendored
+  source exists and every quoted pin is verbatim in it, after whitespace and
+  typographic quotes; an external reference is exact), `the_edition_fits_its_page_budget`,
+  `rules_without_examples_are_not_claimable`.
+- **`bookspec/checker` `tests/lean.rs`:** `the_five_laws_are_stated_and_audited`
+  (no `sorry`), `the_laws_use_standard_axioms_only` (runs `lake build` and
+  `lake env lean Audit.lean` when Lean is installed; skips with a message
+  otherwise).
+- **`bookspec/checker` `tests/derive.rs`:** `no_example_disagrees_with_its_derivation`,
+  `the_law_examples_are_derived_in_full` (no skipped result),
+  `a_wrong_expectation_is_caught` (one cent moved; a refusal the rules do not
+  justify).
+- **`bookspec/gnucash` `tests/gnucash.rs`** (ignored: needs Docker and the
+  image `just oracle` builds; run with `cargo test -p bookspec-gnucash --
+  --ignored`): `gnucash_differs_only_where_it_was_adjudicated` (the three
+  differences, no others, and BS-entry-3, BS-ledger-3, BS-statement-1 and
+  BS-statement-2 pass) and
+  `what_gnucash_did_with_the_entries_the_specification_refuses` (the
+  evidence: ten dollars and 200.00 parked in an Imbalance account, 10.005
+  rounded to 10.01).
+- **`ledger-core` `tests/bookspec.rs`:** `every_bookspec_example_holds` and
+  `the_runner_reports_every_claimed_rule_green`, unchanged in what they
+  prove, now over 66 examples; `BS-entry-1` to `BS-entry-3`, `BS-ledger-1` to
+  `-6`, `BS-ledger-8`, `BS-statement-1`, `-2`, `BS-period-1` and `-2` are now
+  claimed. The adapter's `refusal` maps eight more engine errors to the
+  examples' words.
+
+**For P12 (mutation targets, none run, D-33):** the adapter's `refusal` arms
+(`UnbalancedEntry`, `NegativeAmountLine`, `ZeroAmountLine`,
+`FinerThanMinorUnit`, `ParentTypeMismatch`, `EntryAlreadyReversed`,
+`ClosedPeriod`), each pinned by the example that expects it, and the
+`money` closure's positivity test for an accepted entry; `rule_for_refusal`'s
+new arms; `schema::check_amount`'s `positive` flag for a refused entry;
+`derive`'s `refusal_justified` arms (each reason against its symbolic
+condition), `Model::post`'s close (a debit-normal balance credits, the
+equity line's sign), `signed`'s date window and `closings` flag, and the
+accounting-equation check; the spec test's pin search (a mutant that skips
+the quote check passes only if `every_citation_resolves` has no bad pin).
+
 ## U0b: one attention engine over `PackageBooks` (2026-10-26)
 
 Needs attention moved out of the viewer into `ledger-package::attention`
diff --git a/plan/served.md b/plan/served.md
index a53083a..c929803 100644
--- a/plan/served.md
+++ b/plan/served.md
@@ -1649,7 +1649,15 @@ Each unit follows the 8.0.4 template. "A-n" is an owner answer numbered in 8.3.1
 5. **Files:** owns `bookspec/**`; touches `crates/ledger-core/tests/bookspec.rs`, `crates/ledger-package/tests/package.rs`, `docs/spec/rules.md` (ids), `Cargo.toml` (workspace members if the checker joins the workspace).
 6. **Tests and proofs:** `every_bookspec_example_holds` unchanged; `bookspec/checker` tests (the schema, the derivations); `bookspec/lean` builds with standard axioms only.
 7. **Done when:** (1) the checker crate exists and `just check` still checks all 56+ examples; (2) the `Engine` trait and the wanderbooks adapter run the runner green for every claimed rule; (3) every B-rule has an id, statement, source and example; (4) the five laws are theorems in `bookspec/lean`; (5) the GnuCash adapter runs and its differences are settled from the sources (recorded in the As-built block).
-8. **As built:** none yet.
+8. **As built:** steps 1-3 landed 2026-10-26 (`579d0eed`); steps 4 and 5 built 2026-10-29 on branch `P13` (step 6 not started: it waits on the owner, see below).
+   - **Step 4, the text.** `bookspec/spec/` holds `00-model.md` (definitions, the model, the five laws, how an example is checked) and one file per area (`entry`, `ledger`, `statement`, `period`, `partner`, `asset`, `prepaid`, `revenue`, `arap`, `1099`, `format`), 667 lines of the 3,300 a 60-page edition allows. Every B-rule has a section `### BS-<area>-<n> (B-n)` with status, MUST/SHOULD/MAY statement, sources, symbolic form, examples and applicability; B-39, B-40, B-43, B-45 are reserved sections (allocated, not yet stated in `rules.md`); B-44, stated in `rules.md`, now carries its `bookspec:` line and CONVENTION status (catalogue and index updated). `checker/tests/spec.rs` fails the build on a missing section, a statement without a modal verb, a status that differs from the catalogue, examples that differ from the catalogue, a vendored pin that is not verbatim in its source (whitespace and curly quotes normalized), or more than 60 pages.
+   - **The five laws** are Lean theorems `Bookspec.law_debits_equal_credits`, `law_accounting_equation`, `law_trial_balance`, `law_net_income_articulates`, `law_cash_flow_is_change_in_cash` in `bookspec/lean` (Basic, Entry, Statements, Closing, Ledger ported from `verify/lean` under the namespace `Bookspec`; `Laws.lean` states them; `Audit.lean` prints their axioms: `propext`, `Quot.sound`, `Classical.choice` only). `checker/tests/lean.rs` builds and audits when Lean is installed.
+   - **New examples (8)**, each figure worked by hand in the file: `entry-an-unbalanced-entry-is-refused`, `entry-a-line-amount-is-positive`, `entry-cents-add-exactly`, `ledger-a-fraction-of-a-cent-is-refused`, `ledger-a-child-account-has-its-parents-type`, `ledger-a-mistake-is-reversed-never-erased`, `statement-the-books-balance-and-the-equation-holds`, `period-a-close-sweeps-the-year-into-capital` (66 in all). Rules now with an example: B-1 to B-12 and B-21, B-23 (`arap-hand-control-posting-refused` also shows it). New refusal words: `unbalanced`, `too_few_lines`, `negative_amount`, `zero_amount`, `finer_than_minor_unit`, `parent_type_mismatch`, `already_reversed`, `period_closed`; a refused entry may carry a non-positive amount. Finding while writing: `close ... to = "retained_earnings"` posts to the role account 3999 Retained Earnings, not to a setup capital account; the example says so.
+   - **Step 5, the derivation.** `bookspec/checker/src/derive.rs` is an engine-free reference model (exact decimals) that replays entries, reversals, a close to retained earnings, bills and invoices, derives `trial_balance`, `balances`, `profit_and_loss` and `entry` figures plus the law checks (books net to zero, A = L + E + (R - X)) and checks each refusal against its rule; everything else is reported `Skipped`, never passed. `checker/tests/derive.rs`: no example disagrees; the eight law examples are derived in full; a figure moved by a cent and an unjustified refusal are both caught.
+   - **The runner against wanderbooks** (`the_runner_reports_every_claimed_rule_green`) is green for every claimed rule, now including BS-entry-1 to -3, BS-ledger-1 to -6 and -8, BS-statement-1 and -2, BS-period-1 and -2.
+   - **GnuCash, the second engine** (`bookspec/gnucash`, ignored tests; needs the `just oracle` image). It claims the rules whose examples ask only for balances. Passes BS-entry-3, BS-ledger-3, BS-statement-1, BS-statement-2. Three differences, settled from the sources and pinned by `gnucash/tests/gnucash.rs`: GnuCash books an unbalanced entry and parks the difference in `Imbalance-USD` (BS-entry-1 refuses it: Pacioli ch. 36, Pub. 583); it reads a credit of minus 100.00 as a debit (BS-entry-2 is a CONVENTION that removes the ambiguity); it rounds 10.005 to 10.01 silently (BS-ledger-1's CHOICE, found by the first cross-check, is not to). The examples stand in each case. GnuCash has no reversal link, so BS-ledger-5, -6 are not claimed by it.
+   - **Not done, and why.** (a) Done when 3 is met for the rules the schema can show; these stated rules still have no example because the schema has no event or query for them: BS-entry-4 (B-28), BS-ledger-7 (B-20), -9 (B-29), -12 (B-44), BS-asset-2 (B-22), -3 (B-24), BS-revenue-1 (B-17), BS-arap-1 (B-18), BS-arap-6 (B-42, whose allocated names `arap-settlement-exact` and `processor-fee-gross-presentation` wait on a payment/settlement event and an aging query), BS-format-1 (B-27); each section says why. B-39, B-40, B-43, B-45 are unstated in `rules.md`. (b) Step 6, the repository of its own, is the owner's call (a public repository, CC BY 4.0 for the text) and waits on step 5 being stable; nothing was pushed. (c) The derivation covers the ledger-core examples; depreciation, schedules, members, 1099s, formats and the cash-flow sections are skipped by the model and checked by the engines only.
+
 
 ### 8.3 P4b reference design: receivables and payables, first class (D-45)