2.12. Provenance and audit (R23, R24)🔗

R23 — A value's provenance is recordable and auditable. Beyond what kind a quantity is (R1) and whose it is (R19, R22): where it came from. Provenance ν κ records a kind-typed value-flow graph — ports, node introductions each carrying an evidence tier, hyperedge occurrences, and the exits where values leave the calculus for the bare carrier — and Contract is the boundary an author declares for a scope, checkable against the boundary the scope actually computes (Contract.discharges). A membership choice can be wrong, and this is the structure it can be wrong about: a changed part list changes a difference list, never passes silently.

R24 — An audit is a claim about its scope, never about the library. The discipline that keeps every other requirement's evidence honest at adoption time. The unkinded surface of a scope is enumerable (boundarySites), reported against a tier vocabulary that includes the interface tier — the boundary where erasing to a bare carrier is the sanctioned design, so an audit does not score a Mathlib fderiv call as a defect — and a blessed scope only grows: the ratchet (#kind_mint_ratchet) compares the current ledger against the pinned one and throws on regression, so a clean audit cannot silently shrink to stay clean.