diff --git a/crates/ledger-core/src/arap.rs b/crates/ledger-core/src/arap.rs
index 47a39db..cd8ebd5 100644
--- a/crates/ledger-core/src/arap.rs
+++ b/crates/ledger-core/src/arap.rs
@@ -2,8 +2,10 @@
 //!
 //! Invoices and bills are business documents that auto-post journal entries:
 //!
-//! * `create_invoice`: Dr `1200` Accounts Receivable, Cr `4000` Revenue.
-//! * `create_bill`: Dr `6999` General Expenses, Cr `2000` Accounts Payable.
+//! * `create_invoice`: Dr `1200` Accounts Receivable, Cr each line's account
+//!   (the revenue role, `4000`, when a line names none).
+//! * `create_bill`: Dr each line's account (the general-expenses role,
+//!   `6999`, when a line names none), Cr `2000` Accounts Payable.
 //! * `receive_payment`: Dr Cash, Cr A/R.
 //! * `pay_bill`: Dr A/P, Cr Cash.
 //!
@@ -21,10 +23,15 @@
 //! closed period.
 
 use crate::LedgerError;
-use chrono::NaiveDate;
+use chrono::{Datelike, Days, NaiveDate};
 use rust_decimal::Decimal;
 use serde::{Deserialize, Serialize};
 
+/// The most days a payment term may run: ten years, far beyond any trade
+/// term, and short of the calendar's end for every document date the
+/// books can hold (B-39).
+pub const MAX_TERMS_DAYS: u16 = 3_650;
+
 /// Opaque customer handle.
 pub type CustomerId = u64;
 /// Opaque vendor handle.
@@ -93,6 +100,17 @@ pub enum DocumentStatus {
     Paid,
 }
 
+/// The two kinds of document (an invoice or a bill), without an id: what
+/// a line's account rule and the journal's event names key on.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum DocumentKind {
+    /// A sales invoice (receivables).
+    Invoice,
+    /// A vendor bill (payables).
+    Bill,
+}
+
 /// A document: an invoice or a bill, the two kinds whose ledger lines
 /// carry their document ([`DocTag`]).
 #[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
@@ -407,6 +425,393 @@ impl PaymentDetails {
     }
 }
 
+/// How a document's payment terms count their days (rules.md B-39; plan
+/// P4b S4.1): from the document's date, from the end of its month, or a
+/// date the parties agreed.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum TermsKind {
+    /// Due on the document's own date.
+    DueOnReceipt,
+    /// Due `n` days after the document's date (Net n).
+    Net(u16),
+    /// Due `n` days after the last day of the document's month (Net n
+    /// EOM).
+    NetEom(u16),
+    /// Due on a date the parties agreed; the caller passes it to
+    /// [`Terms::due_date`], and [`Terms::describe`] carries it for
+    /// people.
+    Custom,
+}
+
+/// An early-payment discount: take `percent_bp` off if paid within
+/// `days` of the document's date ("2/10 net 30").
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub struct EarlyDiscount {
+    /// The discount in basis points: 1 to 9,999 (0.01% to 99.99%).
+    pub percent_bp: u32,
+    /// The days after the document's date the discount is open.
+    pub days: u16,
+}
+
+/// Payment terms: one due date, and the early-payment discount open
+/// before it (rules.md B-39; plan P4b S4.1, A-2, A-8).
+///
+/// ```text
+/// GOAL: terms give one due date and one discount date, exactly.
+/// SOURCE: docs/spec/rules.md B-39; plan/served.md 8.3.13 (B-39);
+///         CONVENTION: standard trade-terms notation; UCC §2-310(a) for
+///         goods; for services, the contract.
+/// INVARIANTS:
+///   1. Net n = date + n; Net n EOM = the last day of date's month + n;
+///      due on receipt = date; Custom = the given date. Every result is
+///      >= the document date and in the calendar (calendar::check); n is
+///      0..=3650.
+///   2. discount_by = date + d, d < the net days; no discount with due on
+///      receipt, EOM or custom terms.
+///   3. describe() is the canonical text; parse() accepts it and the
+///      canonical spellings, case-insensitively, and nothing else.
+/// ```
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub struct Terms {
+    /// How the due date counts.
+    kind: TermsKind,
+    /// The early-payment discount, when there is one.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    discount: Option<EarlyDiscount>,
+    /// The canonical text: "Net 30", "Net 15 EOM", "2/10 net 30", "Due on
+    /// receipt", "Due 2026-11-15".
+    text: String,
+}
+
+impl Terms {
+    /// Terms for `kind`, with `discount` when given, canonical text
+    /// composed. Refused when the days are past [`MAX_TERMS_DAYS`], the
+    /// discount is outside 1..=9,999 basis points, or a discount is asked
+    /// for terms that count no net days (due on receipt, EOM or custom).
+    pub fn new(kind: TermsKind, discount: Option<EarlyDiscount>) -> Result<Self, LedgerError> {
+        if let TermsKind::Net(n) | TermsKind::NetEom(n) = kind
+            && n > MAX_TERMS_DAYS
+        {
+            return Err(LedgerError::TermsUnreadable(format!(
+                "net days {n} is outside 0..={MAX_TERMS_DAYS}"
+            )));
+        }
+        if let Some(d) = discount {
+            if !(1..=9_999).contains(&d.percent_bp) {
+                return Err(LedgerError::TermsUnreadable(format!(
+                    "discount {} basis points is outside 1..=9999",
+                    d.percent_bp
+                )));
+            }
+            match kind {
+                TermsKind::Net(n) if d.days < n => {}
+                _ => return Err(LedgerError::TermsDiscountNeedsNetDays),
+            }
+        }
+        // Custom terms are a date; without one there is nothing to print
+        // or derive (Terms::custom is the way to give it).
+        if kind == TermsKind::Custom {
+            return Err(LedgerError::TermsUnreadable(
+                "custom terms need their date: use Terms::custom".into(),
+            ));
+        }
+        Ok(Terms {
+            kind,
+            discount,
+            text: compose_terms_text(kind, discount),
+        })
+    }
+
+    /// Custom terms due on `due`: the parties agreed a date rather than a
+    /// count of days. Its text carries the date for people; the document
+    /// stores the due date itself.
+    pub fn custom(due: NaiveDate) -> Result<Self, LedgerError> {
+        crate::calendar::check(due)?;
+        Ok(Terms {
+            kind: TermsKind::Custom,
+            discount: None,
+            text: format!("Due {due}"),
+        })
+    }
+
+    /// How the due date counts.
+    pub fn kind(&self) -> TermsKind {
+        self.kind
+    }
+
+    /// The early-payment discount, when there is one.
+    pub fn discount(&self) -> Option<EarlyDiscount> {
+        self.discount
+    }
+
+    /// The canonical text ("Net 30", "2/10 net 30", "Due 2026-11-15").
+    pub fn describe(&self) -> String {
+        self.text.clone()
+    }
+
+    /// The date payment is due for a document dated `date`.
+    ///
+    /// For [`TermsKind::Custom`] the caller passes the agreed date itself
+    /// (there is no count to derive it from); for every other kind `date`
+    /// is the document's date. The result is never before `date` and
+    /// always in the calendar: a due date past 9999-12-31 is refused
+    /// ([`LedgerError::DateOverflow`]), never a panic.
+    pub fn due_date(&self, date: NaiveDate) -> Result<NaiveDate, LedgerError> {
+        crate::calendar::check(date)?;
+        let due = match self.kind {
+            TermsKind::DueOnReceipt | TermsKind::Custom => date,
+            TermsKind::Net(n) => add_days(date, n)?,
+            TermsKind::NetEom(n) => add_days(last_day_of_month(date)?, n)?,
+        };
+        validate_due_date(date, due)?;
+        Ok(due)
+    }
+
+    /// The last date the early-payment discount is open for a document
+    /// dated `date`: `date + discount.days`, or `None` when there is no
+    /// discount or the date is outside the calendar.
+    pub fn discount_by(&self, date: NaiveDate) -> Option<NaiveDate> {
+        let d = self.discount?;
+        let by = date.checked_add_days(Days::new(u64::from(d.days)))?;
+        crate::calendar::check(by).ok()
+    }
+
+    /// Read the canonical spellings, case-insensitively: "Net 30", "Net 15
+    /// EOM", "2/10 net 30", "Due on receipt", "Due 2026-11-15". Anything
+    /// else is [`LedgerError::TermsUnreadable`].
+    pub fn parse(text: &str) -> Result<Self, LedgerError> {
+        let raw = text.trim();
+        let lower = raw.to_lowercase();
+        let unreadable = || LedgerError::TermsUnreadable(raw.to_string());
+        if lower == "due on receipt" {
+            return Terms::new(TermsKind::DueOnReceipt, None);
+        }
+        if let Some(rest) = lower.strip_prefix("due ") {
+            let due =
+                NaiveDate::parse_from_str(rest.trim(), "%Y-%m-%d").map_err(|_| unreadable())?;
+            return Terms::custom(due).map_err(|_| unreadable());
+        }
+        // "2/10 net 30" (an optional decimal percentage), or "net 30" /
+        // "net 15 eom".
+        let (percent, days, net, eom) = match lower.split_once('/') {
+            Some((pct, rest)) => {
+                let (days, net_part) = rest.trim().split_once(' ').ok_or_else(unreadable)?;
+                let after = net_part
+                    .trim()
+                    .strip_prefix("net ")
+                    .ok_or_else(unreadable)?
+                    .trim();
+                let (net, eom) = match after.strip_suffix(" eom") {
+                    Some(n) => (n, true),
+                    None => (after, false),
+                };
+                (
+                    Some(parse_percent(pct).ok_or_else(unreadable)?),
+                    days,
+                    net,
+                    eom,
+                )
+            }
+            None => {
+                let rest = lower.strip_prefix("net ").ok_or_else(unreadable)?;
+                let (net, eom) = match rest.trim().strip_suffix(" eom") {
+                    Some(n) => (n, true),
+                    None => (rest.trim(), false),
+                };
+                (None, "0", net, eom)
+            }
+        };
+        let net: u16 = net.trim().parse().map_err(|_| unreadable())?;
+        let discount = match (percent, days) {
+            (Some(percent_bp), days_raw) => {
+                let days: u16 = days_raw.parse().map_err(|_| unreadable())?;
+                Some(EarlyDiscount { percent_bp, days })
+            }
+            (None, _) => None,
+        };
+        let kind = if eom {
+            TermsKind::NetEom(net)
+        } else {
+            TermsKind::Net(net)
+        };
+        Terms::new(kind, discount).map_err(|_| unreadable())
+    }
+}
+
+/// The canonical text of terms: `"2/10 net 30"` with a discount, else
+/// `"Net 30"`, `"Net 15 EOM"` or `"Due on receipt"`.
+fn compose_terms_text(kind: TermsKind, discount: Option<EarlyDiscount>) -> String {
+    match (discount, kind) {
+        (Some(EarlyDiscount { percent_bp, days }), TermsKind::Net(n)) => {
+            format!("{}/{} net {n}", percent_text(percent_bp), days)
+        }
+        (_, TermsKind::Net(n)) => format!("Net {n}"),
+        (_, TermsKind::NetEom(n)) => format!("Net {n} EOM"),
+        (_, TermsKind::DueOnReceipt) => "Due on receipt".to_string(),
+        (_, TermsKind::Custom) => "Due".to_string(),
+    }
+}
+
+/// Basis points as the percentage trade terms print: 200 is "2", 250 is
+/// "2.5", 205 is "2.05".
+fn percent_text(percent_bp: u32) -> String {
+    let whole = percent_bp / 100;
+    let frac = percent_bp % 100;
+    match (whole, frac) {
+        (w, 0) => w.to_string(),
+        (w, f) if f % 10 == 0 => format!("{w}.{}", f / 10),
+        (w, f) => format!("{w}.{f:02}"),
+    }
+}
+
+/// A percentage in trade terms as basis points: "2" is 200, "2.5" is 250,
+/// "2.05" is 205. None when it isn't a percentage with at most two
+/// decimal places.
+fn parse_percent(s: &str) -> Option<u32> {
+    let (whole, frac) = match s.trim().split_once('.') {
+        Some((w, f)) => (w, f),
+        None => (s.trim(), ""),
+    };
+    if frac.len() > 2 || !frac.chars().all(|c| c.is_ascii_digit()) {
+        return None;
+    }
+    let whole: u32 = whole.parse().ok()?;
+    let frac: u32 = if frac.is_empty() {
+        0
+    } else {
+        format!("{frac:0<2}").parse().ok()?
+    };
+    whole.checked_mul(100)?.checked_add(frac)
+}
+
+/// `date` plus `n` days, or [`LedgerError::DateOverflow`] past the
+/// calendar's end.
+fn add_days(date: NaiveDate, n: u16) -> Result<NaiveDate, LedgerError> {
+    date.checked_add_days(Days::new(u64::from(n)))
+        .ok_or(LedgerError::DateOverflow(date))
+}
+
+/// The last day of `date`'s month, or [`LedgerError::DateOverflow`] when
+/// there is no such date in the calendar.
+fn last_day_of_month(date: NaiveDate) -> Result<NaiveDate, LedgerError> {
+    let (year, month) = if date.month() == 12 {
+        (
+            date.year()
+                .checked_add(1)
+                .ok_or(LedgerError::DateOverflow(date))?,
+            1,
+        )
+    } else {
+        (date.year(), date.month() + 1)
+    };
+    NaiveDate::from_ymd_opt(year, month, 1)
+        .and_then(|first| first.pred_opt())
+        .ok_or(LedgerError::DateOverflow(date))
+}
+
+/// The parties on a document, as they were when it was issued (plan P4b
+/// S4.1, A-13): a name, and the address and email that were on the
+/// document. Never today's party record when a snapshot exists.
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub struct PartySnapshot {
+    /// The party's name at issue.
+    pub name: String,
+    /// Its address at issue, when the document printed one.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub address: Option<String>,
+    /// Its email at issue, when the document printed one.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub email: Option<String>,
+}
+
+/// How an invoice was sent (plan P4b S5; the type S4.1 adds so
+/// [`Invoice::sends`] has one from the start).
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum SentVia {
+    /// Email.
+    Email,
+    /// Paper mail.
+    Mail,
+    /// A customer or vendor portal.
+    Portal,
+    /// Handed over.
+    Hand,
+    /// Another channel, named.
+    Other(String),
+}
+
+/// Whether a send was the original or a reminder (plan P4b S5).
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum SendKind {
+    /// The document first went out.
+    Original,
+    /// It went out again.
+    Reminder,
+}
+
+/// One recorded send of an invoice (plan P4b S5): who sent it, how, to
+/// whom, and the channel's own reference. A send changes no figure.
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub struct Sent {
+    /// The day it went out.
+    pub on: NaiveDate,
+    /// Who sent it: the owner, or a named delegate such as an agent (A-4).
+    pub by: String,
+    /// The channel.
+    pub via: SentVia,
+    /// The recipients.
+    pub to: Vec<String>,
+    /// Original or reminder.
+    pub kind: SendKind,
+    /// The channel's own id (a message id), when there is one.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub reference: Option<String>,
+    /// A note about the send, when there is one.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub note: Option<String>,
+}
+
+/// The fields a new invoice carries beyond its figures (plan P4b S4.1).
+/// Every one is optional: all `None` is the invoice every earlier version
+/// wrote, posted and journaled exactly as before.
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct InvoiceFields {
+    /// The number to issue it under ([`crate::Ledger::next_invoice_number`]).
+    pub number: Option<String>,
+    /// Its payment terms.
+    pub terms: Option<Terms>,
+    /// The customer as the document prints it.
+    pub bill_to: Option<PartySnapshot>,
+    /// Us as the document prints us.
+    pub seller: Option<PartySnapshot>,
+    /// The customer's own reference (their purchase order).
+    pub customer_ref: Option<String>,
+    /// A memo printed on the document.
+    pub memo: Option<String>,
+}
+
+/// The fields a new bill carries beyond its figures (plan P4b S4.1).
+/// Every one is optional: all `None` is the bill every earlier version
+/// wrote, posted and journaled exactly as before.
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct BillFields {
+    /// The vendor's own invoice number.
+    pub vendor_ref: Option<String>,
+    /// The day we received the bill, when it differs from its date.
+    pub received_on: Option<NaiveDate>,
+    /// Its payment terms.
+    pub terms: Option<Terms>,
+    /// A memo about the bill.
+    pub memo: Option<String>,
+    /// Why a vendor invoice number that already names a standing bill is
+    /// entered again anyway. Journaled with the bill (S4.3); never part of
+    /// the record itself.
+    pub duplicate_reason: Option<String>,
+}
+
 /// One line on an invoice or bill.
 #[derive(Clone, Debug, Serialize, Deserialize, PartialEq)]
 pub struct DocumentLine {
@@ -421,6 +826,23 @@ pub struct DocumentLine {
     /// have none.
     #[serde(default, skip_serializing_if = "Option::is_none")]
     pub class_id: Option<crate::ClassId>,
+    /// The account the line's revenue, expense or asset goes to (plan P4b
+    /// S4.1, A-10): an invoice line's revenue or a liability holding no
+    /// role; a bill line's expense or a non-cash asset holding no role.
+    /// None is the kind's role account (revenue for an invoice, general
+    /// expenses for a bill), which is also what every legacy line means.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub account: Option<crate::AccountId>,
+    /// How many units the line bills, when it gives a quantity and price
+    /// rather than one amount. It and `unit_price` are both given or
+    /// neither, and `quantity × unit_price` must equal `amount` exactly
+    /// (plan P4b S4.1).
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub quantity: Option<Decimal>,
+    /// The price of one unit, when the line gives a quantity. See
+    /// [`Self::quantity`].
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub unit_price: Option<Decimal>,
 }
 
 /// A sales invoice: we billed a customer.
@@ -455,6 +877,30 @@ pub struct Invoice {
     pub status: DocumentStatus,
     /// The auto-posted journal entry.
     pub entry_id: u64,
+    /// The number it was issued under ("INV-0007"), from
+    /// [`crate::Ledger::next_invoice_number`]; stored at issue, never
+    /// recomputed, kept by a void (A-2, B-40). None on a legacy invoice:
+    /// it is shown as "Invoice {id}" and never counted.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub number: Option<String>,
+    /// Its payment terms, when it has them.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub terms: Option<Terms>,
+    /// The customer as the document printed it, when it printed one.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub bill_to: Option<PartySnapshot>,
+    /// Us as the document printed us, when it printed us.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub seller: Option<PartySnapshot>,
+    /// The customer's own reference (their purchase order), when given.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub customer_ref: Option<String>,
+    /// A memo printed on the document, when given.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub memo: Option<String>,
+    /// Every recorded send, in order (plan P4b S5; empty until then).
+    #[serde(default, skip_serializing_if = "Vec::is_empty")]
+    pub sends: Vec<Sent>,
 }
 
 /// The sum of a document's lines; refused (TooLargeToCompute), never a
@@ -468,39 +914,51 @@ pub fn document_total(lines: &[DocumentLine], what: &str) -> Result<Decimal, Led
         .ok_or_else(|| LedgerError::TooLargeToCompute(format!("{what}'s total")))
 }
 
