feat(bookspec): the specification text and an example for the ledger's own laws (P13 step 4)

bookspec/spec holds the first edition: the model and the five laws
(00-model.md) and one file per area, each B-rule a section with its
status, a MUST/MAY statement, sources pinned either to a vendored source
with a verbatim quotation or to an exact external paragraph, its symbolic
form, its examples and its applicability. B-39, B-40, B-43 and B-45 are
reserved sections (allocated, not yet stated in rules.md); B-44 is stated
in rules.md and now carries its bookspec id and CONVENTION status.

Eight new examples show the laws that had none, each figure worked by
hand: an unbalanced entry is refused (Pacioli ch. 36, Pub. 583), a
negative or zero line is refused, a fraction of a cent is refused (ISO
4217), a child account takes its parent's type, the trial balance and the
accounting equation on one small book (cash 6550.25 = loan 2000 + capital
5000 + (sales 750.50 - rent 1200.25)), a reversal leaves the original
standing and a second reversal is refused, a close sweeps revenue and
expenses into Retained Earnings (3999) and the closed quarter takes no
late entry, and cents add exactly. The refusal vocabulary gains
unbalanced, negative_amount, zero_amount, too_few_lines,
finer_than_minor_unit, parent_type_mismatch, already_reversed and
period_closed; a refused entry may carry a non-positive amount.

The checker's spec.rs fails the build on a rule without its section, a
statement without MUST/SHOULD/MAY, a pin that is not verbatim in its
vendored source, examples that differ from the catalogue, or more than 60
pages.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp

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`).