diff --git a/WALLET.md b/WALLET.md
index 7930922..4bf8a2c 100644
--- a/WALLET.md
+++ b/WALLET.md
@@ -98,6 +98,22 @@ custody wallet that cannot show its evidence has no business existing.
`--trusted-provider` is **required**: you must name whose *observations*
you are consuming. You are never asked to trust their verdicts.
+### You hold the ruler
+
+The allowed-axioms lists the gate checks against are a **requirements
+card** that ships in *your* tooling ([the ed25519
+profile](src/pacta/profiles/ed25519.py)) — small enough to read over
+coffee, re-derivable from the attested repos' own docs and check
+scripts, and replaceable with a card you write yourself from first
+principles. Verdicts are re-derived against *your* copy, name by name;
+the provider's labels are ignored. If your card is stricter than
+today's supply (e.g. "SHA-512 itself proven"), the gap is itemized and
+your options are honest: accept a named line item, walk away, or prove
+the missing piece and enter it into the log — *if your ruler is
+stricter than our supply, your ruler is our roadmap.* The full
+walk-through is
+[lecture 11](notebooks/11_the_customers_eye_view.ipynb).
+
---
## Quickstart
diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py
index 8216406..ec12b15 100644
--- a/provider/src/pacta_provider/webdocs.py
+++ b/provider/src/pacta_provider/webdocs.py
@@ -249,6 +249,27 @@ the content hash) and build it yourself — compiler and build are declared trus
until the reproducible-builds program (R5) lands. Every attestation carries its full
residual-risk list. Honesty about the boundary is the product.
+You hold the ruler
+The list of assumptions a certificate is allowed to rest on
+is not something this site hands you at verification time — it is a
+requirements card that lives in your tooling, on
+your disk, and that you can read in five minutes or rewrite from first
+principles: Lean's three foundational axioms, plus — for the signature tiers only —
+named placeholders for SHA-512 and the wire format. Your tooling ignores this
+operator's pass/fail labels entirely and re-derives every verdict by comparing the
+attestation's observed axiom list against your card, name by name.
+The operator is trusted to copy down what the proof kernel printed — never to
+interpret it.
+A card you write yourself will match this log's supply
+
exactly — and that is engineered, not coincidence: the corpus was
+shrunk until every remaining axiom justifies its existence. If your card is
+
stricter (say: "SHA-512 itself must be proven"), there is nothing here to
+negotiate — the gap is itemized, never blurred, and you have three honest options:
+accept a
named line item, walk away, or prove the missing piece and enter it
+into this same log.
If your ruler is stricter than our supply, your ruler is
+our roadmap. (The full walk-through is lecture 11 in the
+
course.)
The paper