-/// The revenue (an invoice's) or expense (a bill's) side of a document's
-/// entry: one part per project the lines name, in the order each first
-/// appears, the untagged lines together as one part (`None`), each the
-/// sum of its lines ([`document_total`]).
+/// The account and project a document's lines group by (plan P4b S4.1):
+/// None for either means the kind's role account (an invoice's revenue, a
+/// bill's general expenses) and no project.
+pub type DocumentPartKey = (Option<crate::AccountId>, Option<crate::ClassId>);
+
+/// The revenue (an invoice's), expense or asset (a bill's) side of a
+/// document's entry: one part per (account, project) the lines name, in
+/// the order each first appears, the lines naming neither together as one
+/// part (`(None, None)`), each the sum of its lines ([`document_total`]).
 ///
 /// ```text
-/// GOAL: a document's lines count toward their projects, and a document
-///       whose lines name none posts exactly as before.
+/// GOAL: a document's lines post to their accounts and count toward their
+///       projects, and a document whose lines name neither posts exactly
+///       as before.
 /// SOURCE: docs/spec/rules.md B-37 item 3 (job costing: the revenue and
 ///         direct costs identified with one job) and item 8 (an
-///         invoice's or bill's line names its project).
+///         invoice's or bill's line names its project); B-39 and plan
+///         P4b S4.1 A-10 (every bill line names its account).
 /// INVARIANTS:
 ///   1. The parts sum to the document's total (conservation), and each
 ///      line is in exactly one part.
-///   2. No two parts name the same project; no part is empty.
-///   3. Lines naming no project make one part, so an untagged document is
-///      one part: the one line every document posted before projects.
+///   2. No two parts name the same account and project; no part is empty.
+///   3. Lines naming neither make one part, so a document with no new
+///      fields is one part: the one line every document posted before
+///      S4.1.
 ///   4. NEVER panics: TooLargeToCompute past exact arithmetic.
 /// ```
 pub fn document_parts(
     lines: &[DocumentLine],
     what: &str,
-) -> Result<Vec<(Option<crate::ClassId>, Decimal)>, LedgerError> {
-    let mut keys: Vec<Option<crate::ClassId>> = Vec::new();
+) -> Result<Vec<(DocumentPartKey, Decimal)>, LedgerError> {
+    let mut keys: Vec<DocumentPartKey> = Vec::new();
     for l in lines {
-        if !keys.contains(&l.class_id) {
-            keys.push(l.class_id);
+        let key = (l.account, l.class_id);
+        if !keys.contains(&key) {
+            keys.push(key);
         }
     }
     keys.into_iter()
         .map(|k| {
-            let part: Vec<DocumentLine> =
-                lines.iter().filter(|l| l.class_id == k).cloned().collect();
+            let part: Vec<DocumentLine> = lines
+                .iter()
+                .filter(|l| (l.account, l.class_id) == k)
+                .cloned()
+                .collect();
             Ok((k, document_total(&part, what)?))
         })
         .collect()
@@ -553,6 +1011,19 @@ pub struct Bill {
     pub status: DocumentStatus,
     /// The auto-posted journal entry.
     pub entry_id: u64,
+    /// The vendor's own invoice number, when given: what a duplicate
+    /// check reads (B-40; [`crate::Ledger::check_vendor_ref`]).
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub vendor_ref: Option<String>,
+    /// The day we received the bill, when it differs from its date.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub received_on: Option<NaiveDate>,
+    /// Its payment terms, when it has them.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub terms: Option<Terms>,
+    /// A memo about the bill, when given.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub memo: Option<String>,
 }
 
 impl Bill {
@@ -571,8 +1042,9 @@ impl Bill {
 }
 
 /// Validate document lines: at least one, all positive amounts, each in a
-/// journal line's range. For new documents; replay restores them as
-/// journaled (rules.md B-28).
+/// journal line's range, and a quantity and unit price that multiply to
+/// the amount exactly (plan P4b S4.1). For new documents; replay restores
+/// them as journaled (rules.md B-28).
 pub fn validate_lines(lines: &[DocumentLine]) -> Result<(), LedgerError> {
     if lines.is_empty() {
         return Err(LedgerError::EmptyDocumentLines);
@@ -589,6 +1061,36 @@ pub fn validate_lines(lines: &[DocumentLine]) -> Result<(), LedgerError> {
                 line.amount
             )));
         }
+        match (line.quantity, line.unit_price) {
+            (None, None) => {}
+            (Some(quantity), Some(unit_price)) => {
+                if quantity <= Decimal::ZERO || unit_price <= Decimal::ZERO {
+                    return Err(LedgerError::LineArithmetic(format!(
+                        "line '{}': quantity {quantity} and unit price {unit_price} must both be positive",
+                        line.description
+                    )));
+                }
+                let product =
+                    crate::kernel::line_amount(quantity, unit_price).ok_or_else(|| {
+                        LedgerError::LineArithmetic(format!(
+                            "line '{}': {quantity} x {unit_price} is too large to compute exactly",
+                            line.description
+                        ))
+                    })?;
+                if product != line.amount {
+                    return Err(LedgerError::LineArithmetic(format!(
+                        "line '{}': {quantity} x {unit_price} = {product}, not the line's amount {}; the engine never rounds a quantity times a price",
+                        line.description, line.amount
+                    )));
+                }
+            }
+            (quantity, unit_price) => {
+                return Err(LedgerError::LineArithmetic(format!(
+                    "line '{}': a quantity and a unit price are both given or neither (quantity {quantity:?}, unit price {unit_price:?})",
+                    line.description
+                )));
+            }
+        }
     }
     Ok(())
 }
@@ -739,6 +1241,9 @@ mod tests {
                     description: "Widgets".to_string(),
                     amount: "1000.00".parse().unwrap(),
                     class_id: None,
+                    account: None,
+                    quantity: None,
+                    unit_price: None,
                 }],
             )
             .unwrap();
@@ -789,6 +1294,9 @@ mod tests {
                     description: "Paper".to_string(),
                     amount: "250.00".parse().unwrap(),
                     class_id: None,
+                    account: None,
+                    quantity: None,
+                    unit_price: None,
                 }],
             )
             .unwrap();
@@ -831,6 +1339,9 @@ mod tests {
                     description: "X".to_string(),
                     amount: "100.00".parse().unwrap(),
                     class_id: None,
+                    account: None,
+                    quantity: None,
+                    unit_price: None,
                 }],
             )
             .unwrap();
@@ -909,6 +1420,9 @@ mod tests {
                 description: "A".to_string(),
                 amount: "100.00".parse().unwrap(),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
@@ -921,6 +1435,9 @@ mod tests {
                 description: "B".to_string(),
                 amount: "200.00".parse().unwrap(),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
@@ -951,6 +1468,9 @@ mod tests {
                 description: "X".to_string(),
                 amount: "100.00".parse().unwrap(),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         );
         assert!(matches!(err, Err(LedgerError::ClosedPeriod(_, _))));
diff --git a/crates/ledger-core/src/error.rs b/crates/ledger-core/src/error.rs
index 2c92cbd..d6eb3be 100644
--- a/crates/ledger-core/src/error.rs
+++ b/crates/ledger-core/src/error.rs
@@ -601,6 +601,67 @@ pub enum LedgerError {
     #[error("document line amount must be positive, got {0}")]
     InvalidDocumentLineAmount(Decimal),
 
+    /// A document line's quantity and unit price don't multiply to its
+    /// amount, or only one of the two is given: the engine never rounds
+    /// one (plan P4b S4.1; rules.md B-39).
+    #[error("{0}")]
+    LineArithmetic(String),
+
+    /// A document line is on an account that kind of document can't post
+    /// to (plan P4b S4.1, A-10; rules.md B-39): a role account, a cash
+    /// account, or a type the document's side doesn't take.
+    #[error("account {code} \"{name}\" cannot take {kind} line: {why}")]
+    DocumentLineAccount {
+        /// The account's code.
+        code: String,
+        /// Its name.
+        name: String,
+        /// "an invoice" or "a bill".
+        kind: &'static str,
+        /// What the rule is, in a sentence.
+        why: String,
+    },
+
+    /// A vendor's invoice number (normalized) already names a standing
+    /// bill of that vendor, and no duplicate reason was given (rules.md
+    /// B-40).
+    #[error(
+        "vendor invoice number '{vendor_ref}' is already on another standing bill of this vendor; \
+         give duplicate_reason when it really is a second bill"
+    )]
+    DuplicateVendorRef {
+        /// The vendor the bill is from.
+        vendor: u64,
+        /// The number as given.
+        vendor_ref: String,
+    },
+
+    /// An invoice number already names an invoice: numbers are never
+    /// reused (rules.md B-40, A-2).
+    #[error("invoice number '{0}' is already used; numbers are never reused")]
+    DuplicateInvoiceNumber(String),
+
+    /// Payment terms could not be read: the message says what to write.
+    #[error(
+        "payment terms '{0}' are not in a form the books read (Net 30, Net 15 EOM, 2/10 net 30, Due on receipt, Due 2026-11-15)"
+    )]
+    TermsUnreadable(String),
+
+    /// An early-payment discount needs net days to be open before: it
+    /// can't be given with due-on-receipt, end-of-month or custom terms
+    /// (rules.md B-39).
+    #[error(
+        "an early-payment discount needs net terms with a fixed number of days; it can't be given with due-on-receipt, end-of-month or custom terms"
+    )]
+    TermsDiscountNeedsNetDays,
+
+    /// A date computed from another (payment terms' due or discount date)
+    /// falls past the calendar the books keep.
+    #[error(
+        "a date computed from {0} is outside the calendar the books keep (0001-01-01 through 9999-12-31)"
+    )]
+    DateOverflow(chrono::NaiveDate),
+
     /// Payment amount must be positive.
     #[error("payment amount must be positive, got {0}")]
     InvalidPaymentAmount(Decimal),
diff --git a/crates/ledger-core/src/kernel.rs b/crates/ledger-core/src/kernel.rs
index 1b352a4..9881b12 100644
--- a/crates/ledger-core/src/kernel.rs
+++ b/crates/ledger-core/src/kernel.rs
@@ -28,6 +28,9 @@
 //! * a payment to a vendor splits, line by line, into what counts toward
 //!   its 1099, what a card or payment network paid, and what is unknown,
 //!   and money moved between the company's own sources nets out (B-19);
+//! * an early-payment discount never exceeds its stated percentage of the
+//!   total, and a document line's amount is exactly its quantity times its
+//!   unit price, neither rounded (B-39);
 //! * an allocation's parts sum to the whole, to the last unit, by largest
 //!   remainder (B-13);
 //! * a cumulative allocation hands out exactly the new amount, and leaves
