diff --git a/crates/buzz-core/djinn-relay-filter/README.md b/crates/buzz-core/djinn-relay-filter/README.md
index 2c412fd87b..d829418515 100644
--- a/crates/buzz-core/djinn-relay-filter/README.md
+++ b/crates/buzz-core/djinn-relay-filter/README.md
@@ -17,7 +17,7 @@ Keys and values are exact case-sensitive UTF-8 bytes. Later tag strings are irre
 
 ## Generation and proof boundary
 
-The installed upstream is pinned to `8a9ae17c9a6cdbc5220f1881f5ad69f7e2d7e047`. `cargo djinn implement --agent codex` generated both [the complete Rust solution](djinn/solution/mod.rs) and [its Lean proofs](djinn/proofs/RelayFilter/Proofs.lean). The outer implementation owner authored the declarative specification, data-only projection, workload, tests and registry plumbing, **not** the Rust matching algorithm or Lean proofs. The initial fully verified implementation has 144 Rust lines and passed all 16 obligations with the standard axiom audit. Actual `cargo djinn optimize --cycles 3 --jobs 1` accepted two candidates and rejected/reverted the third after proof and timing. The frozen full caller objective improved from 10.297 ms to 7.560 ms per iteration (1.36× versus the first generated implementation), measured by the isolated research compiler. Detailed case measurements, regressions and hashes are recorded in the evidence.
+The installed upstream is pinned to `8a9ae17c9a6cdbc5220f1881f5ad69f7e2d7e047`. `cargo djinn implement --agent codex` generated both [the complete Rust solution](djinn/solution/mod.rs) and [its Lean proofs](djinn/proofs/RelayFilter/Proofs.lean). The outer implementation owner authored the declarative specification, data-only projection, workload, tests and registry plumbing, **not** the Rust matching algorithm or Lean proofs. The initial fully verified implementation has 144 Rust lines and passed all 16 obligations with the standard axiom audit. Actual `cargo djinn optimize --cycles 3 --jobs 1` accepted two candidates and rejected/reverted the third after proof and timing. The [archived original structural objective](evidence/STRUCTURAL-V1.md), which included the later-corrected routing-inconsistent fixtures, improved from 10.297 ms to 7.560 ms per iteration (1.36× versus the first generated implementation), measured by the isolated research compiler. Detailed case measurements, regressions and hashes are recorded in the evidence.
 
 The proof covers the complete generated predicate: OR, all scalar fields, all generic tags, fallback, termination and absence of Rust panics in the translated operation. The supporting specifications are total and the top-level Boolean result is unambiguous; existence is discharged from the proved implementation. Only `propext`, `Classical.choice`, and `Quot.sound` may occur in audited theorem dependencies. There are no added axioms, admissions, weak output contracts or modifications to trusted translation/models.