diff --git a/README.md b/README.md
index aa44b64..ab653c1 100644
--- a/README.md
+++ b/README.md
@@ -18,8 +18,10 @@ coherent proof pyramid in Lean 4 via the Charon/Aeneas transpilation pipeline:
 Every layer states its theorems about the **actual Aeneas-transpiled Rust
 code** (never about a hand-written re-model), and every claim in the status
 table below is backed by a compiled proof plus an axiom audit of the named
-certificate. Files that do not compile under `verification/check.sh` are not
-in this repository.
+certificate. Files that compile under neither `verification/check.sh` nor
+`verification/check-scalar.sh` are not in this repository — each shipped
+proof source belongs to exactly one button's manifest, and the seam gate
+fails the build otherwise.
 
 ## Layer status
 
@@ -110,7 +112,7 @@ cones deviates from the boundary above.
 source ~/aeneas-toolchain/env.sh
 cd verification
 ./extract.sh    # Rust → LLBC → Lean (regenerates gen/)
-./check.sh      # compiles EVERY shipped file + axiom-audits EVERY certificate
+./check.sh      # compiles + audits everything the MAIN manifest owns (scalar layer: its own button below)
 ```
 
 The gen model is ONE merged universe (`gen/CurveField`: field + curve +
diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md
index 6bcd6b4..dbc14a0 100644
--- a/TRUSTED-BASE.md
+++ b/TRUSTED-BASE.md
@@ -4,8 +4,11 @@ What you must believe for the theorems in this repository to transfer to the
 running Rust code. Everything else is machine-checked.
 
 1. **Lean 4 kernel** (v4.30.0-rc2) and its three foundational axioms
-   `[propext, Classical.choice, Quot.sound]`. Every certificate is
-   `#print axioms`-audited against exactly this list.
+   `[propext, Classical.choice, Quot.sound]`. Every arithmetic and scalar
+   certificate is `#print axioms`-audited against exactly this list; the four
+   apex-tier certificates are audited against this list plus their documented
+   boundary axioms (the signature-apex item below), both enforced exactly —
+   nothing more, nothing less — by the button.
 2. **mathlib** (prebuilt oleans fetched by `lake exe cache get`).
 3. **Charon + Aeneas** (pinned `9dd7f23c` / `bf13c42e`): the translation
    from Rust MIR to the Lean model is assumed faithful. The generated
@@ -175,8 +178,10 @@ running Rust code. Everything else is machine-checked.
      cross-check, its corpus being mathlib-free.
 
    · *The scalar layer is outside this phase.* Thirteen `Proofs/Scalar*`
-     modules belong to `check-scalar.sh` and are inventoried by nothing. That
-     is the two-button seam, still open. Phase 2c prints every uncovered
+     modules belong to `check-scalar.sh` and sit outside `check.sh`'s
+     Phase 2c specifically — they are inventoried by `check-scalar.sh`'s own
+     Phase 2c against `inventory-allowlist-scalar.txt`, both directions. The
+     two-button seam itself closed 2026-07-30 (see the two-button item below). Phase 2c prints every uncovered
      module by name on every run, so the omission is visible rather than
      inferred.