@@ -71,6 +74,20 @@ pub trait Amount: Copy + Ord {
     /// True when the amount is small and precise enough for a journal line
     /// (see [`MAX_LINE_AMOUNT`] and [`MAX_LINE_SCALE`] for [`Decimal`]).
     fn in_line_range(self) -> bool;
+    /// `n`, exactly, or `None` when it doesn't fit.
+    ///
+    /// A whole count (a percentage in basis points, ten thousand) as the
+    /// arithmetic here needs it; the kernel's other functions get their
+    /// counts as [`crate::kernel::Units`].
+    fn from_u32(n: u32) -> Option<Self>;
+    /// `self * rhs`, or `None` when it cannot be represented exactly.
+    ///
+    /// A quantity times a unit price (a document line, B-39) is the one
+    /// use: it never rounds.
+    fn checked_mul(self, rhs: Self) -> Option<Self>;
+    /// `self / rhs` exactly, or `None` when `rhs` is zero or the quotient
+    /// is not a whole amount of `Self` (never a rounded share).
+    fn checked_div_exact(self, rhs: Self) -> Option<Self>;
 
     /// `self - rhs`, or `None` when it cannot be represented exactly.
     fn checked_sub(self, rhs: Self) -> Option<Self> {
@@ -99,6 +116,43 @@ impl Amount for Decimal {
     fn in_line_range(self) -> bool {
         self.abs() <= MAX_LINE_AMOUNT && self.normalize().scale() <= MAX_LINE_SCALE
     }
+    fn from_u32(n: u32) -> Option<Self> {
+        Some(Decimal::from(n))
+    }
+    fn checked_mul(self, rhs: Self) -> Option<Self> {
+        Decimal::checked_mul(self, rhs)
+    }
+    fn checked_div_exact(self, rhs: Self) -> Option<Self> {
+        let q = self.checked_div(rhs)?;
+        (q.checked_mul(rhs) == Some(self)).then_some(q)
+    }
+}
+
+impl Amount for i32 {
+    const ZERO: Self = 0;
+    fn checked_add(self, rhs: Self) -> Option<Self> {
+        i32::checked_add(self, rhs)
+    }
+    fn checked_neg(self) -> Option<Self> {
+        i32::checked_neg(self)
+    }
+    fn in_line_range(self) -> bool {
+        // The same headroom, scaled down: a proof model, never money.
+        self.unsigned_abs() <= (1 << 20)
+    }
+    fn from_u32(n: u32) -> Option<Self> {
+        i32::try_from(n).ok()
+    }
+    fn checked_mul(self, rhs: Self) -> Option<Self> {
+        i32::checked_mul(self, rhs)
+    }
+    fn checked_div_exact(self, rhs: Self) -> Option<Self> {
+        let r = self.checked_rem(rhs)?;
+        if r != 0 {
+            return None;
+        }
+        self.checked_div(rhs)
+    }
 }
 
 impl Amount for i64 {
@@ -114,6 +168,19 @@ impl Amount for i64 {
         // this size can be summed many times over without overflow.
         self.unsigned_abs() <= (1 << 40)
     }
+    fn from_u32(n: u32) -> Option<Self> {
+        Some(i64::from(n))
+    }
+    fn checked_mul(self, rhs: Self) -> Option<Self> {
+        i64::checked_mul(self, rhs)
+    }
+    fn checked_div_exact(self, rhs: Self) -> Option<Self> {
+        let r = self.checked_rem(rhs)?;
+        if r != 0 {
+            return None;
+        }
+        self.checked_div(rhs)
+    }
 }
 
 /// Why the kernel rejected an entry's lines.
@@ -174,6 +241,50 @@ pub fn net<T: Amount>(lines: impl IntoIterator<Item = (Side, T)>) -> Option<T> {
     Some(total)
 }
 
+/// The most a stated early-payment discount can take from `total`:
+/// `total × percent_bp / 10,000`, exactly. The caller gives the exact
+/// cents it takes; the kernel only bounds them, so it never rounds a
+/// discount up or down (a discount no amount of `Self` can hold is
+/// `None`, not a rounded bound).
+///
+/// ```text
+/// GOAL: an early-payment discount never takes more than its percentage
+///       says, in exact money.
+/// SOURCE: docs/spec/rules.md B-39 INVARIANT 2, B-42; plan/served.md
+///         8.3.13; CHOICE: the gross method, A-8 (the discount is
+///         booked when taken, never estimated).
+/// INVARIANTS:
+///   1. 0 <= result <= total for every total >= 0 and 1 <= percent_bp <=
+///      9,999.
+///   2. result x 10,000 = total x percent_bp exactly: no rounding.
+///   3. None when a factor overflows or the quotient is finer than Self;
+///      NEVER a rounded or wrapped result, never a panic.
+/// ```
+pub fn discount_max<T: Amount>(total: T, percent_bp: u32) -> Option<T> {
+    if total < T::ZERO || percent_bp == 0 || percent_bp > 9_999 {
+        return None;
+    }
+    let bp = T::from_u32(percent_bp)?;
+    let ten_thousand = T::from_u32(10_000)?;
+    total.checked_mul(bp)?.checked_div_exact(ten_thousand)
+}
+
+/// A document line's amount from its quantity and unit price: the exact
+/// product, never rounded.
+///
+/// ```text
+/// GOAL: a line's quantity times its unit price is the amount it posts,
+///       to the last decimal place.
+/// SOURCE: docs/spec/rules.md B-39; plan/served.md 8.3.4 ("kernel::
+///         line_amount(q, u) == amount exactly").
+/// INVARIANTS:
+///   1. Some(p) gives p = quantity x unit_price exactly.
+///   2. None on overflow; never a rounded product, never a panic.
+/// ```
+pub fn line_amount<T: Amount>(quantity: T, unit_price: T) -> Option<T> {
+    quantity.checked_mul(unit_price)
+}
+
 /// Check an entry's lines: two or more, every amount positive and within
 /// line range, debits equal to credits. Accounts and currencies are the
 /// caller's to check; this is the arithmetic.
diff --git a/crates/ledger-core/src/ledger.rs b/crates/ledger-core/src/ledger.rs
index eaf1a68..894ed05 100644
--- a/crates/ledger-core/src/ledger.rs
+++ b/crates/ledger-core/src/ledger.rs
@@ -5270,18 +5270,24 @@ impl Ledger {
         self.add_control_account(c).expect("fresh code cannot fail")
     }
 
-    /// A document's revenue or expense side on its draft `entry`: one line
-    /// on `account` per part ([`arap::document_parts`]), each tagged with
-    /// its project (a project the books don't have: UnknownClass, and the
-    /// caller's `atomically` leaves the books unchanged).
+    /// A document's revenue, expense or asset side on its draft `entry`:
+    /// one line on each part's account, or on `default_account` when the
+    /// part names none ([`arap::document_parts`]), each tagged with its
+    /// project (a project the books don't have: UnknownClass, and the
+    /// caller's `atomically` leaves the books unchanged). Every account is
+    /// checked for the document's kind first
+    /// ([`Self::check_document_line_account`]).
     fn add_document_parts(
         &mut self,
         entry: EntryId,
-        account: AccountId,
+        default_account: AccountId,
         side: Side,
-        parts: &[(Option<ClassId>, Decimal)],
+        kind: arap::DocumentKind,
+        parts: &[(arap::DocumentPartKey, Decimal)],
     ) -> Result<(), LedgerError> {
-        for &(class, amount) in parts {
+        for &((account, class), amount) in parts {
+            let account = account.unwrap_or(default_account);
+            self.check_document_line_account(kind, account)?;
             self.add_line(entry, account, side, Money::new(amount, self.base_currency))?;
             if class.is_some() {
                 let last = self
@@ -5294,20 +5300,119 @@ impl Ledger {
         Ok(())
     }
 
+    /// A document line's account must be one its kind can post to (plan
+    /// P4b S4.1, A-10): an invoice line takes a revenue account, or a
+    /// liability holding no role (2400 Deferred Revenue, a contract
+    /// liability); a bill line takes an expense account, or an asset that
+    /// is not cash and holds no role (1500 Equipment, 1300 Prepaid).
+    /// Placeholders and the receivables and payables control accounts are
+    /// refused. Checked when a line is added and when the entry posts.
+    ///
+    /// ```text
+    /// GOAL: a document's lines go where its kind can put them, never to a
+    ///       control, a cash account or a header.
+    /// SOURCE: docs/spec/rules.md B-39; plan P4b S4.1 ("Line accounts"),
+    ///         A-10 (every bill line names its account);
+    ///         ASC 606-10-45-2 (deferred revenue is a liability).
+    /// INVARIANTS:
+    ///   1. An invoice line: a revenue account, or a liability that holds
+    ///      no role.
+    ///   2. A bill line: an expense account, or an asset that is not cash
+    ///      (`Ledger::account_is_cash`) and holds no role.
+    ///   3. A placeholder, or an account that is a document control
+    ///      (receivables or payables), is refused for both.
+    ///   4. A refusal names the account, the kind and the rule.
+    /// ```
+    pub fn check_document_line_account(
+        &self,
+        kind: arap::DocumentKind,
+        account: AccountId,
+    ) -> Result<(), LedgerError> {
+        self.check_line_account(account)?;
+        let a = self.chart.get(account).expect("checked above");
+        let kind_name = match kind {
+            arap::DocumentKind::Invoice => "an invoice",
+            arap::DocumentKind::Bill => "a bill",
+        };
+        let refuse = |why: &str| {
+            Err(LedgerError::DocumentLineAccount {
+                code: a.code.clone(),
+                name: a.name.clone(),
+                kind: kind_name,
+                why: why.to_string(),
+            })
+        };
+        if self.control_role_of(account).is_some() {
+            return refuse(
+                "it is a receivables or payables control account; its balance is its documents'",
+            );
+        }
+        match kind {
+            arap::DocumentKind::Invoice => match a.account_type {
+                AccountType::Revenue => Ok(()),
+                AccountType::Liability if !self.holds_any_role(account) => Ok(()),
+                _ => refuse(
+                    "an invoice line takes a revenue account, or a liability holding no role (deferred revenue)",
+                ),
+            },
+            arap::DocumentKind::Bill => {
+                if a.account_type == AccountType::Expense {
+                    return Ok(());
+                }
+                if a.account_type == AccountType::Asset
+                    && !self.account_is_cash(account)
+                    && !self.holds_any_role(account)
+                {
+                    return Ok(());
+                }
+                refuse(
+                    "a bill line takes an expense account, or an asset that is not cash and holds no role (equipment, prepaid)",
+                )
+            }
+        }
+    }
+
+    /// Whether `account` is one of the books' cash accounts: the codes in
+    /// `books.cash_accounts` when set, else (as `ledger-store`'s
+    /// reconciliation reads them) the asset accounts whose names say they
+    /// hold cash.
+    fn account_is_cash(&self, account: AccountId) -> bool {
+        let Some(a) = self.chart.get(account) else {
+            return false;
+        };
+        let configured = self.settings.cash_accounts();
+        if !configured.is_empty() {
+            return configured.iter().any(|c| c == &a.code);
+        }
+        const CASH_WORDS: [&str; 5] = ["cash", "bank", "checking", "savings", "money market"];
+        let name = a.name.to_lowercase();
+        a.account_type == AccountType::Asset
+            && !a.placeholder
+            && CASH_WORDS.iter().any(|w| name.contains(w))
+    }
+
+    /// Whether `account` fills any of the books' control roles (assigned,
+    /// or the account at the role's code and type).
+    fn holds_any_role(&self, account: AccountId) -> bool {
+        control_accounts().any(|c| self.holds_role(c, account))
+    }
+
     /// Create a sales invoice. Auto-posts: Dr `1200` Accounts Receivable,
-    /// Cr `4000` Revenue. The invoice date must not fall in a closed period.
+    /// Cr each line's revenue account (the revenue role, `4000`, when a
+    /// line names none). The invoice date must not fall in a closed period.
     ///
     /// ```text
     /// GOAL: bill a customer and recognize the revenue (accrual basis).
     /// SOURCE: IRS Pub. 538, accrual method (docs/spec/sources/irs-periods-and-methods.md:
     ///         "report income in the year it is earned"); ASC 606-10-25-23;
-    ///         control accounts: Ledger::check_controls; rules.md B-38.
+    ///         control accounts: Ledger::check_controls; rules.md B-38, B-39.
     /// INVARIANTS:
-    ///   1. MUST post one balanced entry: Dr 1200 receivables, Cr 4000 revenue,
-    ///      for the sum of the lines, dated the invoice date: one revenue
-    ///      line per project the lines name, the untagged lines' as one
-    ///      (arap::document_parts), each tagged with its project; the
-    ///      receivable line never (rules.md B-37 item 8).
+    ///   1. MUST post one balanced entry: Dr 1200 receivables, Cr the lines'
+    ///      accounts, for the sum of the lines, dated the invoice date: one
+    ///      line per (account, project) part the lines name, the parts
+    ///      naming neither as one (arap::document_parts), each revenue line
+    ///      tagged with its project; the receivable line never (rules.md
+    ///      B-37 item 8).
     ///   2. The receivable line MUST carry the invoice (Origin), in the
     ///      step that posts it: the invoice starts Open, owing its total.
     ///   3. A refusal MUST leave the books unchanged.
@@ -5324,7 +5429,28 @@ impl Ledger {
         due_date: NaiveDate,
         lines: Vec<DocumentLine>,
     ) -> Result<InvoiceId, LedgerError> {
-        self.atomically(|l| l.create_invoice_steps(customer_id, date, due_date, lines))
+        self.create_invoice_with(
+            customer_id,
+            date,
+            due_date,
+            lines,
+            arap::InvoiceFields::default(),
+        )
+    }
+
+    /// [`Self::create_invoice`] with the document's new fields (number,
+    /// terms, snapshots, references: plan P4b S4.1). The fields are stored
+    /// on the invoice at issue and never change. All `None` is exactly
+    /// [`Self::create_invoice`].
+    pub fn create_invoice_with(
+        &mut self,
+        customer_id: CustomerId,
+        date: NaiveDate,
+        due_date: NaiveDate,
+        lines: Vec<DocumentLine>,
+        fields: arap::InvoiceFields,
+    ) -> Result<InvoiceId, LedgerError> {
+        self.atomically(|l| l.create_invoice_steps(customer_id, date, due_date, lines, fields))
     }
 
     /// The steps of [`Self::create_invoice`], run inside [`Self::atomically`].
@@ -5334,12 +5460,21 @@ impl Ledger {
         date: NaiveDate,
         due_date: NaiveDate,
         lines: Vec<DocumentLine>,
+        fields: arap::InvoiceFields,
     ) -> Result<InvoiceId, LedgerError> {
         if !self.customers.contains_key(&customer_id) {
             return Err(LedgerError::UnknownCustomer(customer_id));
         }
         arap::validate_lines(&lines)?;
         arap::validate_due_date(date, due_date)?;
+        if let Some(number) = &fields.number
+            && self
+                .invoices
+                .values()
+                .any(|i| i.number.as_deref() == Some(number.as_str()))
+        {
+            return Err(LedgerError::DuplicateInvoiceNumber(number.clone()));
+        }
         if let Some(pid) = self.closed_period_containing(date) {
             return Err(LedgerError::ClosedPeriod(pid, date.to_string()));
         }
@@ -5360,7 +5495,13 @@ impl Ledger {
                 movement: arap::Movement::Origin,
             },
         )?;
-        self.add_document_parts(entry, revenue, Side::Credit, &parts)?;
+        self.add_document_parts(
+            entry,
+            revenue,
+            Side::Credit,
+            arap::DocumentKind::Invoice,
+            &parts,
+        )?;
         self.post_entry(entry)?;
         self.next_invoice_id += 1;
         self.invoices.insert(
@@ -5375,6 +5516,13 @@ impl Ledger {
                 owed: Decimal::ZERO,
                 status: DocumentStatus::Open,
                 entry_id: entry,
+                number: fields.number,
+                terms: fields.terms,
+                bill_to: fields.bill_to,
+                seller: fields.seller,
+                customer_ref: fields.customer_ref,
+                memo: fields.memo,
+                sends: Vec::new(),
             },
         );
         self.tag_customer(entry, customer_id);
@@ -5382,22 +5530,24 @@ impl Ledger {
         Ok(id)
     }
 
-    /// Create a vendor bill. Auto-posts: Dr `6999` General Expenses,
-    /// Cr `2000` Accounts Payable. The bill date must not fall in a closed
+    /// Create a vendor bill. Auto-posts: Dr each line's expense or asset
+    /// account (general expenses, `6999`, when a line names none), Cr
+    /// `2000` Accounts Payable. The bill date must not fall in a closed
     /// period.
     ///
     /// ```text
-    /// GOAL: record a vendor's bill as an expense owed (accrual basis).
+    /// GOAL: record a vendor's bill as an expense or asset owed (accrual
+    ///       basis).
     /// SOURCE: IRS Pub. 538, accrual method ("deduct ... expenses in the year
     ///         incurred"); control accounts: Ledger::check_controls;
-    ///         rules.md B-38.
+    ///         rules.md B-38, B-39 (plan P4b S4.1, A-10).
     /// INVARIANTS:
-    ///   1. MUST post one balanced entry: Dr 6999 general expenses, Cr 2000
+    ///   1. MUST post one balanced entry: Dr the lines' accounts, Cr 2000
     ///      payables, for the sum of the lines, dated the bill date, tagged
-    ///      with the vendor (1099s): one expense line per project the lines
-    ///      name, the untagged lines' as one (arap::document_parts), each
-    ///      tagged with its project; the payable line never (rules.md B-37
-    ///      item 8).
+    ///      with the vendor (1099s): one line per (account, project) part
+    ///      the lines name, the parts naming neither as one
+    ///      (arap::document_parts), each tagged with its project; the
+    ///      payable line never (rules.md B-37 item 8).
     ///   2. The payable line MUST carry the bill (Origin), in the step that
     ///      posts it.
     ///   3. A refusal MUST leave the books unchanged.
@@ -5413,7 +5563,28 @@ impl Ledger {
         due_date: NaiveDate,
         lines: Vec<DocumentLine>,
     ) -> Result<BillId, LedgerError> {
-        self.atomically(|l| l.create_bill_steps(vendor_id, date, due_date, lines))
+        self.create_bill_with(
+            vendor_id,
+            date,
+            due_date,
+            lines,
+            arap::BillFields::default(),
+        )
+    }
+
+    /// [`Self::create_bill`] with the bill's new fields (the vendor's
+    /// invoice number, terms, receipt date, memo: plan P4b S4.1). The
+    /// fields are stored on the bill at issue and never change. All `None`
+    /// is exactly [`Self::create_bill`].
+    pub fn create_bill_with(
+        &mut self,
+        vendor_id: VendorId,
+        date: NaiveDate,
+        due_date: NaiveDate,
+        lines: Vec<DocumentLine>,
+        fields: arap::BillFields,
+    ) -> Result<BillId, LedgerError> {
+        self.atomically(|l| l.create_bill_steps(vendor_id, date, due_date, lines, fields))
     }
 
     /// The steps of [`Self::create_bill`], run inside [`Self::atomically`].
@@ -5423,12 +5594,19 @@ impl Ledger {
         date: NaiveDate,
         due_date: NaiveDate,
         lines: Vec<DocumentLine>,
+        fields: arap::BillFields,
     ) -> Result<BillId, LedgerError> {
         if !self.vendors.contains_key(&vendor_id) {
             return Err(LedgerError::UnknownVendor(vendor_id));
         }
         arap::validate_lines(&lines)?;
         arap::validate_due_date(date, due_date)?;
+        if let Some(received_on) = fields.received_on {
+            crate::calendar::check(received_on)?;
+        }
+        if let Some(vendor_ref) = fields.vendor_ref.as_deref() {
+            self.check_vendor_ref(vendor_id, vendor_ref, fields.duplicate_reason.as_deref())?;
+        }
         if let Some(pid) = self.closed_period_containing(date) {
             return Err(LedgerError::ClosedPeriod(pid, date.to_string()));
         }
@@ -5439,7 +5617,13 @@ impl Ledger {
         let ap = self.ensure_control(&PAYABLES);
         let id = self.next_bill_id;
         let entry = self.create_entry(date, &format!("Bill {id}"));
-        self.add_document_parts(entry, expense, Side::Debit, &parts)?;
+        self.add_document_parts(
+            entry,
+            expense,
+            Side::Debit,
+            arap::DocumentKind::Bill,
+            &parts,
+        )?;
         self.add_tagged_line(
             entry,
             ap,
@@ -5464,6 +5648,10 @@ impl Ledger {
                 owed: Decimal::ZERO,
                 status: DocumentStatus::Open,
                 entry_id: entry,
+                vendor_ref: fields.vendor_ref,
+                received_on: fields.received_on,
+                terms: fields.terms,
+                memo: fields.memo,
             },
         );
         self.tag_vendor(entry, vendor_id);
@@ -5471,6 +5659,54 @@ impl Ledger {
         Ok(id)
     }
 
+    /// The number the next invoice is issued under (A-2, B-40): `prefix`,
+    /// then `first_number` plus the count of numbered invoices issued so
+    /// far, zero-padded to four digits and wider past 9,999 (never
+    /// truncated). Stored at issue, never recomputed; a void keeps its
+    /// number, so the series never reuses one; a legacy invoice
+    /// (`number: None`) is not counted.
+    pub fn next_invoice_number(&self, prefix: &str, first_number: u64) -> String {
+        let issued = self
+            .invoices
+            .values()
+            .filter(|i| i.number.is_some())
+            .count() as u64;
+        format!("{prefix}{:04}", first_number.saturating_add(issued))
+    }
+
+    /// Refuse a vendor invoice number that already names a standing bill
+    /// of the same vendor (B-40), unless `duplicate_reason` says why it is
+    /// entered again. Case, spaces and hyphens are ignored: "ACME-123",
+    /// "acme 123" and "Acme123" are the same number.
+    pub fn check_vendor_ref(
+        &self,
+        vendor: VendorId,
+        vendor_ref: &str,
+        duplicate_reason: Option<&str>,
+    ) -> Result<(), LedgerError> {
+        if duplicate_reason.is_some_and(|r| !r.trim().is_empty()) {
+            return Ok(());
+        }
+        let key = normalize_vendor_ref(vendor_ref);
+        if key.is_empty() {
+            return Ok(());
+        }
+        for bill in self.bills.values() {
+            if bill.vendor_id != vendor || !self.in_effect(bill.entry_id) {
+                continue;
+            }
+            if let Some(existing) = &bill.vendor_ref
+                && normalize_vendor_ref(existing) == key
+            {
+                return Err(LedgerError::DuplicateVendorRef {
+                    vendor,
+                    vendor_ref: vendor_ref.to_string(),
+                });
+            }
+        }
+        Ok(())
+    }
+
     /// Look up an invoice.
     pub fn get_invoice(&self, id: InvoiceId) -> Option<&Invoice> {
         self.invoices.get(&id)
@@ -6395,6 +6631,13 @@ impl Ledger {
                 owed: Decimal::ZERO,
                 status: DocumentStatus::Open,
                 entry_id,
+                number: None,
+                terms: None,
+                bill_to: None,
+                seller: None,
+                customer_ref: None,
+                memo: None,
+                sends: Vec::new(),
             },
         );
         self.tag_customer(entry_id, customer_id);
@@ -6443,6 +6686,10 @@ impl Ledger {
                 owed: Decimal::ZERO,
                 status: DocumentStatus::Open,
                 entry_id,
+                vendor_ref: None,
+                received_on: None,
+                terms: None,
+                memo: None,
             },
         );
         self.tag_vendor(entry_id, vendor_id);
@@ -7933,6 +8180,17 @@ fn same_member_set(a: &[(AccountId, Decimal)], b: &[(AccountId, Decimal)]) -> bo
     a.len() == b.len() && sorted(a) == sorted(b)
 }
 
+/// A vendor invoice number as the duplicate check compares it: lower case,
+/// with spaces and hyphens removed ("ACME-123" and "acme 123" are the
+/// same number; rules.md B-40).
+fn normalize_vendor_ref(vendor_ref: &str) -> String {
+    vendor_ref
+        .chars()
+        .filter(|c| !c.is_whitespace() && *c != '-')
+        .flat_map(char::to_lowercase)
+        .collect()
+}
+
 /// A members regime ([`Ledger::members_regime`]): the members closes with
 /// one set of members and shares since the last close with another.
 #[derive(Clone, Debug, PartialEq)]
diff --git a/crates/ledger-core/src/lib.rs b/crates/ledger-core/src/lib.rs
index 4058909..a52639e 100644
--- a/crates/ledger-core/src/lib.rs
+++ b/crates/ledger-core/src/lib.rs
@@ -48,9 +48,10 @@ pub mod tax_capital;
 
 pub use account::{Account, AccountId, AccountType, ChartOfAccounts, Side};
 pub use arap::{
-    AgingRow, Bill, BillId, ControlCheck, Customer, CustomerId, DocLine, DocRef, DocState,
-    DocStatus, DocTag, DocumentLine, DocumentStatus, Invoice, InvoiceId, Movement, PaymentDetails,
-    UnattachedLine, Vendor, VendorId,
+    AgingRow, Bill, BillFields, BillId, ControlCheck, Customer, CustomerId, DocLine, DocRef,
+    DocState, DocStatus, DocTag, DocumentKind, DocumentLine, DocumentPartKey, DocumentStatus,
+    EarlyDiscount, Invoice, InvoiceFields, InvoiceId, Movement, PartySnapshot, PaymentDetails,
+    SendKind, Sent, SentVia, Terms, TermsKind, UnattachedLine, Vendor, VendorId,
 };
 pub use assets::{
     Asset, AssetBasis, AssetCorrection, AssetId, AssetStatus, BasisRule, DepreciationMethod,
diff --git a/crates/ledger-core/src/proofs.rs b/crates/ledger-core/src/proofs.rs
index fa0cd53..b7929f2 100644
--- a/crates/ledger-core/src/proofs.rs
+++ b/crates/ledger-core/src/proofs.rs
@@ -1892,6 +1892,65 @@ fn bounds_kept_is_the_definition_on_books_in_bounds() {
     );
 }
 
+// ---------------------------------------------------------------------------
+// Terms and document lines (P4b S4.1)
+// ---------------------------------------------------------------------------
+
+/// `kernel::discount_max` never bounds a discount above the total, and what
+/// it gives is exact: result x 10,000 = total x basis points. None is an
+/// exact bound no whole cent can hold, not a rounded one.
+///
+/// At `i32`, like the proration charge harnesses: the law relates a
+/// product to a quotient, which the model checker proves far faster on
+/// 32-bit arithmetic; the bridge property carries it to `Decimal`.
+#[kani::proof]
+fn discount_max_is_bounded() {
+    let total: i32 = kani::any();
+    kani::assume(total >= 0 && total <= 200_000);
+    // A u16 stands for the percentage: any 1..=9,999 basis points, and a
+    // narrower divisor keeps the model checker quick (the kernel takes
+    // u32; the bridge checks that boundary).
+    let percent_bp: u16 = kani::any();
+    kani::assume(percent_bp >= 1 && percent_bp <= 9_999);
+    let got = kernel::discount_max(total, u32::from(percent_bp));
+    if let Some(discount) = got {
+        assert!(discount >= 0);
+        assert!(discount <= total);
+        assert_eq!(
+            discount.checked_mul(10_000),
+            total.checked_mul(i32::from(percent_bp))
+        );
+    }
+    kani::cover!(
+        got.is_some_and(|d| d > 0),
+        "a discount that takes something"
+    );
+    kani::cover!(got.is_none(), "an exact bound finer than a whole cent");
+}
+
+/// `kernel::line_amount` is the exact product of a quantity and a unit
+/// price: never a rounded amount, and None rather than an overflow.
+#[kani::proof]
+fn line_amount_is_exact() {
+    let quantity: i64 = kani::any();
+    let unit_price: i64 = kani::any();
+    kani::assume(quantity >= 0 && quantity <= 1_000_000);
+    kani::assume(unit_price >= 0 && unit_price <= 1_000_000);
+    let got = kernel::line_amount(quantity, unit_price);
+    assert_eq!(got, quantity.checked_mul(unit_price));
+    if let Some(amount) = got {
+        assert!(amount >= 0);
+        if quantity > 0 && unit_price > 0 {
+            assert!(amount >= quantity);
+            assert!(amount >= unit_price);
+        }
+    }
+    kani::cover!(
+        got.is_some_and(|a| a > 1) && quantity > 1 && unit_price > 1,
+        "a product both factors grow"
+    );
+}
+
 // ---------------------------------------------------------------------------
 // The checker itself
 // ---------------------------------------------------------------------------
diff --git a/crates/ledger-core/tests/bookspec.rs b/crates/ledger-core/tests/bookspec.rs
index 48a7155..d1d0f48 100644
--- a/crates/ledger-core/tests/bookspec.rs
+++ b/crates/ledger-core/tests/bookspec.rs
@@ -982,6 +982,9 @@ impl<'a> Books<'a> {
                 description: description.to_string(),
                 amount: positive(a),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
             (None, [_, ..]) => lines
                 .iter()
@@ -993,6 +996,9 @@ impl<'a> Books<'a> {
                             panic!("{what}: project {p:?} not in setup.projects")
                         })
                     }),
+                    account: None,
+                    quantity: None,
+                    unit_price: None,
                 })
                 .collect(),
             _ => panic!("{what}: a document has an amount or lines, exactly one"),
diff --git a/crates/ledger-core/tests/form1099.rs b/crates/ledger-core/tests/form1099.rs
index e4bbbf8..78e348e 100644
--- a/crates/ledger-core/tests/form1099.rs
+++ b/crates/ledger-core/tests/form1099.rs
@@ -161,6 +161,9 @@ fn books() -> Ledger {
                 description: "Design work".into(),
                 amount: dec("1500"),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
diff --git a/crates/ledger-core/tests/invariants.rs b/crates/ledger-core/tests/invariants.rs
index 5ecb581..09a078e 100644
--- a/crates/ledger-core/tests/invariants.rs
+++ b/crates/ledger-core/tests/invariants.rs
@@ -990,6 +990,9 @@ fn doc(amount: u64) -> Vec<ledger_core::DocumentLine> {
         description: "work".into(),
         amount: Decimal::from(amount),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }]
 }
 
diff --git a/crates/ledger-core/tests/kernel_bridge.rs b/crates/ledger-core/tests/kernel_bridge.rs
index c9da630..0f0c14a 100644
--- a/crates/ledger-core/tests/kernel_bridge.rs
+++ b/crates/ledger-core/tests/kernel_bridge.rs
@@ -484,4 +484,53 @@ proptest! {
             prop_assert_eq!(i.built_in_gain_704c.map(dec), d.built_in_gain_704c);
         }
     }
