diff --git a/README.md b/README.md
index f73a0d6..ae606b8 100644
--- a/README.md
+++ b/README.md
@@ -16,10 +16,14 @@ Charon/Aeneas transpilation pipeline:
 ```
 
 Every theorem is stated about the **actual Aeneas-transpiled Rust code** from
-`src/fields/fp.rs` / `src/curves.rs`. There are **no bridge axioms**: the
-correctness of add/sub/neg/mul/square/montgomery_reduce/invert is *proven*,
-not assumed. (A previous attempt at this target axiomatized exactly those
-statements; this repository exists to do it properly.)
+`src/fields/fp.rs`. The rule is **no bridge axioms**: nothing is claimed
+proven that is in fact assumed. Proven today: sub/neg, the adc/sbb/mac
+helpers, the constants, primality, and the denotation layer;
+add/mul/montgomery_reduce/square/invert are **in progress** (drafted in
+`Proofs/drafts/`, blocked on kernel proof-checking memory — see Layer status
+below). No curve extraction exists yet. (A previous attempt at this target
+axiomatized exactly the statements this repository refuses to assume; it
+exists to do them properly or not claim them.)
 
 ## Layer status
 
diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md
index f6a6ebc..23c900c 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]`. Three representative
+   certificates (`P_prime`, `sub_spec`, `INV_spec`) are `#print axioms`-audited
+   against exactly this list; the remaining foundation theorems are protected
+   by the no-axiom-declaration grep over `Proofs/` only, which is weaker —
+   it does not audit their cones.
 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