+
+    /// kernel::discount_max at i64 (what Kani's discount_max_is_bounded
+    /// proved) and at Decimal agree where both are exact: the bound is
+    /// the same money, never above the total, and result x 10,000 =
+    /// total x basis points on both.
+    #[test]
+    fn discount_max_agrees(
+        total in 0..=MAX_CENTS,
+        percent_bp in 1u32..=9_999,
+    ) {
+        let narrow = kernel::discount_max(total, percent_bp);
+        let wide = kernel::discount_max(dec(total), percent_bp)
+            .expect("a decimal division by 10,000 is exact");
+        if let Some(n) = narrow {
+            prop_assert_eq!(wide, dec(n));
+        }
+        prop_assert!(wide >= Decimal::ZERO);
+        prop_assert!(wide <= dec(total));
+        prop_assert_eq!(
+            wide * Decimal::from(10_000u32),
+            dec(total) * Decimal::from(percent_bp)
+        );
+    }
+
+    /// The discount bound Kani proves at i32 (small totals) is the same
+    /// bound at i64, which the property above carries to Decimal.
+    #[test]
+    fn discount_max_i32_agrees_with_i64(
+        total in 0i32..=200_000,
+        percent_bp in 1u32..=9_999,
+    ) {
+        prop_assert_eq!(
+            kernel::discount_max(total, percent_bp).map(i64::from),
+            kernel::discount_max(i64::from(total), percent_bp)
+        );
+    }
+
+    /// kernel::line_amount at i64 (what Kani's line_amount_is_exact
+    /// proved) and at Decimal agree: cents x cents at i64 is the same
+    /// product as dollars x dollars at Decimal, to four places.
+    #[test]
+    fn line_amount_agrees(
+        quantity in 0..=1_000_000i64,
+        unit_price in 0..=1_000_000i64,
+    ) {
+        let narrow = kernel::line_amount(quantity, unit_price);
+        let wide = kernel::line_amount(dec(quantity), dec(unit_price));
+        prop_assert_eq!(narrow.map(|n| Decimal::new(n, 4)), wide);
+    }
 }
diff --git a/crates/ledger-core/tests/spec_arap.rs b/crates/ledger-core/tests/spec_arap.rs
index bd00892..c38fdde 100644
--- a/crates/ledger-core/tests/spec_arap.rs
+++ b/crates/ledger-core/tests/spec_arap.rs
@@ -37,6 +37,9 @@ fn line(desc: &str, amount: &str) -> DocumentLine {
         description: desc.to_string(),
         amount: dec(amount),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }
 }
 
@@ -187,6 +190,13 @@ fn invoice_total_is_sum_of_lines_and_balance_is_what_is_owed() {
         owed: dec("90.00"),
         status: DocumentStatus::Partial,
         entry_id: 1,
+        number: None,
+        terms: None,
+        bill_to: None,
+        seller: None,
+        customer_ref: None,
+        memo: None,
+        sends: Vec::new(),
     };
     assert_eq!(inv.total().unwrap(), dec("150.00"));
     assert_eq!(inv.balance().unwrap(), dec("90.00"));
@@ -205,6 +215,10 @@ fn bill_total_is_sum_of_lines_and_balance_is_what_is_owed() {
         owed: Decimal::ZERO,
         status: DocumentStatus::Paid,
         entry_id: 9,
+        vendor_ref: None,
+        received_on: None,
+        terms: None,
+        memo: None,
     };
     assert_eq!(bill.total().unwrap(), dec("20.00"));
     assert_eq!(bill.balance().unwrap(), Decimal::ZERO);
@@ -384,7 +398,14 @@ proptest! {
     ) {
         let lines: Vec<DocumentLine> = amts
             .iter()
-            .map(|c| DocumentLine { description: "l".into(), amount: cents(*c), class_id: None })
+            .map(|c| DocumentLine {
+                description: "l".into(),
+                amount: cents(*c),
+                class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
+            })
             .collect();
         let ok = !amts.is_empty() && amts.iter().all(|c| *c > 0);
         prop_assert_eq!(validate_lines(&lines).is_ok(), ok);
@@ -1088,6 +1109,9 @@ fn doc_lines(doc: &Doc) -> Vec<DocumentLine> {
             description: "item".into(),
             amount: cents(*c),
             class_id: None,
+            account: None,
+            quantity: None,
+            unit_price: None,
         })
         .collect()
 }
diff --git a/crates/ledger-core/tests/spec_bounds.rs b/crates/ledger-core/tests/spec_bounds.rs
index 6d9d7a8..88ae63d 100644
--- a/crates/ledger-core/tests/spec_bounds.rs
+++ b/crates/ledger-core/tests/spec_bounds.rs
@@ -142,6 +142,9 @@ fn dates_outside_the_calendar_are_refused_everywhere() {
         description: "work".into(),
         amount: Decimal::ONE,
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }];
     assert_eq!(
         b.ledger
@@ -221,6 +224,9 @@ fn replayed_dates_outside_the_calendar_are_accepted() {
         description: "work".into(),
         amount: Decimal::ONE,
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }];
     b.ledger
         .replay_invoice(1, customer, NaiveDate::MIN, NaiveDate::MAX, line.clone(), 1)
@@ -329,11 +335,17 @@ fn amounts_larger_than_a_line_are_refused_everywhere() {
                 description: "a".into(),
                 amount: a,
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             },
             DocumentLine {
                 description: "b".into(),
                 amount: Decimal::ONE,
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             },
         ]
     };
@@ -623,6 +635,9 @@ fn replayed_payments_are_as_journaled() {
                 description: "work".into(),
                 amount: Decimal::new(10000, 2),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
diff --git a/crates/ledger-core/tests/spec_cash_flow.rs b/crates/ledger-core/tests/spec_cash_flow.rs
index eea05d0..57890e5 100644
--- a/crates/ledger-core/tests/spec_cash_flow.rs
+++ b/crates/ledger-core/tests/spec_cash_flow.rs
@@ -2092,6 +2092,9 @@ fn a_bill_payment_carries_its_bills_split() {
             description: "Equipment and supplies".into(),
             amount: x("1700.00"),
             class_id: None,
+            account: None,
+            quantity: None,
+            unit_price: None,
         }],
         entry,
     )
@@ -2517,6 +2520,9 @@ fn a_reversed_bill_payment_leaves_the_purchase_unpaid() {
             description: "Equipment".into(),
             amount: x("1000.00"),
             class_id: None,
+            account: None,
+            quantity: None,
+            unit_price: None,
         }],
         entry,
     )
diff --git a/crates/ledger-core/tests/spec_document_projects.rs b/crates/ledger-core/tests/spec_document_projects.rs
index 17acaa1..3a8402b 100644
--- a/crates/ledger-core/tests/spec_document_projects.rs
+++ b/crates/ledger-core/tests/spec_document_projects.rs
@@ -17,8 +17,8 @@ use ledger_core::form1099::{PaymentAccounts, vendor_1099_report};
 use ledger_core::parties::{MoneyAccounts, activity};
 use ledger_core::reports::profit_and_loss_by_class;
 use ledger_core::{
-    AccountType, ClassId, Currency, Ledger, LedgerError, ProjectFacts, ProjectStatus, Side,
-    project_entries, project_to_date,
+    AccountId, AccountType, ClassId, Currency, Ledger, LedgerError, ProjectFacts, ProjectStatus,
+    Side, project_entries, project_to_date,
 };
 use proptest::prelude::*;
 use rust_decimal::Decimal;
@@ -36,6 +36,9 @@ fn line(what: &str, c: i64, class: Option<ClassId>) -> DocumentLine {
         description: what.into(),
         amount: cents(c),
         class_id: class,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }
 }
 
@@ -436,20 +439,25 @@ proptest! {
         let parts = document_parts(&lines, "doc").unwrap();
         let total: Decimal = lines.iter().map(|l| l.amount).sum();
         prop_assert_eq!(parts.iter().map(|p| p.1).sum::<Decimal>(), total);
-        let mut first: Vec<Option<ClassId>> = Vec::new();
+        let mut first: Vec<(Option<AccountId>, Option<ClassId>)> = Vec::new();
         for l in &lines {
-            if !first.contains(&l.class_id) {
-                first.push(l.class_id);
+            let key = (l.account, l.class_id);
+            if !first.contains(&key) {
+                first.push(key);
             }
         }
         prop_assert_eq!(parts.iter().map(|p| p.0).collect::<Vec<_>>(), first);
-        for (k, amount) in &parts {
-            let sum: Decimal = lines.iter().filter(|l| l.class_id == *k).map(|l| l.amount).sum();
+        for ((account, class), amount) in &parts {
+            let sum: Decimal = lines
+                .iter()
+                .filter(|l| l.account == *account && l.class_id == *class)
+                .map(|l| l.amount)
+                .sum();
             prop_assert_eq!(*amount, sum);
             prop_assert!(*amount > Decimal::ZERO);
         }
-        if lines.iter().all(|l| l.class_id.is_none()) {
-            prop_assert_eq!(parts, vec![(None, total)]);
+        if lines.iter().all(|l| l.class_id.is_none() && l.account.is_none()) {
+            prop_assert_eq!(parts, vec![((None, None), total)]);
         }
     }
 }
@@ -462,6 +470,9 @@ fn document_parts_refuse_past_exact_arithmetic() {
         description: "x".into(),
         amount: Decimal::MAX,
         class_id: Some(1),
+        account: None,
+        quantity: None,
+        unit_price: None,
     };
     assert!(matches!(
         document_parts(&[big.clone(), big], "doc"),
diff --git a/crates/ledger-core/tests/spec_documents.rs b/crates/ledger-core/tests/spec_documents.rs
index e9fc79c..1e02949 100644
--- a/crates/ledger-core/tests/spec_documents.rs
+++ b/crates/ledger-core/tests/spec_documents.rs
@@ -11,7 +11,9 @@
 //! ```
 
 use chrono::NaiveDate;
-use ledger_core::arap::DocumentLine;
+use ledger_core::arap::{
+    BillFields, DocumentKind, DocumentLine, EarlyDiscount, InvoiceFields, Terms, TermsKind,
+};
 use ledger_core::{
     AccountId, AccountType, Currency, DocRef, DocStatus, Ledger, LedgerError, Money, Movement,
     PaymentDetails, Side,
@@ -36,6 +38,9 @@ fn line(what: &str, c: i64) -> Vec<DocumentLine> {
         description: what.into(),
         amount: cents(c),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }]
 }
 
@@ -1402,3 +1407,518 @@ proptest! {
         }
     }
 }
+
+// ---------------------------------------------------------------------------
+// S4.1: terms, numbers, line accounts, quantity and price
+// ---------------------------------------------------------------------------
+
+/// A document line naming its account and, when `qty` and `price` are
+/// given, its quantity and unit price (plan P4b S4.1).
+fn doc_line(
+    what: &str,
+    c: i64,
+    account: Option<AccountId>,
+    qty: Option<i64>,
+    price: Option<i64>,
+) -> DocumentLine {
+    let quantity = qty.map(Decimal::from);
+    let unit_price = price.map(cents);
+    let amount = match (quantity, unit_price) {
+        (Some(q), Some(p)) => q * p,
+        _ => cents(c),
+    };
+    DocumentLine {
+        description: what.into(),
+        amount,
+        class_id: None,
+        account,
+        quantity,
+        unit_price,
+    }
+}
+
+/// B-39 SCENARIOS: Net 30, Net 15 EOM, a leap day, due on receipt, a
+/// custom date, and the 9999-12 bound refused instead of panicking.
+#[test]
+fn terms_derive_due_dates() {
+    let net30 = Terms::new(TermsKind::Net(30), None).unwrap();
+    assert_eq!(net30.due_date(d(2026, 1, 31)).unwrap(), d(2026, 3, 2));
+    assert_eq!(net30.describe(), "Net 30");
+
+    let eom15 = Terms::new(TermsKind::NetEom(15), None).unwrap();
+    assert_eq!(eom15.due_date(d(2026, 10, 23)).unwrap(), d(2026, 11, 15));
+    assert_eq!(eom15.describe(), "Net 15 EOM");
+
+    let net28 = Terms::new(TermsKind::Net(28), None).unwrap();
+    assert_eq!(net28.due_date(d(2028, 2, 1)).unwrap(), d(2028, 2, 29));
+    let net0 = Terms::new(TermsKind::Net(0), None).unwrap();
+    assert_eq!(net0.due_date(d(2026, 5, 4)).unwrap(), d(2026, 5, 4));
+
+    let on_receipt = Terms::new(TermsKind::DueOnReceipt, None).unwrap();
+    assert_eq!(on_receipt.due_date(d(2026, 7, 4)).unwrap(), d(2026, 7, 4));
+
+    let custom = Terms::custom(d(2026, 11, 15)).unwrap();
+    assert_eq!(custom.describe(), "Due 2026-11-15");
+    assert_eq!(custom.due_date(d(2026, 11, 15)).unwrap(), d(2026, 11, 15));
+
+    // The calendar's end: refused, not a panic.
+    let last_day = Terms::new(TermsKind::Net(1), None).unwrap();
+    assert!(last_day.due_date(d(9999, 12, 31)).is_err());
+    let last_month = Terms::new(TermsKind::NetEom(1), None).unwrap();
+    assert!(last_month.due_date(d(9999, 12, 1)).is_err());
+    // Ten years is the most a term may run.
+    assert!(Terms::new(TermsKind::Net(3_651), None).is_err());
+    assert!(Terms::new(TermsKind::NetEom(3_651), None).is_err());
+}
+
+/// B-39 INVARIANT 2: the discount's bound, its date, and the terms that
+/// cannot carry one.
+#[test]
+fn discount_bounds_and_late_reason() {
+    let discount = EarlyDiscount {
+        percent_bp: 200,
+        days: 10,
+    };
+    let net30 = Terms::new(TermsKind::Net(30), Some(discount)).unwrap();
+    assert_eq!(net30.describe(), "2/10 net 30");
+    assert_eq!(net30.discount_by(d(2026, 1, 10)), Some(d(2026, 1, 20)));
+    // The discount window closes after its last day: the discount is the
+    // bound, and a payment after it has no discount to take without a
+    // reason (the payment path's check, S6).
+    assert!(net30.discount_by(d(2026, 1, 10)).unwrap() < net30.due_date(d(2026, 1, 10)).unwrap());
+
+    // Due on receipt and EOM terms have no net days to discount before.
+    assert_eq!(
+        Terms::new(TermsKind::DueOnReceipt, Some(discount)),
+        Err(LedgerError::TermsDiscountNeedsNetDays)
+    );
+    assert_eq!(
+        Terms::new(TermsKind::NetEom(30), Some(discount)),
+        Err(LedgerError::TermsDiscountNeedsNetDays)
+    );
+    // The discount must close before the net days run out.
+    assert_eq!(
+        Terms::new(
+            TermsKind::Net(10),
+            Some(EarlyDiscount {
+                percent_bp: 200,
+                days: 10
+            })
+        ),
+        Err(LedgerError::TermsDiscountNeedsNetDays)
+    );
+    // A percentage outside 0.01%..99.99% is not a discount.
+    assert!(
+        Terms::new(
+            TermsKind::Net(30),
+            Some(EarlyDiscount {
+                percent_bp: 0,
+                days: 10
+            })
+        )
+        .is_err()
+    );
+    assert!(
+        Terms::new(
+            TermsKind::Net(30),
+            Some(EarlyDiscount {
+                percent_bp: 10_000,
+                days: 10
+            })
+        )
+        .is_err()
+    );
+
+    // The kernel bounds the exact cents: 2% of 100.00 is 2.00, and 2% of
+    // 100.01 is 2.0002, never a rounded 2.00.
+    use ledger_core::kernel;
+    assert_eq!(kernel::discount_max(cents(10_000), 200), Some(cents(200)));
+    assert_eq!(
+        kernel::discount_max(cents(10_001), 200),
+        Some(Decimal::new(20_002, 4))
+    );
+    assert_eq!(kernel::discount_max(cents(10_000), 0), None);
+    assert_eq!(kernel::discount_max(cents(-1), 200), None);
+}
+
+/// B-39 INVARIANT 3: the canonical spellings read back as they print.
+#[test]
+fn terms_describe_and_parse_round_trip() {
+    for text in [
+        "Net 30",
+        "Net 15 EOM",
+        "2/10 net 30",
+        "Due on receipt",
+        "Due 2026-11-15",
+    ] {
+        let terms = Terms::parse(text).unwrap();
+        assert_eq!(terms.describe(), text, "parsing {text}");
+        assert_eq!(Terms::parse(&terms.describe()).unwrap(), terms);
+    }
+    // Case does not matter; the text printed is the canonical spelling.
+    assert_eq!(Terms::parse("net 30").unwrap().describe(), "Net 30");
+    assert_eq!(
+        Terms::parse("2/10 NET 30").unwrap().describe(),
+        "2/10 net 30"
+    );
+    assert_eq!(
+        Terms::parse("2.5/10 net 30").unwrap().describe(),
+        "2.5/10 net 30"
+    );
+    // Anything else is refused, never guessed.
+    for bad in [
+        "net thirty",
+        "net 30 days",
+        "2/10 net 5",
+        "Due 2026-13-01",
+        "2/10",
+        "",
+    ] {
+        assert!(
+            matches!(Terms::parse(bad), Err(LedgerError::TermsUnreadable(_))),
+            "{bad:?} was read as {:?}",
+            Terms::parse(bad)
+        );
+    }
+}
+
+/// A bill's lines post to the accounts they name, one line per (account,
+/// project) part (plan P4b S4.1, 8.3.6 "Record bill").
+#[test]
+fn bill_lines_post_to_their_accounts() {
+    let mut b = books();
+    let equipment =
+        b.l.add_account("1500", "Equipment", AccountType::Asset, None, false)
+            .unwrap();
+    let supplies =
+        b.l.add_account("6100", "Supplies", AccountType::Expense, None, false)
+            .unwrap();
+    let bill =
+        b.l.create_bill(
+            b.vendor,
+            d(2026, 3, 1),
+            d(2026, 3, 31),
+            vec![
+                doc_line("Chair", 30_000, Some(equipment), None, None),
+                doc_line("Paper", 5_000, Some(supplies), None, None),
+                doc_line("Ink", 1_000, Some(supplies), None, None),
+            ],
+        )
+        .unwrap();
+    assert_eq!(b.account("1500"), equipment);
+    assert_eq!(b.l.account_balance(equipment).unwrap(), cents(30_000));
+    assert_eq!(b.l.account_balance(supplies).unwrap(), cents(6_000));
+    let ap = b.account("2000");
+    assert_eq!(b.l.account_balance(ap).unwrap(), cents(36_000));
+    // The legacy default account takes nothing when every line names one.
+    assert_eq!(
+        b.l.account_balance(b.account("6999")).unwrap(),
+        Decimal::ZERO
+    );
+    // Three lines: one per (account, project) part (equipment, supplies
+    // for Paper and Ink together) and one payable line.
+    assert_eq!(
+        b.l.get_entry(b.l.get_bill(bill).unwrap().entry_id)
+            .unwrap()
+            .lines()
+            .len(),
+        3
+    );
+    b.ties(d(2026, 3, 31));
+}
+
+/// An invoice line billed ahead of the work goes to 2400 Deferred Revenue,
+/// a contract liability (ASC 606-10-45-2; A-10's invoice rule).
+#[test]
+fn invoice_line_to_deferred_revenue_posts_to_2400() {
+    let mut b = books();
+    let deferred =
+        b.l.add_account(
+            "2400",
+            "Deferred Revenue",
+            AccountType::Liability,
+            None,
+            false,
+        )
+        .unwrap();
+    let inv =
+        b.l.create_invoice(
+            b.customer,
+            d(2026, 4, 1),
+            d(2026, 5, 1),
+            vec![doc_line("Retainer", 50_000, Some(deferred), None, None)],
+        )
+        .unwrap();
+    assert_eq!(b.l.account_balance(deferred).unwrap(), cents(50_000));
+    let revenue = b.account("4000");
+    assert_eq!(b.l.account_balance(revenue).unwrap(), Decimal::ZERO);
+    assert_eq!(b.l.get_invoice(inv).unwrap().total(), Ok(cents(50_000)));
+    b.ties(d(2026, 5, 1));
+}
+
+/// A line's amount is exactly its quantity times its unit price; the
+/// engine never rounds one (plan P4b S4.1; kernel::line_amount).
+#[test]
+fn qty_times_price_must_equal_amount() {
+    let mut b = books();
+    let inv =
+        b.l.create_invoice(
+            b.customer,
+            d(2026, 5, 1),
+            d(2026, 5, 31),
+            vec![doc_line("Hours", 0, None, Some(3), Some(3_333))],
+        )
+        .unwrap();
+    assert_eq!(b.l.get_invoice(inv).unwrap().total(), Ok(cents(9_999)));
+
+    // 3 x 33.33 is 99.99, not 100.00: refused, and nothing is posted.
+    let bad = vec![DocumentLine {
+        description: "Hours".into(),
+        amount: cents(10_000),
+        class_id: None,
+        account: None,
+        quantity: Some(Decimal::from(3)),
+        unit_price: Some(cents(3_333)),
+    }];
+    let ar = b.account("1200");
+    let before = b.l.account_balance(ar).unwrap();
+    assert!(matches!(
+        b.l.create_invoice(b.customer, d(2026, 6, 1), d(2026, 6, 30), bad.clone()),
+        Err(LedgerError::LineArithmetic(_))
+    ));
+    assert_eq!(b.l.account_balance(ar).unwrap(), before);
+    assert_eq!(b.l.next_invoice_id(), inv + 1);
+
+    // Both or neither: a quantity without a price is refused too.
+    let mut half = bad.clone();
+    half[0].amount = cents(9_999);
+    half[0].unit_price = None;
+    assert!(matches!(
+        b.l.create_invoice(b.customer, d(2026, 6, 1), d(2026, 6, 30), half),
+        Err(LedgerError::LineArithmetic(_))
+    ));
+}
+
+/// B-39 line accounts: an invoice takes revenue or deferred revenue; a
+/// bill takes an expense or a non-cash asset; roles, cash and headers are
+/// refused (plan P4b S4.1, A-10).
+#[test]
+fn document_line_account_refuses_roles_cash_and_placeholders() {
+    let mut b = books();
+    let deferred =
+        b.l.add_account(
+            "2400",
+            "Deferred Revenue",
+            AccountType::Liability,
+            None,
+            false,
+        )
+        .unwrap();
+    let revenue =
+        b.l.add_account("4000", "Revenue", AccountType::Revenue, None, false)
+            .unwrap();
+    let equipment =
+        b.l.add_account("1500", "Equipment", AccountType::Asset, None, false)
+            .unwrap();
+    let supplies =
+        b.l.add_account("6100", "Supplies", AccountType::Expense, None, false)
+            .unwrap();
+    let header =
+        b.l.add_account("9000", "Header", AccountType::Asset, None, true)
+            .unwrap();
+    let control =
+        b.l.add_account("1150", "Trade Receivables", AccountType::Asset, None, false)
+            .unwrap();
+    b.l.assign_role("receivables", Some(control)).unwrap();
+
+    let check = |l: &Ledger, kind, account| l.check_document_line_account(kind, account);
+    // An invoice line: revenue, or a liability holding no role.
+    assert!(check(&b.l, DocumentKind::Invoice, revenue).is_ok());
+    assert!(check(&b.l, DocumentKind::Invoice, deferred).is_ok());
+    assert!(check(&b.l, DocumentKind::Invoice, b.bank).is_err());
+    assert!(check(&b.l, DocumentKind::Invoice, supplies).is_err());
+    assert!(check(&b.l, DocumentKind::Invoice, equipment).is_err());
+    assert!(check(&b.l, DocumentKind::Invoice, control).is_err());
+    assert!(check(&b.l, DocumentKind::Invoice, header).is_err());
+    // A bill line: an expense, or a non-cash asset holding no role.
+    assert!(check(&b.l, DocumentKind::Bill, supplies).is_ok());
+    assert!(check(&b.l, DocumentKind::Bill, equipment).is_ok());
+    assert!(check(&b.l, DocumentKind::Bill, b.bank).is_err());
+    assert!(check(&b.l, DocumentKind::Bill, revenue).is_err());
+    assert!(check(&b.l, DocumentKind::Bill, deferred).is_err());
+    assert!(check(&b.l, DocumentKind::Bill, control).is_err());
+    assert!(check(&b.l, DocumentKind::Bill, header).is_err());
+
+    // The create path applies the same rule, and refuses before posting.
+    let before = b.l.next_bill_id();
+    let bad = vec![doc_line("Loan", 1_000, Some(b.bank), None, None)];
+    assert!(matches!(
+        b.l.create_bill(b.vendor, d(2026, 7, 1), d(2026, 7, 31), bad),
+        Err(LedgerError::DocumentLineAccount { .. })
+    ));
+    assert_eq!(b.l.next_bill_id(), before);
+}
+
+/// A-2, B-40: numbers run, a void keeps its number, legacy invoices are
+/// not counted, and a number is never reused.
+#[test]
+fn numbers_run_and_voids_keep_theirs() {
+    let mut b = books();
+    let first = {
+        let number = b.l.next_invoice_number("INV-", 1);
+        assert_eq!(number, "INV-0001");
+        b.l.create_invoice_with(
+            b.customer,
+            d(2026, 1, 5),
+            d(2026, 2, 4),
+            line("Work", 10_000),
+            InvoiceFields {
+                number: Some(number),
+                ..InvoiceFields::default()
+            },
+        )
+        .unwrap()
+    };
+    let second = {
+        let number = b.l.next_invoice_number("INV-", 1);
+        assert_eq!(number, "INV-0002");
+        b.l.create_invoice_with(
+            b.customer,
+            d(2026, 1, 6),
+            d(2026, 2, 5),
+            line("Work", 20_000),
+            InvoiceFields {
+                number: Some(number),
+                ..InvoiceFields::default()
+            },
+        )
+        .unwrap()
+    };
+    assert_eq!(
+        b.l.get_invoice(first).unwrap().number.as_deref(),
+        Some("INV-0001")
+    );
+    // A void keeps its number and still counts: the series never reuses
+    // one.
+    b.l.void_document(DocRef::Invoice(first), d(2026, 1, 7), "Duplicate")
+        .unwrap();
+    assert_eq!(
+        b.l.get_invoice(first).unwrap().number.as_deref(),
+        Some("INV-0001")
+    );
+    assert_eq!(b.l.next_invoice_number("INV-", 1), "INV-0003");
+    // A legacy invoice (no number) is not counted, shown as "Invoice {id}".
+    let legacy =
+        b.l.create_invoice(b.customer, d(2026, 1, 8), d(2026, 2, 7), line("Old", 100))
+            .unwrap();
+    assert_eq!(b.l.get_invoice(legacy).unwrap().number, None);
+    assert_eq!(b.l.next_invoice_number("INV-", 1), "INV-0003");
+    // Numbers are never reused, even by a direct create.
+    assert_eq!(
+        b.l.create_invoice_with(
+            b.customer,
+            d(2026, 1, 9),
+            d(2026, 2, 8),
+            line("Work", 100),
+            InvoiceFields {
+                number: Some("INV-0002".into()),
+                ..InvoiceFields::default()
+            },
+        ),
+        Err(LedgerError::DuplicateInvoiceNumber("INV-0002".into()))
+    );
+    assert_eq!(
+        b.l.get_invoice(second).unwrap().number.as_deref(),
+        Some("INV-0002")
+    );
+}
+
+/// B-40: four digits, wider past 9,999, never truncated.
+#[test]
+fn number_widens_past_9999() {
+    let mut b = books();
+    let number = b.l.next_invoice_number("INV-", 9_999);
+    assert_eq!(number, "INV-9999");
+    b.l.create_invoice_with(
+        b.customer,
+        d(2026, 2, 1),
+        d(2026, 3, 1),
+        line("Work", 100),
+        InvoiceFields {
+            number: Some(number),
+            ..InvoiceFields::default()
+        },
+    )
+    .unwrap();
+    assert_eq!(b.l.next_invoice_number("INV-", 9_999), "INV-10000");
+}
+
+/// B-40: a vendor's invoice number names one standing bill; case, spaces
+/// and hyphens are ignored; a duplicate needs a reason (plan P4b S4.1).
+#[test]
+fn duplicate_vendor_ref_refused_unless_a_reason_is_given() {
+    let mut b = books();
+    let fields = |vendor_ref: &str, reason: Option<&str>| BillFields {
+        vendor_ref: Some(vendor_ref.into()),
+        duplicate_reason: reason.map(str::to_string),
+        ..BillFields::default()
+    };
+    let first =
+        b.l.create_bill_with(
+            b.vendor,
+            d(2026, 1, 5),
+            d(2026, 2, 4),
+            line("Paper", 1_000),
+            fields("ACME-123", None),
+        )
+        .unwrap();
+    // Case, spaces and hyphens do not make a new number.
+    for same in ["acme 123", "Acme123", "ACME - 123"] {
+        assert_eq!(
+            b.l.create_bill_with(
+                b.vendor,
+                d(2026, 1, 6),
+                d(2026, 2, 5),
+                line("Paper", 2_000),
+                fields(same, None),
+            ),
+            Err(LedgerError::DuplicateVendorRef {
+                vendor: b.vendor,
+                vendor_ref: same.into()
+            })
+        );
+    }
+    // Another vendor's invoice may carry the same number.
+    let other = b.l.add_vendor("Other Supply").unwrap();
+    b.l.create_bill_with(
+        other,
+        d(2026, 1, 6),
+        d(2026, 2, 5),
+        line("Paper", 2_000),
+        fields("ACME-123", None),
+    )
+    .unwrap();
+    // A reason makes the second one a bill of its own.
+    let second =
+        b.l.create_bill_with(
+            b.vendor,
+            d(2026, 1, 7),
+            d(2026, 2, 6),
+            line("Paper", 3_000),
+            fields("acme 123", Some("Second shipment, vendor reissued it")),
+        )
+        .unwrap();
+    // A voided bill no longer stands, so its number is free again.
+    b.l.void_document(DocRef::Bill(first), d(2026, 1, 8), "Entered twice")
+        .unwrap();
+    b.l.void_document(DocRef::Bill(second), d(2026, 1, 8), "Entered twice")
+        .unwrap();
+    b.l.create_bill_with(
+        b.vendor,
+        d(2026, 1, 9),
+        d(2026, 2, 8),
+        line("Paper", 4_000),
+        fields("ACME-123", None),
+    )
+    .unwrap();
+}
diff --git a/crates/ledger-core/tests/spec_ledger.rs b/crates/ledger-core/tests/spec_ledger.rs
index 004ddcc..24d4662 100644
--- a/crates/ledger-core/tests/spec_ledger.rs
+++ b/crates/ledger-core/tests/spec_ledger.rs
@@ -1914,6 +1914,9 @@ fn one_line(amount: &str) -> Vec<DocumentLine> {
         description: "consulting".into(),
         amount: dec(amount),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }]
 }
 
@@ -2798,6 +2801,9 @@ fn a_new_account_named_like_a_sibling_or_holding_a_tin_is_refused() {
             description: "work".into(),
             amount: dec("100.00"),
             class_id: None,
+            account: None,
+            quantity: None,
+            unit_price: None,
         }],
     )
     .unwrap();
diff --git a/crates/ledger-core/tests/spec_party_totals.rs b/crates/ledger-core/tests/spec_party_totals.rs
index a88dd1f..4dfae4a 100644
--- a/crates/ledger-core/tests/spec_party_totals.rs
+++ b/crates/ledger-core/tests/spec_party_totals.rs
@@ -466,6 +466,9 @@ fn audit() -> Audit {
                 description: "filing".into(),
                 amount: d("80.00"),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
@@ -484,6 +487,9 @@ fn audit() -> Audit {
                 description: "consulting".into(),
                 amount: d("120.00"),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
diff --git a/crates/ledger-core/tests/spec_replayed_extremes.rs b/crates/ledger-core/tests/spec_replayed_extremes.rs
index 900f42f..b2ff481 100644
--- a/crates/ledger-core/tests/spec_replayed_extremes.rs
+++ b/crates/ledger-core/tests/spec_replayed_extremes.rs
@@ -305,6 +305,9 @@ fn documents_and_aging_are_exact_or_refused() {
         description: "x".into(),
         amount: a,
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     };
     // An entry as replay rebuilds it: Dr `dr` / Cr `cr` for `a`.
     let replayed = |l: &mut Ledger, dr, cr, a: Decimal| {
diff --git a/crates/ledger-core/tests/spec_roles.rs b/crates/ledger-core/tests/spec_roles.rs
index cff37c5..09d6fb5 100644
--- a/crates/ledger-core/tests/spec_roles.rs
+++ b/crates/ledger-core/tests/spec_roles.rs
@@ -42,6 +42,9 @@ fn line(desc: &str, amount: &str) -> DocumentLine {
         description: desc.to_string(),
         amount: dec(amount),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }
 }
 
diff --git a/crates/ledger-gui/src/demo.rs b/crates/ledger-gui/src/demo.rs
index b7dc75c..016bc55 100644
--- a/crates/ledger-gui/src/demo.rs
+++ b/crates/ledger-gui/src/demo.rs
@@ -764,6 +764,9 @@ pub fn build(dir: &Path, today: NaiveDate) -> Result<(), StoreError> {
                         .into(),
                     amount: amt,
                     class_id: Some(client_class),
+                    account: None,
+                    quantity: None,
+                    unit_price: None,
                 }],
             )?;
             open_invoices.push((inv, date, amt));
diff --git a/crates/ledger-gui/src/pages/cash.rs b/crates/ledger-gui/src/pages/cash.rs
index 43f4278..2a02053 100644
--- a/crates/ledger-gui/src/pages/cash.rs
+++ b/crates/ledger-gui/src/pages/cash.rs
@@ -667,6 +667,9 @@ mod tests {
                 description: "work".into(),
                 amount: cents(c),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }]
         };
         let acme = b.s.add_customer("Acme").unwrap();
diff --git a/crates/ledger-gui/src/pages/company.rs b/crates/ledger-gui/src/pages/company.rs
index 9430677..81220e1 100644
--- a/crates/ledger-gui/src/pages/company.rs
+++ b/crates/ledger-gui/src/pages/company.rs
@@ -798,6 +798,9 @@ mod tests {
                 description: "work".into(),
                 amount: cents(c),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }]
         };
         let acme = b.s.add_customer("Acme").unwrap();
diff --git a/crates/ledger-gui/src/pages/entry.rs b/crates/ledger-gui/src/pages/entry.rs
index 60b5f35..30d4b3c 100644
--- a/crates/ledger-gui/src/pages/entry.rs
+++ b/crates/ledger-gui/src/pages/entry.rs
@@ -785,6 +785,9 @@ mod tests {
                     description: "Brand identity, website and a long tail of revisions".into(),
                     amount: Decimal::new(123_456, 2),
                     class_id: Some(project),
+                    account: None,
+                    quantity: None,
+                    unit_price: None,
                 }],
             )
             .unwrap();
diff --git a/crates/ledger-gui/src/pages/parties.rs b/crates/ledger-gui/src/pages/parties.rs
index 641970e..0c61f7c 100644
--- a/crates/ledger-gui/src/pages/parties.rs
+++ b/crates/ledger-gui/src/pages/parties.rs
@@ -1725,6 +1725,9 @@ mod tests {
                 description: "work".into(),
                 amount: cents(c),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }]
         };
         // Owed, not yet due; owed, due today; paid, past due; owed, past
diff --git a/crates/ledger-gui/src/pages/profit.rs b/crates/ledger-gui/src/pages/profit.rs
index c2a74f6..4ceb8a2 100644
--- a/crates/ledger-gui/src/pages/profit.rs
+++ b/crates/ledger-gui/src/pages/profit.rs
@@ -449,6 +449,9 @@ mod tests {
                 description: "work".into(),
                 amount: cents(c),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }]
         };
         let acme = b.s.add_customer("Acme").unwrap();
diff --git a/crates/ledger-gui/tests/invoices.rs b/crates/ledger-gui/tests/invoices.rs
index f1025c7..f51ad3c 100644
--- a/crates/ledger-gui/tests/invoices.rs
+++ b/crates/ledger-gui/tests/invoices.rs
@@ -42,6 +42,9 @@ fn line(description: &str, cents: i64) -> DocumentLine {
         description: description.into(),
         amount: Decimal::new(cents, 2),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }
 }
 
diff --git a/crates/ledger-gui/tests/parties.rs b/crates/ledger-gui/tests/parties.rs
index 1095f65..4c68456 100644
--- a/crates/ledger-gui/tests/parties.rs
+++ b/crates/ledger-gui/tests/parties.rs
@@ -75,6 +75,9 @@ fn doc(c: i64) -> Vec<DocumentLine> {
         description: "work".into(),
         amount: cents(c),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }]
 }
 
diff --git a/crates/ledger-gui/tests/projects.rs b/crates/ledger-gui/tests/projects.rs
index 7dc9d9e..b0b3735 100644
--- a/crates/ledger-gui/tests/projects.rs
+++ b/crates/ledger-gui/tests/projects.rs
@@ -1284,6 +1284,9 @@ fn an_invoice_and_a_bill_show_each_lines_project() {
         description: what.into(),
         amount: cents(c),
         class_id: class,
+        account: None,
+        quantity: None,
+        unit_price: None,
     };
     let inv = s
         .create_invoice(
diff --git a/crates/ledger-gui/tests/view_model.rs b/crates/ledger-gui/tests/view_model.rs
index cf3c1e7..f184b07 100644
--- a/crates/ledger-gui/tests/view_model.rs
+++ b/crates/ledger-gui/tests/view_model.rs
@@ -263,6 +263,9 @@ fn origins_and_parties() {
             description: "x".into(),
             amount: Decimal::new(a, 2),
             class_id: None,
+            account: None,
+            quantity: None,
+            unit_price: None,
         }]
     };
     let inv = s
@@ -645,6 +648,9 @@ fn more_origins_and_parties() {
             description: "x".into(),
             amount: Decimal::new(a, 2),
             class_id: None,
+            account: None,
+            quantity: None,
+            unit_price: None,
         }]
     };
     s.create_invoice(cust, today, today + Days::new(30), line(10_000))
diff --git a/crates/ledger-mcp/src/server.rs b/crates/ledger-mcp/src/server.rs
index 4b236dd..be1013b 100644
--- a/crates/ledger-mcp/src/server.rs
+++ b/crates/ledger-mcp/src/server.rs
@@ -2627,6 +2627,9 @@ fn document_lines(
                     .as_deref()
                     .map(|c| resolve_class(store, c))
                     .transpose()?,
+                account: None,
+                quantity: None,
+                unit_price: None,
             })
         })
         .collect()
diff --git a/crates/ledger-package/src/invoice.rs b/crates/ledger-package/src/invoice.rs
index 60647fc..6fa94b6 100644
--- a/crates/ledger-package/src/invoice.rs
+++ b/crates/ledger-package/src/invoice.rs
@@ -181,6 +181,9 @@ mod tests {
                     description: "Consulting".into(),
                     amount: Decimal::new(50_000, 2),
                     class_id: None,
+                    account: None,
+                    quantity: None,
+                    unit_price: None,
                 }],
             )
             .unwrap();
@@ -248,6 +251,9 @@ mod tests {
             description: d.into(),
             amount: Decimal::new(cents, 2),
             class_id: None,
+            account: None,
+            quantity: None,
+            unit_price: None,
         };
         let inv = l
             .create_invoice(
diff --git a/crates/ledger-package/tests/package.rs b/crates/ledger-package/tests/package.rs
index 972b90c..164e2f5 100644
--- a/crates/ledger-package/tests/package.rs
+++ b/crates/ledger-package/tests/package.rs
@@ -1774,6 +1774,9 @@ fn the_package_iif_carries_an_invoices_and_a_bills_projects() {
         description: description.into(),
         amount: Decimal::from_str(amount).unwrap(),
         class_id,
+        account: None,
+        quantity: None,
+        unit_price: None,
     };
     let customer = s.add_customer("Potter").unwrap();
     s.create_invoice(
diff --git a/crates/ledger-store/src/error.rs b/crates/ledger-store/src/error.rs
index 5affe43..09881aa 100644
--- a/crates/ledger-store/src/error.rs
+++ b/crates/ledger-store/src/error.rs
@@ -47,6 +47,17 @@ pub enum StoreError {
     #[error("json error: {0}")]
     Json(#[from] serde_json::Error),
 
+    /// A document line carries a field this version's journal cannot write
+    /// yet: line accounts, quantities and unit prices are journaled from
+    /// S4.3 (`documents_v2`) on. Refused before anything is journaled.
+    #[error(
+        "this document line names {field}, which these books cannot journal yet: line accounts, quantities and unit prices wait for the documents_v2 upgrade (S4.3). Nothing was changed; give the line one amount for now"
+    )]
+    DocumentFieldsAwaitUpgrade {
+        /// The field it names: "an account", "a quantity and unit price".
+        field: &'static str,
+    },
+
     /// The engine rejected the operation. The journal is untouched.
     #[error("ledger error: {0}")]
     Ledger(#[from] ledger_core::LedgerError),
diff --git a/crates/ledger-store/src/store.rs b/crates/ledger-store/src/store.rs
index c5410b0..986e5ad 100644
--- a/crates/ledger-store/src/store.rs
+++ b/crates/ledger-store/src/store.rs
@@ -2959,6 +2959,10 @@ impl Store {
         due_date: NaiveDate,
         lines: Vec<DocumentLine>,
     ) -> Result<InvoiceId, StoreError> {
+        // S4.1's line fields are not journaled yet (S4.3's `documents_v2`
+        // writes them); refuse before `rehearse`, so replay can never lose
+        // one.
+        check_journaled_document_lines(&lines)?;
         self.rehearse(|l| l.create_invoice(customer_id, date, due_date, lines.clone()))?;
         self.approval_gate(
             |l| l.create_invoice(customer_id, date, due_date, lines.clone()),
@@ -2986,7 +2990,9 @@ impl Store {
         posting.extend(
             arap::document_parts(&lines, "the invoice")?
                 .into_iter()
-                .map(|(class, amount)| (revenue, Side::Credit, amount, class)),
+                .map(|((account, class), amount)| {
+                    (account.unwrap_or(revenue), Side::Credit, amount, class)
+                }),
         );
         let (entry_id, mut journaled) = self.journal_auto_lines(date, &description, &posting)?;
         let doc_lines: Vec<Value> = lines.iter().map(document_line_json).collect();
@@ -3029,6 +3035,9 @@ impl Store {
         due_date: NaiveDate,
         lines: Vec<DocumentLine>,
     ) -> Result<BillId, StoreError> {
+        // See create_invoice: the line's account, quantity and unit price
+        // wait for S4.3's journaling.
+        check_journaled_document_lines(&lines)?;
         self.rehearse(|l| l.create_bill(vendor_id, date, due_date, lines.clone()))?;
         self.approval_gate(
             |l| l.create_bill(vendor_id, date, due_date, lines.clone()),
@@ -3050,7 +3059,9 @@ impl Store {
         let description = format!("Bill {bill_id}");
         let mut posting: Vec<_> = arap::document_parts(&lines, "the bill")?
             .into_iter()
-            .map(|(class, amount)| (expense, Side::Debit, amount, class))
+            .map(|((account, class), amount)| {
+                (account.unwrap_or(expense), Side::Debit, amount, class)
+            })
             .collect();
         posting.push((ap, Side::Credit, total, None));
         let (entry_id, mut journaled) = self.journal_auto_lines(date, &description, &posting)?;
@@ -5607,6 +5618,27 @@ fn plain_line_json(account: AccountId, side: Side, amount: Money) -> Value {
 
 /// One invoice/bill document line as journal JSON. Amounts are decimal
 /// strings, never floats.
+/// Refuse a document line carrying a field the journal does not write yet
+/// (S4.1 through S4.2): S4.3's `documents_v2` journals the line's account,
+/// quantity and unit price. Called before `rehearse`, so a refusal leaves
+/// the journal and the books exactly as they were, and replay never loses
+/// one. S4.3 removes this guard when it journals the fields.
+fn check_journaled_document_lines(lines: &[DocumentLine]) -> Result<(), StoreError> {
+    for line in lines {
+        if line.account.is_some() {
+            return Err(StoreError::DocumentFieldsAwaitUpgrade {
+                field: "an account",
+            });
+        }
+        if line.quantity.is_some() || line.unit_price.is_some() {
+            return Err(StoreError::DocumentFieldsAwaitUpgrade {
+                field: "a quantity and unit price",
+            });
+        }
+    }
+    Ok(())
+}
+
 fn document_line_json(l: &DocumentLine) -> Value {
     let mut v = json!({
         "description": l.description,
@@ -5646,6 +5678,12 @@ fn parse_document_lines(p: &Value) -> Result<Vec<DocumentLine>, StoreError> {
                             })?,
                     ),
                 },
+                // The new line fields are read in S4.3; an older version
+                // never wrote them, and replay of a document written by
+                // this one leaves the S4.1 shape.
+                account: None,
+                quantity: None,
+                unit_price: None,
             })
         })
         .collect()
diff --git a/crates/ledger-store/tests/arap_props.rs b/crates/ledger-store/tests/arap_props.rs
index c806128..a014f20 100644
--- a/crates/ledger-store/tests/arap_props.rs
+++ b/crates/ledger-store/tests/arap_props.rs
@@ -133,6 +133,9 @@ fn run(s: &mut Store, k: &Setup, ops: &[Op], docs: &mut Vec<DocRef>) -> Result<(
                 description: "work".into(),
                 amount: cents(c),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }]
         };
         let result: Result<(), StoreError> = match *op {
diff --git a/crates/ledger-store/tests/arap_standing.rs b/crates/ledger-store/tests/arap_standing.rs
index bbf582e..b2b9723 100644
--- a/crates/ledger-store/tests/arap_standing.rs
+++ b/crates/ledger-store/tests/arap_standing.rs
@@ -12,7 +12,7 @@
 use chrono::NaiveDate;
 use ledger_core::arap::DocumentLine;
 use ledger_core::{AccountType, Currency, Money, Side};
-use ledger_store::{JOURNAL_FILE, Store};
+use ledger_store::{JOURNAL_FILE, Store, StoreError};
 use rust_decimal::Decimal;
 use serde_json::{Value, json};
 use std::path::{Path, PathBuf};
@@ -30,6 +30,9 @@ fn line(what: &str, c: i64) -> DocumentLine {
         description: what.into(),
         amount: cents(c),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }
 }
 
@@ -611,3 +614,97 @@ fn legacy_documents_replay_with_tags() {
         .id();
     assert!((0..2).all(|i| l.line_doc(hand, i).is_none()));
 }
+
+/// S4.1's line fields (the account, the quantity and unit price) are not
+/// journaled yet: S4.3's `documents_v2` writes them. The store refuses
+/// such a line before it rehearses or journals anything, so replay can
+/// never lose one; an ordinary line still posts exactly as before, with
+/// no new key in its journal payload.
+#[test]
+fn document_line_fields_wait_for_documents_v2() {
+    let dir = test_dir("unjournaled-fields");
+    let mut s = Store::create(&dir.0, Currency::USD).unwrap();
+    let bank = s
+        .add_account("1000", "Bank", AccountType::Asset, None, false)
+        .unwrap();
+    let c = s.add_customer("Fernhill Labs").unwrap();
+    let v = s.add_vendor("Tobin Harlow Supply").unwrap();
+    // A first invoice creates the control accounts, so the assertions
+    // below see only the document's own events.
+    s.create_invoice(c, d(2026, 3, 1), d(2026, 4, 1), vec![line("Seed", 1_000)])
+        .unwrap();
+    let from = journal_len(&dir.0);
+    let next_invoice = s.ledger().next_invoice_id();
+    let next_bill = s.ledger().next_bill_id();
+
+    let with_account = DocumentLine {
+        description: "Design".into(),
+        amount: cents(5_000),
+        class_id: None,
+        account: Some(bank),
+        quantity: None,
+        unit_price: None,
+    };
+    for refused in [
+        s.create_invoice(c, d(2026, 4, 1), d(2026, 5, 1), vec![with_account.clone()]),
+        s.create_bill(v, d(2026, 4, 1), d(2026, 5, 1), vec![with_account]),
+    ] {
+        assert!(
+            matches!(
+                refused,
+                Err(StoreError::DocumentFieldsAwaitUpgrade {
+                    field: "an account"
+                })
+            ),
+            "{refused:?}"
+        );
+    }
+
+    let with_price = DocumentLine {
+        description: "Hours".into(),
+        amount: cents(9_999),
+        class_id: None,
+        account: None,
+        quantity: Some(Decimal::from(3)),
+        unit_price: Some(cents(3_333)),
+    };
+    assert!(matches!(
+        s.create_invoice(c, d(2026, 4, 1), d(2026, 5, 1), vec![with_price.clone()]),
+        Err(StoreError::DocumentFieldsAwaitUpgrade {
+            field: "a quantity and unit price"
+        })
+    ));
+    assert!(matches!(
+        s.create_bill(v, d(2026, 4, 1), d(2026, 5, 1), vec![with_price]),
+        Err(StoreError::DocumentFieldsAwaitUpgrade {
+            field: "a quantity and unit price"
+        })
+    ));
+
+    // Every refusal left the journal and the allocators exactly as they
+    // were.
+    assert_eq!(journal_len(&dir.0), from);
+    assert_eq!(s.ledger().next_invoice_id(), next_invoice);
+    assert_eq!(s.ledger().next_bill_id(), next_bill);
+    s.verify().unwrap();
+
+    // An ordinary line posts exactly as before: the same five events, and
+    // the line carries no key the older journal did not have.
+    let inv = s
+        .create_invoice(c, d(2026, 4, 1), d(2026, 5, 1), vec![line("Design", 5_000)])
+        .unwrap();
+    let got = since(&dir.0, from);
+    assert_eq!(got.len(), 5, "{got:?}");
+    assert_eq!(got[4].0, "invoice.created");
+    let keys: Vec<&String> = got[4].1["lines"][0].as_object().unwrap().keys().collect();
+    assert_eq!(keys, ["amount", "description"]);
+    let live = s.ledger().clone();
+    drop(s);
+    let s = Store::open(&dir.0).unwrap();
+    assert!(live.differs_from(s.ledger()).is_empty());
+    assert_eq!(
+        s.ledger().get_invoice(inv).unwrap().total(),
+        Ok(cents(5_000))
+    );
+    s.verify().unwrap();
+}
diff --git a/crates/ledger-store/tests/attachments.rs b/crates/ledger-store/tests/attachments.rs
index 8370705..a23afc6 100644
--- a/crates/ledger-store/tests/attachments.rs
+++ b/crates/ledger-store/tests/attachments.rs
@@ -322,6 +322,9 @@ fn every_subject(s: &mut Store, fx: &Fx) -> Vec<Subject> {
                 description: "App".into(),
                 amount: dec("100.00"),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
@@ -335,6 +338,9 @@ fn every_subject(s: &mut Store, fx: &Fx) -> Vec<Subject> {
                 description: "Design".into(),
                 amount: dec("200.00"),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
diff --git a/crates/ledger-store/tests/document_projects.rs b/crates/ledger-store/tests/document_projects.rs
index 7de8558..d3722ea 100644
--- a/crates/ledger-store/tests/document_projects.rs
+++ b/crates/ledger-store/tests/document_projects.rs
@@ -53,6 +53,9 @@ fn line(what: &str, c: i64, class: Option<ClassId>) -> DocumentLine {
         description: what.into(),
         amount: cents(c),
         class_id: class,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }
 }
 
diff --git a/crates/ledger-store/tests/fixtures/old-books-writer/src/main.rs b/crates/ledger-store/tests/fixtures/old-books-writer/src/main.rs
index bde25f8..fb86ddb 100644
--- a/crates/ledger-store/tests/fixtures/old-books-writer/src/main.rs
+++ b/crates/ledger-store/tests/fixtures/old-books-writer/src/main.rs
@@ -79,7 +79,9 @@ fn main() {
     // 11. invoice with sub-cent lines that cancel
     { let mut b = books(&root, "invoice_fine");
       let c = b.s.add_customer("Cust").unwrap();
-      report("invoice_fine", b.s.create_invoice(c, d(2026,3,1), d(2026,3,31), vec![DocumentLine{description:"a".into(), amount: dec("0.00000000001")}, DocumentLine{description:"b".into(), amount: dec("9.99999999999")}])); }
+      report("invoice_fine", b.s.create_invoice(c, d(2026,3,1), d(2026,3,31), vec![
+        DocumentLine{description:"a".into(), amount: dec("0.00000000001"), account: None, quantity: None, unit_price: None},
+        DocumentLine{description:"b".into(), amount: dec("9.99999999999"), account: None, quantity: None, unit_price: None}])); }
     // 12. period year 0
     { let mut b = books(&root, "period_year0");
       report("period_year0", b.s.create_period("y0", d(0,1,1), d(0,12,31))); }
diff --git a/crates/ledger-store/tests/roles.rs b/crates/ledger-store/tests/roles.rs
index 08523ec..c601de6 100644
--- a/crates/ledger-store/tests/roles.rs
+++ b/crates/ledger-store/tests/roles.rs
@@ -60,6 +60,9 @@ fn line(desc: &str, amount: &str) -> DocumentLine {
         description: desc.to_string(),
         amount: dec(amount),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     }
 }
 
diff --git a/crates/ledger-store/tests/settings.rs b/crates/ledger-store/tests/settings.rs
index da4e8af..973dbef 100644
--- a/crates/ledger-store/tests/settings.rs
+++ b/crates/ledger-store/tests/settings.rs
@@ -350,6 +350,9 @@ fn approvals_cover_every_post() {
         description: "work".into(),
         amount: Decimal::from(n),
         class_id: None,
+        account: None,
+        quantity: None,
+        unit_price: None,
     };
     assert!(matches!(
         s.create_bill(v, d(2026, 10, 1), d(2026, 10, 31), vec![line(600)]),
diff --git a/crates/ledger-store/tests/store.rs b/crates/ledger-store/tests/store.rs
index caf6440..8e68376 100644
--- a/crates/ledger-store/tests/store.rs
+++ b/crates/ledger-store/tests/store.rs
@@ -816,6 +816,9 @@ fn vendor_1099_tags_replay_and_project() {
                 description: "Design".into(),
                 amount: Decimal::from(1500),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
@@ -1229,6 +1232,9 @@ mod refusals {
                 description: "work".into(),
                 amount: Decimal::new(c, 2),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }]
         };
         match *op {
@@ -2827,6 +2833,9 @@ fn the_database_tracks_what_an_invoice_has_been_paid() {
                 description: "work".into(),
                 amount: Decimal::from(100),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
@@ -3388,6 +3397,9 @@ fn the_tax_category_policy_refuses_only_what_it_says() {
                 description: "hosting".into(),
                 amount: Decimal::new(4_200, 2),
                 class_id: None,
+                account: None,
+                quantity: None,
+                unit_price: None,
             }],
         )
         .unwrap();
diff --git a/docs/verification.md b/docs/verification.md
index 734d687..9d03108 100644
--- a/docs/verification.md
+++ b/docs/verification.md
@@ -479,6 +479,31 @@ one kernel function, `kernel::unrecovered_cost`:
     `unrecovered_cost_only_for_on_spec_and_never_negative`. No Lean model:
     the function is one subtraction and a `max`.
 
+### Payment terms and document lines (P4b S4.1)
+
+Payment terms (rules.md B-39) give a due date and a discount date by
+calendar arithmetic in `arap::Terms`, and the two money figures they touch
+come from the kernel:
+
+33. **A discount never exceeds its stated percentage of the total, and a
+    line's amount is exactly its quantity times its unit price.** The
+    bound is `total × basis points / 10,000`, exact: a result times 10,000
+    is the total times the basis points, and it is never above the total;
+    when no whole amount can hold the exact bound, or a factor would
+    overflow, the kernel refuses (None) rather than rounding. A line's
+    amount is the exact product, never rounded, and None on overflow.
+    Terms' own due dates (Net n, Net n EOM, due on receipt, custom; the
+    9999-12 bound) are checked by `spec_documents.rs`'s
+    `terms_derive_due_dates`, and the parser's round trip by
+    `terms_describe_and_parse_round_trip`.
+    - Kani `discount_max_is_bounded` (at i32, as the proration charge
+      harnesses are: the law relates a product to a quotient) ·
+      `line_amount_is_exact` (at i64) · bridge `discount_max_agrees`,
+      `discount_max_i32_agrees_with_i64`, `line_amount_agrees` · tests
+      `discount_bounds_and_late_reason`, `qty_times_price_must_equal_amount`.
+      No Lean model: these are two arithmetic laws, not a new `Ledger`
+      command (S4.1 adds fields to the existing document commands).
+
 ## What the proofs found
 
 The engine already had 190+ tests, property tests, mutation testing,
@@ -674,6 +699,10 @@ then) and `just prove-slow` 1,365 s (seven then; `entry_flows_sum_to_cash`
 headline theorems) and `just prove-slow` 467 s (8 harnesses, the slowest
 `entry_flows_sum_to_cash` at 301 s).
 
+P4b S4.1's two harnesses were measured on 2026-10-26 (a busy machine);
+the rest are the 2026-10-22 run. `discount_max_is_bounded`'s 163 s is
+Kani's verification time (it runs in `prove-slow`).
+
 Every harness, the law it proves, the recipe that runs it, and its time
 in that quiet run (`prove`: each harness's verification time; `prove-slow`:
 each harness's whole run, its compile of about 50 s included):
@@ -735,4 +764,6 @@ each harness's whole run, its compile of about 50 s included):
 | `true_up_reaches_the_target` | 30 | prove | 0 |
 | `basis_figures_laws` | 31 | prove | 0 |
 | `unrecovered_cost_laws` | 32 | prove | 0 |
+| `discount_max_is_bounded` | 33 | prove-slow | 163 |
+| `line_amount_is_exact` | 33 | prove | 6 |
 | `kani_symbolic_copy_canary` | (the checker: "Trusting the checker") | prove | 3 |
diff --git a/justfile b/justfile
index cbe97f1..1fa699d 100644
--- a/justfile
+++ b/justfile
@@ -69,7 +69,7 @@ sweep-test-tmp:
 # 100 minutes of CPU, 2026-10-21) can't finish inside the 30-minute cap at
 # four jobs, a CI runner's. Every other harness in src/proofs.rs runs in `prove`, a new one
 # included; a name here that isn't a harness fails both (docs/verification.md).
-kani_slow := "accounting_equation cumulative_close_never_drifts_a_unit_at_near_thirds cumulative_closing_entry_balances entry_flows_pure_are_movements entry_flows_sum_to_cash prorate_parts_sum_to_total sums_are_exact the_last_months_charge_is_within_half_a_cent"
+kani_slow := "accounting_equation cumulative_close_never_drifts_a_unit_at_near_thirds cumulative_closing_entry_balances discount_max_is_bounded entry_flows_pure_are_movements entry_flows_sum_to_cash prorate_parts_sum_to_total sums_are_exact the_last_months_charge_is_within_half_a_cent"
 
 # Formal proofs: Kani on the accounting kernel (all but kani_slow), Lean for books of any size (docs/verification.md)
 prove: (_kani "fast")