diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 025df4b..0e662ba 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -6,10 +6,10 @@
 
 [abstract]
 This is the current, source-anchored verification record for the Agda
-formalisation. The authoritative positive tree contains *25 source modules* and
-the negative-control manifest contains *19 expected-rejection fixtures*. The
-partial-recovery extension adds two modules and two fixtures to the preceding
-23-module/17-fixture corpus, retaining four isolated mutation controls. The
+formalisation. The authoritative positive tree contains *31 source modules* and
+the negative-control manifest contains *24 expected-rejection fixtures*. The
+query/observer/sufficiency extension adds six modules and five fixtures to the
+preceding 25-module/19-fixture corpus, retaining four isolated mutation controls. The
 source is constructive, builtins-only, map-only at its base interface, and has
 no postulates or proof escape hatches. Exact theorem scope and trust boundaries
 are recorded below; historical snapshots remain in `AFFIRMATION.adoc` and are
@@ -17,6 +17,13 @@ not current inventory.
 
 == Status vocabulary
 
+The query/observer/sufficiency extension is locally *AGDA-VERIFIED*: 31 source
+modules, 24 semantic rejections, five new valid-prefix controls, four mutation
+controls and the unchanged exact 23-span warning allowance passed under Agda
+2.6.4.3. Its exact assumptions and verification scope are in
+link:docs/query-recovery.adoc[]. The following partial-recovery receipt applies
+to the preceding corpus and is not a receipt for the new six modules.
+
 The partial-recovery extension is locally *AGDA-VERIFIED* by the complete
 Agda 2.6.4.3 core gate: 25 source modules, 19 intended rejections and four
 mutation controls, with the existing exact 23-span warning manifest unchanged.
@@ -92,7 +99,7 @@ its 23 existing warning spans are checked separately against the exact manifest
 in `tests/check-proofs.sh`. A new, moved, or stale location fails the gate. The
 safe proofs check, but no Cubical transport-computation claim is made for those
 indexed eliminations, including `Kripke.Belief.believed`. The policy gate also
-compares all 25 source modules, 19 rejection fixtures, and four integration
+compares all 31 source modules, 24 rejection fixtures, and four integration
 witnesses with exact path manifests; rejects additional `OPTIONS` pragmas, proof
 escape hatches, and non-core imports; and verifies a generated negative
 control: `--safe` must reject a planted postulate with Agda's expected
@@ -254,10 +261,10 @@ external runtime or an unlisted mathematical correspondence.
 | Documentary comparison only; no imported owning definition
 
 | C-1
-| Every one of the 19 intended-invalid constructions is rejected for its
+| All 24 intended-invalid constructions are rejected for their
   enumerated semantic type mismatch. This is negative-control evidence, not a
   positive theorem.
-| TESTED
+| TESTED — local receipt 2026-11-07; five new valid prefixes also accepted
 | `tests/check-rejections.sh`, `tests/reject/*.agda`
 
 | C-2
@@ -294,6 +301,29 @@ external runtime or an unlisted mathematical correspondence.
 | PROVEN — local receipt 2026-11-07
 | `PartialRecovery.agda`; link:docs/partial-recovery.adoc[exact assumptions]
 
+| QR-1
+| Query recovery implies fibre constancy; an explicit image decision and
+  constancy construct a decoder. Success-to-image evidence supplies the
+  converse image decision; compatible-source query agreement follows from
+  adequacy. Universal extraction without that evidence would decide every Set.
+| PROVEN — local receipt 2026-11-07
+| `QueryRecovery.agda`, `QueryRecoveryExamples.agda`
+
+| OS-1
+| For generated pairs and a supplied result observer/source relation,
+  noninterference is equivalent by implications to release invariance.
+  Transparent full recovery forces related sources equal. Arbitrary visible
+  requests can have different success statuses; this is not private leakage.
+| PROVEN — local receipt 2026-11-07
+| `ObserverSafety.agda`, `ObserverSafetyExamples.agda`
+
+| RS-1
+| Total residue simulation relative to visible data is a preorder. The query
+  residue is adequate and least among residues admitting total Migration for
+  that query. Stronger residue preserves adequacy. No bit/cost bound follows.
+| PROVEN — local receipt 2026-11-07
+| `ResidueSufficiency.agda`, `ResidueSufficiencyExamples.agda`
+
 | C-4
 | The local retained-pair image is definitionally canonical `Echo` of the
   retained-pair function. Conversions preserve the source and equality path;
diff --git a/README.adoc b/README.adoc
index 4442495..9f43af7 100644
--- a/README.adoc
+++ b/README.adoc
@@ -9,6 +9,10 @@ image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www
 
 Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge, belief, and warrant, with proof transport sound relative to an explicit claim meaning.
 
+The link:docs/query-recovery.adoc[query-recovery extension] distinguishes answering
+a query from recovering its source, states observer safety for generated inputs,
+and characterises sufficient residue relative to already visible information.
+
 == Overview
 
 When an agent observes a fact, the type of their access matters. Knowledge is factive; belief is not. A warrant records evidence without assuming soundness. Proof transported across a boundary becomes a receipt; a receiving proof requires a successful sound check of the receiver's claim meaning.
@@ -228,7 +232,7 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
 
 [source,bash]
 ----
-just check  # policy guard + 25 positive modules + 19 expected rejections + 4 mutation controls
+just check  # policy guard + 31 positive modules + 24 expected rejections + 4 mutation controls
 ----
 
 `just check` calls `scripts/check.sh`: it uses a local `agda` when one is on
diff --git a/docs/query-recovery.adoc b/docs/query-recovery.adoc
new file mode 100644
index 0000000..db66c60
--- /dev/null
+++ b/docs/query-recovery.adoc
@@ -0,0 +1,124 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Query recovery, observer safety and sufficient residue
+:revdate: 2026-11-07
+
+This extension distinguishes answering a query from recovering its entire
+source. It reuses `Retention`, `Migration`, and the existing partial-recovery
+image. All carriers are `Set`; image witnesses remain proof-relevant and
+untruncated. No choice, automatic image decision, quotient, proof irrelevance,
+function extensionality or runtime secrecy property is assumed.
+
+== Query-relative recovery
+
+`QueryRecovery C q` has a pair-only `answer : B -> R -> Maybe T` and an
+adequacy law: every generated pair answers `just (q x)`. The decoder does not
+receive a source, `Case`, or consistency witness as input. Off-image behaviour
+is unconstrained by this law.
+
+[cols="1,3",options="header"]
+|===
+|Declaration in `QueryRecovery.agda` |Exact obligation/result
+|`queryConstant`, `queryComplete`
+|An adequate query agrees on every retained-pair fibre and answers any supplied
+image witness's query correctly. This does not implement a search for that witness.
+|`sourceToQuery`, `identityQueryToSource`
+|Full-source partial recovery answers every supplied query. An identity-query
+decoder recovers the source. General query recovery is weaker.
+|`migrationToQuery`, `queryToMigration`
+|Total Migration gives query recovery; an explicit target fallback totalizes a
+query decoder. The fallback is target data, not a source or an assumed inhabitant.
+|`successfulQueryAgrees`
+|Success agrees with the query of any compatible source, by adequacy alone.
+|`QuerySuccessSound`
+|The additional obligation supplies an actual image witness for each success.
+An extra query-equality field would be redundant by the preceding theorem.
+|`soundQueryDecidesImage`
+|This additional success obligation yields an explicit image decision. Failure
+refutes every image witness using adequacy.
+|`fromQueryImageDecision`, `queryImageDecisionSound`
+|Constancy on fibres plus an explicit image decision constructs a query decoder
+with the additional success obligation. These are constructive implications,
+not equalities of functions, records or proof fields.
+|===
+
+`QueryRecoveryExamples.agda` recovers a nonconstant first-bit query while the
+second bit is lost, and proves that full-source recovery is impossible for
+the same retention. A constant query needs no image decision and can succeed
+off-image, so success alone supplies no compatible source. The stronger
+`unrestrictedExtractionDecidesEveryType` is a constructive reduction: an
+extractor from arbitrary query recovery to image decision would decide every
+small type. It does not postulate that extractor or claim a formal independence
+theorem. The finite off-image example alone would not prove undecidability.
+
+== Observer safety
+
+`ObserverSafety.agda` defines `ObservationNI` for an explicit deterministic
+observer of the entire `Maybe T` result, on generated retained pairs and a
+supplied source relation. No equivalence laws for that relation are assumed.
+`releaseInvariantToNI` and `niToReleaseInvariant` relate this property to
+invariance of the observed released query. A transparent result observer forces
+equal query values; a transparent full-source result forces related sources to
+be equal. `hiddenPairForcesQueryAgreement` separately requires equality of the
+actual visible/residue pair; equal visible projections alone do not suffice.
+
+The positive example retains a second bit privately and publishes only the
+first bit of the recovered source. That public observation respects the
+first-bit source relation. Publishing both bits violates it. This is a theorem
+about the explicit result observer, not a claim that the raw input pair, logs,
+timing, memory, certificates or private residue are inaccessible at runtime.
+
+The arbitrary-request example distinguishes a generated request's success from
+an unreachable request's failure even for a constant query. The two requests
+are caller-selected and visible. This demonstrates the limit of the
+generated-input theorem; it is not itself a private-source confidentiality
+breach. A security theorem for arbitrary requests needs its own relation and
+observation contract. Neither this result nor the separate Secret Types
+fuelled-outcome counterexample establishes probabilistic or cryptographic secrecy.
+
+== Residue sufficiency
+
+`RelativeReduction f r s` means that an explicit total simulator reconstructs
+`r x` from `(f x, s x)`. Its law holds on generated inputs. Reflexivity and
+transitivity give a semantic preorder relative to the already visible `f`.
+
+`queryResidueAdequate` shows that retaining the query itself is sufficient.
+`queryResidueLeast` turns any adequate total Migration into a reduction from
+its residue to that query; `reductionToMigration` provides the converse field
+construction. Thus the query residue is least sufficient in this stated
+preorder. `migrateWithMoreResidue` preserves adequacy when additional residue
+can simulate the old one.
+
+`replaceResidue` uses a trivial certificate to expose the capability result;
+it does not transport the original certificate or claim authenticity.
+The examples show mutually simulating single and duplicate Boolean encodings,
+and that a unit residue can suffice when the visible value already supplies
+the answer but fails when visibility is constant. No minimum bit count, byte
+layout, time, cost, unique carrier, or partial-map preorder follows. Query
+minimality here is a factorization statement, not a new compression theorem.
+
+== Validation and ownership
+
+The complete four-entrypoint gate passed locally with Agda 2.6.4.3 on
+2026-11-07: `tests/check-policy.sh`, `tests/check-proofs.sh`,
+`tests/check-rejections.sh`, and `tests/check-approval-seal-mutations.sh`.
+These are the entrypoints composed by `bash scripts/check.sh`. They checked
+31 source modules, 24 intended semantic rejections, five new valid-prefix
+controls, and the existing four mutation controls.
+The existing exact 23-span warning allowance is unchanged. The four canonical
+Echo integration modules and their source pins are unchanged; their historical
+receipts remain in `partial-recovery.adoc`.
+
+The source and gates were copied byte-for-byte to an isolated ext4 directory
+because WSL startup and the mounted workspace were intermittent. A persistent
+WSL session completed the checks. The missing diagnostic matcher was supplied
+by a user-local extraction of Debian's authenticated `ripgrep=14.1.1-1+b4`
+package; no substitute matcher or warning exception was used. Local logs,
+compiler/tool hashes and source hashes are retained under `_build/`.
+Hosted checks and any later sibling adapters have separate receipts.
+
+These constructions are standard deterministic constructive factorization
+arguments packaged into the owning Epistemic API. The independent source
+review identified and removed a redundant success premise and narrowed the
+arbitrary-request example's claim. Compilation and source review are distinct.
+No new sibling adapter or complete Secret Types semantics bridge is claimed.
+Ordinal work remains excluded.
diff --git a/src/EpistemicTypes/All.agda b/src/EpistemicTypes/All.agda
index 332fc5c..f8fc032 100644
--- a/src/EpistemicTypes/All.agda
+++ b/src/EpistemicTypes/All.agda
@@ -13,6 +13,12 @@ import EpistemicTypes.Kripke.Dependence
 open import EpistemicTypes.EchoBridge public
 import EpistemicTypes.PartialRecovery
 import EpistemicTypes.PartialRecoveryExamples
+import EpistemicTypes.QueryRecovery
+import EpistemicTypes.QueryRecoveryExamples
+import EpistemicTypes.ObserverSafety
+import EpistemicTypes.ObserverSafetyExamples
+import EpistemicTypes.ResidueSufficiency
+import EpistemicTypes.ResidueSufficiencyExamples
 -- Imported (checked) but NOT re-exported publicly: ReadConsistency keeps
 -- its own self-contained ⊥/¬_ (matching the Examples.agda convention),
 -- which would clash with Examples' identically-named helpers if both were
diff --git a/src/EpistemicTypes/ObserverSafety.agda b/src/EpistemicTypes/ObserverSafety.agda
new file mode 100644
index 0000000..27728de
--- /dev/null
+++ b/src/EpistemicTypes/ObserverSafety.agda
@@ -0,0 +1,71 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module EpistemicTypes.ObserverSafety where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (Maybe; just)
+open import EpistemicTypes.EchoBridge using (Retention)
+open import EpistemicTypes.PartialRecovery using (retainedPair; withDefault)
+open import EpistemicTypes.QueryRecovery using (QueryRecovery; queryConstant)
+
+private
+  sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x
+  sym refl = refl
+
+  trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
+  trans refl p = p
+
+  cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
+  cong f refl = refl
+
+-- An explicit deterministic observation of the whole Maybe result, including
+-- success/failure if see exposes it. These results concern GENERATED inputs.
+-- E is a supplied relation; no unproved equivalence laws are silently assumed.
+ObservationNI : {A B R T O : Set} {C : Retention A B R} {q : A -> T} ->
+  QueryRecovery C q -> (Maybe T -> O) -> (A -> A -> Set) -> Set
+ObservationNI {C = C} rec see E = ∀ {x z} -> E x z ->
+  see (QueryRecovery.answer rec (Retention.observe C x) (Retention.retain C x)) ≡
+  see (QueryRecovery.answer rec (Retention.observe C z) (Retention.retain C z))
+
+ReleaseInvariant : {A T O : Set} -> (A -> T) -> (Maybe T -> O) ->
+  (A -> A -> Set) -> Set
+ReleaseInvariant q see E = ∀ {x z} -> E x z -> see (just (q x)) ≡ see (just (q z))
+
+releaseInvariantToNI : {A B R T O : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (see : Maybe T -> O) (E : A -> A -> Set) ->
+  ReleaseInvariant q see E -> ObservationNI rec see E
+releaseInvariantToNI rec see E invariant {x} {z} related =
+  trans (cong see (QueryRecovery.adequate rec x))
+    (trans (invariant related) (sym (cong see (QueryRecovery.adequate rec z))))
+
+niToReleaseInvariant : {A B R T O : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (see : Maybe T -> O) (E : A -> A -> Set) ->
+  ObservationNI rec see E -> ReleaseInvariant q see E
+niToReleaseInvariant rec see E invariant {x} {z} related =
+  trans (sym (cong see (QueryRecovery.adequate rec x)))
+    (trans (invariant related) (cong see (QueryRecovery.adequate rec z)))
+
+-- When the whole answer is visible, related sources must have equal queries.
+transparentNIForcesQueryAgreement : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (E : A -> A -> Set) ->
+  ObservationNI rec (λ result -> result) E -> ∀ {x z} -> E x z -> q x ≡ q z
+transparentNIForcesQueryAgreement {q = q} rec E ni {x} related =
+  cong (withDefault (q x)) (niToReleaseInvariant rec (λ result -> result) E ni related)
+
+-- Taking the query to be the whole source rules out hiding a genuinely
+-- distinct related pair from an observer who sees that recovered source.
+fullRecoveryNIForcesEquality : {A B R : Set} {C : Retention A B R}
+  (rec : QueryRecovery C (λ x -> x)) (E : A -> A -> Set) ->
+  ObservationNI rec (λ result -> result) E -> ∀ {x z} -> E x z -> x ≡ z
+fullRecoveryNIForcesEquality = transparentNIForcesQueryAgreement
+
+-- A separate INPUT-side assumption: if the actual pair hides a relation,
+-- every adequate query must respect it. A private residue need not satisfy
+-- this assumption merely because the visible projection does.
+hiddenPairForcesQueryAgreement : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) (E : A -> A -> Set) ->
+  (∀ {x z} -> E x z -> retainedPair C x ≡ retainedPair C z) ->
+  ∀ {x z} -> E x z -> q x ≡ q z
+hiddenPairForcesQueryAgreement rec E hides related = queryConstant rec (hides related)
diff --git a/src/EpistemicTypes/ObserverSafetyExamples.agda b/src/EpistemicTypes/ObserverSafetyExamples.agda
new file mode 100644
index 0000000..1def04e
--- /dev/null
+++ b/src/EpistemicTypes/ObserverSafetyExamples.agda
@@ -0,0 +1,73 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module EpistemicTypes.ObserverSafetyExamples where
+
+open import Agda.Builtin.Bool using (Bool; false; true)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (Maybe; just; nothing)
+open import Agda.Builtin.Sigma using (_,_; fst; snd)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.EchoBridge using (Retention; Impossible)
+open import EpistemicTypes.PartialRecoveryExamples using (finiteRetention; finiteImageDecision)
+open import EpistemicTypes.QueryRecovery
+open import EpistemicTypes.QueryRecoveryExamples using (Pair)
+open import EpistemicTypes.ObserverSafety
+
+private
+  cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
+  cong f refl = refl
+
+-- The second bit is privately retained. Publishing only the first bit of
+-- the recovered result respects low equivalence; publishing both does not.
+privateRetention : Retention Pair Bool Bool
+Retention.observe privateRetention = fst
+Retention.retain privateRetention = snd
+Retention.Cert privateRetention _ _ = ⊤
+Retention.sound privateRetention _ = tt
+
+privateRecovery : QueryRecovery privateRetention (λ x -> x)
+QueryRecovery.answer privateRecovery b secret = just (b , secret)
+QueryRecovery.adequate privateRecovery (b , secret) = refl
+
+LowRelated : Pair -> Pair -> Set
+LowRelated x z = fst x ≡ fst z
+
+redactedNI : ObservationNI privateRecovery (mapMaybe fst) LowRelated
+redactedNI {x} {z} related = releaseInvariantToNI privateRecovery (mapMaybe fst) LowRelated
+  (λ {u} {v} same -> cong just same) {x} {z} related
+
+transparentResult : Pair -> Maybe Pair
+transparentResult x = QueryRecovery.answer privateRecovery (fst x) (snd x)
+
+transparentLeak : transparentResult (false , false) ≡ transparentResult (false , true) -> Impossible
+transparentLeak ()
+
+noTransparentNI : ObservationNI privateRecovery (λ result -> result) LowRelated -> Impossible
+noTransparentNI ni = transparentLeak (ni {false , false} {false , true} refl)
+
+-- Even a constant query can have different statuses on ARBITRARY requests.
+-- Here the second request bit selects an unreachable input, rather than a
+-- generated pair. This does not contradict generated-input noninterference.
+-- Both requests are caller-selected and visible: this example alone is NOT
+-- leakage of a private source or a two-run confidentiality counterexample.
+guardedConstant : QueryRecovery finiteRetention (λ _ -> tt)
+guardedConstant = fromQueryImageDecision {C = finiteRetention} {q = λ _ -> tt}
+  (λ _ -> refl) finiteImageDecision
+
+generatedConstantNI : ObservationNI guardedConstant (λ result -> result) (λ _ _ -> ⊤)
+generatedConstantNI {x} {z} related = releaseInvariantToNI guardedConstant (λ result -> result)
+  (λ _ _ -> ⊤) (λ {u} {v} _ -> refl) {x} {z} related
+
+requestResult : Bool -> Maybe ⊤
+requestResult b = QueryRecovery.answer guardedConstant (false , b) tt
+
+reachableRequest : requestResult false ≡ just tt
+reachableRequest = refl
+
+unreachableRequest : requestResult true ≡ nothing
+unreachableRequest = refl
+
+requestStatusDifference : requestResult false ≡ requestResult true -> Impossible
+requestStatusDifference ()
diff --git a/src/EpistemicTypes/QueryRecovery.agda b/src/EpistemicTypes/QueryRecovery.agda
new file mode 100644
index 0000000..6b5ef6c
--- /dev/null
+++ b/src/EpistemicTypes/QueryRecovery.agda
@@ -0,0 +1,128 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module EpistemicTypes.QueryRecovery where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (Maybe; just; nothing)
+open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd)
+open import EpistemicTypes.EchoBridge using (Retention; Migration; Impossible)
+open import EpistemicTypes.PartialRecovery
+  using (PartialRecovery; Image; ImageDecision; Decision; yes; no; retainedPair; withDefault)
+
+private
+  sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x
+  sym refl = refl
+
+  trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
+  trans refl p = p
+
+  cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
+  cong f refl = refl
+
+  justInjective : {A : Set} {x y : A} -> just x ≡ just y -> x ≡ y
+  justInjective {x = x} = cong (withDefault x)
+
+  nothingNotJust : {A : Set} {x : A} -> nothing ≡ just x -> Impossible
+  nothingNotJust ()
+
+  eliminate : {A : Set} -> Impossible -> A
+  eliminate ()
+
+mapMaybe : {A T : Set} -> (A -> T) -> Maybe A -> Maybe T
+mapMaybe q nothing = nothing
+mapMaybe q (just x) = just (q x)
+
+-- The answer consumes ONLY a visible/residue pair, never a Case or source
+-- witness. Correctness constrains generated inputs; off-image behaviour is
+-- deliberately separate. The target may forget distinctions in the source.
+record QueryRecovery {A B R T : Set} (C : Retention A B R) (q : A -> T) : Set where
+  field
+    answer : B -> R -> Maybe T
+    adequate : (x : A) ->
+      answer (Retention.observe C x) (Retention.retain C x) ≡ just (q x)
+
+QueryConstant : {A B R T : Set} -> Retention A B R -> (A -> T) -> Set
+QueryConstant C q = ∀ {x z} -> retainedPair C x ≡ retainedPair C z -> q x ≡ q z
+
+queryConstant : {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  QueryRecovery C q -> QueryConstant C q
+queryConstant rec {x} {z} same = justInjective
+  (trans (sym (QueryRecovery.adequate rec x))
+    (trans (cong (λ pair -> QueryRecovery.answer rec (fst pair) (snd pair)) same)
+      (QueryRecovery.adequate rec z)))
+
+queryComplete : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) {y : B} {r : R} (w : Image C y r) ->
+  QueryRecovery.answer rec y r ≡ just (q (fst w))
+queryComplete rec (x , same) =
+  trans (sym (cong (λ p -> QueryRecovery.answer rec (fst p) (snd p)) same))
+    (QueryRecovery.adequate rec x)
+
+sourceToQuery : {A B R T : Set} {C : Retention A B R} (q : A -> T) ->
+  PartialRecovery C -> QueryRecovery C q
+QueryRecovery.answer (sourceToQuery q rec) y r = mapMaybe q (PartialRecovery.decode rec y r)
+QueryRecovery.adequate (sourceToQuery q rec) x =
+  cong (mapMaybe q) (PartialRecovery.roundtrip rec x)
+
+identityQueryToSource : {A B R : Set} {C : Retention A B R} ->
+  QueryRecovery C (λ x -> x) -> PartialRecovery C
+PartialRecovery.decode (identityQueryToSource rec) = QueryRecovery.answer rec
+PartialRecovery.roundtrip (identityQueryToSource rec) = QueryRecovery.adequate rec
+
+migrationToQuery : {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  Migration C q -> QueryRecovery C q
+QueryRecovery.answer (migrationToQuery m) y r = just (Migration.migrate m y r)
+QueryRecovery.adequate (migrationToQuery m) x = cong just (Migration.adequate m x)
+
+-- This fallback is explicit target data, not a source witness or choice axiom.
+queryToMigration : {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  T -> QueryRecovery C q -> Migration C q
+Migration.migrate (queryToMigration fallback rec) y r =
+  withDefault fallback (QueryRecovery.answer rec y r)
+Migration.adequate (queryToMigration fallback rec) x =
+  cong (withDefault fallback) (QueryRecovery.adequate rec x)
+
+-- Agreement with ANY supplied source witness follows from adequacy alone.
+successfulQueryAgrees : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) {y : B} {r : R} {t : T} ->
+  QueryRecovery.answer rec y r ≡ just t -> (w : Image C y r) -> q (fst w) ≡ t
+successfulQueryAgrees rec success w =
+  justInjective (trans (sym (queryComplete rec w)) success)
+
+-- The additional success obligation is precisely an actual image witness.
+-- No query-equality field is needed: successfulQueryAgrees derives it.
+-- Agreement with sources IF any exist does not justify the converse.
+QuerySuccessSound : {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  QueryRecovery C q -> Set
+QuerySuccessSound {B = B} {R = R} {T = T} {C = C} {q = q} rec =
+  (y : B) (r : R) (t : T) -> QueryRecovery.answer rec y r ≡ just t -> Image C y r
+
+soundQueryDecidesImage : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (rec : QueryRecovery C q) -> QuerySuccessSound rec -> ImageDecision C
+soundQueryDecidesImage rec sound y r with QueryRecovery.answer rec y r in result
+... | just t = yes (sound y r t result)
+... | nothing = no (λ w -> nothingNotJust (trans (sym result) (queryComplete rec w)))
+
+private
+  queryValue : {A B R T : Set} {C : Retention A B R} (q : A -> T) {y : B} {r : R} ->
+    Decision (Image C y r) -> Maybe T
+  queryValue q (yes (x , _)) = just (q x)
+  queryValue q (no _) = nothing
+
+fromQueryImageDecision : {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  QueryConstant C q -> ImageDecision C -> QueryRecovery C q
+QueryRecovery.answer (fromQueryImageDecision {C = C} {q = q} constant decide) y r =
+  queryValue {C = C} q (decide y r)
+QueryRecovery.adequate (fromQueryImageDecision {C = C} constant decide) x
+  with decide (Retention.observe C x) (Retention.retain C x)
+... | yes (z , same) = cong just (constant same)
+... | no absent = eliminate (absent (x , refl))
+
+queryImageDecisionSound : {A B R T : Set} {C : Retention A B R} {q : A -> T}
+  (constant : QueryConstant C q) (decide : ImageDecision C) ->
+  QuerySuccessSound (fromQueryImageDecision {C = C} {q = q} constant decide)
+queryImageDecisionSound constant decide y r t success with decide y r
+... | yes (x , same) = x , same
+... | no absent = eliminate (nothingNotJust success)
diff --git a/src/EpistemicTypes/QueryRecoveryExamples.agda b/src/EpistemicTypes/QueryRecoveryExamples.agda
new file mode 100644
index 0000000..7120df9
--- /dev/null
+++ b/src/EpistemicTypes/QueryRecoveryExamples.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module EpistemicTypes.QueryRecoveryExamples where
+
+open import Agda.Builtin.Bool using (Bool; false; true)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (just)
+open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.EchoBridge using (Retention; Impossible)
+open import EpistemicTypes.PartialRecovery
+  using (PartialRecovery; partialSeparates; ImageDecision; Decision; yes; no)
+open import EpistemicTypes.PartialRecoveryExamples
+  using (finiteRetention; finiteImageDecision; offImageIncompatible)
+open import EpistemicTypes.QueryRecovery
+
+private
+  cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
+  cong f refl = refl
+
+  falseNotTrue : false ≡ true -> Impossible
+  falseNotTrue ()
+
+-- A nonconstant public query remains recoverable despite a source collision.
+Pair : Set
+Pair = Σ Bool (λ _ -> Bool)
+
+publicRetention : Retention Pair Bool ⊤
+Retention.observe publicRetention = fst
+Retention.retain publicRetention _ = tt
+Retention.Cert publicRetention _ _ = ⊤
+Retention.sound publicRetention _ = tt
+
+publicQueryConstant : QueryConstant publicRetention fst
+publicQueryConstant same = cong fst same
+
+publicImage : ImageDecision publicRetention
+publicImage b tt = yes ((b , false) , refl)
+
+publicQuery : QueryRecovery publicRetention fst
+publicQuery = fromQueryImageDecision {C = publicRetention} {q = fst}
+  (λ {x} {z} -> publicQueryConstant {x} {z}) publicImage
+
+publicQuerySound : QuerySuccessSound publicQuery
+publicQuerySound = queryImageDecisionSound {C = publicRetention} {q = fst}
+  (λ {x} {z} -> publicQueryConstant {x} {z}) publicImage
+
+publicQueryTrue : QueryRecovery.answer publicQuery true tt ≡ just true
+publicQueryTrue = refl
+
+noFullPublicRecovery : PartialRecovery publicRetention -> Impossible
+noFullPublicRecovery rec = falseNotTrue
+  (cong snd (partialSeparates rec {false , false} {false , true} refl))
+
+-- For ANY retention a constant query can be answered with no image decision.
+constantQuery : {A B R : Set} (C : Retention A B R) -> QueryRecovery C (λ _ -> tt)
+QueryRecovery.answer (constantQuery C) _ _ = just tt
+QueryRecovery.adequate (constantQuery C) _ = refl
+
+constantOffImage : QueryRecovery.answer (constantQuery finiteRetention) (false , true) tt ≡ just tt
+constantOffImage = refl
+
+constantNotSuccessSound : QuerySuccessSound (constantQuery finiteRetention) -> Impossible
+constantNotSuccessSound sound with sound (false , true) tt tt refl
+... | b , same = falseNotTrue (cong (λ p -> snd (fst p)) same)
+
+-- This is a constructive REDUCTION, not an assumed decision principle or
+-- an undecidability theorem: unrestricted extraction would decide every P.
+propositionRetention : (P : Set) -> Retention P ⊤ ⊤
+Retention.observe (propositionRetention P) _ = tt
+Retention.retain (propositionRetention P) _ = tt
+Retention.Cert (propositionRetention P) _ _ = ⊤
+Retention.sound (propositionRetention P) _ = tt
+
+UniversalQueryImageExtraction : Set₁
+UniversalQueryImageExtraction =
+  {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  QueryRecovery C q -> ImageDecision C
+
+unrestrictedExtractionDecidesEveryType : UniversalQueryImageExtraction ->
+  (P : Set) -> Decision P
+unrestrictedExtractionDecidesEveryType extract P
+  with extract (constantQuery (propositionRetention P)) tt tt
+... | yes (p , _) = yes p
+... | no absent = no (λ p -> absent (p , refl))
diff --git a/src/EpistemicTypes/ResidueSufficiency.agda b/src/EpistemicTypes/ResidueSufficiency.agda
new file mode 100644
index 0000000..ff69f87
--- /dev/null
+++ b/src/EpistemicTypes/ResidueSufficiency.agda
@@ -0,0 +1,72 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module EpistemicTypes.ResidueSufficiency where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.EchoBridge using (Retention; Migration)
+
+private
+  trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
+  trans refl p = p
+
+  cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
+  cong f refl = refl
+
+-- r is no more informative than s RELATIVE TO the already visible f.
+-- A total simulator is explicit; its law is only on generated inputs.
+-- This is a semantic preorder, with no byte/cost/uniqueness assertion.
+record RelativeReduction {A B R S : Set} (f : A -> B)
+  (r : A -> R) (s : A -> S) : Set where
+  field
+    reduce : B -> S -> R
+    realizes : (x : A) -> reduce (f x) (s x) ≡ r x
+
+relativeRefl : {A B R : Set} {f : A -> B} {r : A -> R} -> RelativeReduction f r r
+RelativeReduction.reduce relativeRefl _ v = v
+RelativeReduction.realizes relativeRefl _ = refl
+
+relativeTrans : {A B R S T : Set} {f : A -> B} {r : A -> R} {s : A -> S} {t : A -> T} ->
+  RelativeReduction f r s -> RelativeReduction f s t -> RelativeReduction f r t
+RelativeReduction.reduce (relativeTrans rs st) b v =
+  RelativeReduction.reduce rs b (RelativeReduction.reduce st b v)
+RelativeReduction.realizes (relativeTrans {f = f} rs st) x =
+  trans (cong (RelativeReduction.reduce rs (f x)) (RelativeReduction.realizes st x))
+    (RelativeReduction.realizes rs x)
+
+-- This creates an observation/retention contract with a trivial certificate.
+-- It does not transport an old Cert or confer any authentication guarantee.
+replaceResidue : {A B R S : Set} -> Retention A B R -> (A -> S) -> Retention A B S
+Retention.observe (replaceResidue C s) = Retention.observe C
+Retention.retain (replaceResidue C s) = s
+Retention.Cert (replaceResidue C s) _ _ = ⊤
+Retention.sound (replaceResidue C s) _ = tt
+
+queryResidueAdequate : {A B R T : Set} (C : Retention A B R) (q : A -> T) ->
+  Migration (replaceResidue C q) q
+Migration.migrate (queryResidueAdequate C q) _ t = t
+Migration.adequate (queryResidueAdequate C q) _ = refl
+
+-- The query residue itself is least among residues sufficient for this
+-- total Migration contract. This packages factorization, not compression.
+queryResidueLeast : {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  Migration C q -> RelativeReduction (Retention.observe C) q (Retention.retain C)
+RelativeReduction.reduce (queryResidueLeast m) = Migration.migrate m
+RelativeReduction.realizes (queryResidueLeast m) = Migration.adequate m
+
+reductionToMigration : {A B R T : Set} {C : Retention A B R} {q : A -> T} ->
+  RelativeReduction (Retention.observe C) q (Retention.retain C) -> Migration C q
+Migration.migrate (reductionToMigration r) = RelativeReduction.reduce r
+Migration.adequate (reductionToMigration r) = RelativeReduction.realizes r
+
+-- Strengthening available residue preserves any already adequate query.
+migrateWithMoreResidue : {A B R S T : Set} {C : Retention A B R} {q : A -> T}
+  (s : A -> S) -> RelativeReduction (Retention.observe C) (Retention.retain C) s ->
+  Migration C q -> Migration (replaceResidue C s) q
+Migration.migrate (migrateWithMoreResidue s reduction m) b v =
+  Migration.migrate m b (RelativeReduction.reduce reduction b v)
+Migration.adequate (migrateWithMoreResidue {C = C} s reduction m) x =
+  trans (cong (Migration.migrate m (Retention.observe C x)) (RelativeReduction.realizes reduction x))
+    (Migration.adequate m x)
diff --git a/src/EpistemicTypes/ResidueSufficiencyExamples.agda b/src/EpistemicTypes/ResidueSufficiencyExamples.agda
new file mode 100644
index 0000000..fbe8f6b
--- /dev/null
+++ b/src/EpistemicTypes/ResidueSufficiencyExamples.agda
@@ -0,0 +1,52 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module EpistemicTypes.ResidueSufficiencyExamples where
+
+open import Agda.Builtin.Bool using (Bool; false; true)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Sigma using (Σ; _,_; fst)
+open import Agda.Builtin.Unit using (⊤; tt)
+open import EpistemicTypes.EchoBridge using (Impossible)
+open import EpistemicTypes.ResidueSufficiency
+
+private
+  sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x
+  sym refl = refl
+
+  trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
+  trans refl p = p
+
+  falseNotTrue : false ≡ true -> Impossible
+  falseNotTrue ()
+
+silent : Bool -> ⊤
+silent _ = tt
+
+duplicate : Bool -> Σ Bool (λ _ -> Bool)
+duplicate b = b , b
+
+singleFromDuplicate : RelativeReduction silent (λ b -> b) duplicate
+RelativeReduction.reduce singleFromDuplicate _ = fst
+RelativeReduction.realizes singleFromDuplicate _ = refl
+
+duplicateFromSingle : RelativeReduction silent duplicate (λ b -> b)
+RelativeReduction.reduce duplicateFromSingle _ b = duplicate b
+RelativeReduction.realizes duplicateFromSingle _ = refl
+
+-- Mutual semantic simulation does not make the carriers/encodings identical.
+-- No machine representation or bit cost is defined by these declarations.
+singleRoundtrip : RelativeReduction silent (λ b -> b) (λ b -> b)
+singleRoundtrip = relativeTrans singleFromDuplicate duplicateFromSingle
+
+-- Visible information matters: the identity visible value makes a unit
+-- residue adequate, while the same unit residue with silent visibility fails.
+visibleSuppliesBit : RelativeReduction (λ b -> b) (λ b -> b) silent
+RelativeReduction.reduce visibleSuppliesBit b _ = b
+RelativeReduction.realizes visibleSuppliesBit _ = refl
+
+silentCannotSupplyBit : RelativeReduction silent (λ b -> b) silent -> Impossible
+silentCannotSupplyBit reduction = falseNotTrue
+  (trans (sym (RelativeReduction.realizes reduction false))
+    (RelativeReduction.realizes reduction true))
diff --git a/tests/check-policy.sh b/tests/check-policy.sh
index 27f28f0..e3929b7 100755
--- a/tests/check-policy.sh
+++ b/tests/check-policy.sh
@@ -25,11 +25,17 @@ expected_source_modules=(
   src/EpistemicTypes/Kripke/Frame.agda
   src/EpistemicTypes/Kripke/Indexed.agda
   src/EpistemicTypes/Kripke/Residual.agda
+  src/EpistemicTypes/ObserverSafety.agda
+  src/EpistemicTypes/ObserverSafetyExamples.agda
   src/EpistemicTypes/PartialRecovery.agda
   src/EpistemicTypes/PartialRecoveryExamples.agda
   src/EpistemicTypes/ProofTransport.agda
   src/EpistemicTypes/ProofTransportExample.agda
+  src/EpistemicTypes/QueryRecovery.agda
+  src/EpistemicTypes/QueryRecoveryExamples.agda
   src/EpistemicTypes/ReadConsistency.agda
+  src/EpistemicTypes/ResidueSufficiency.agda
+  src/EpistemicTypes/ResidueSufficiencyExamples.agda
   src/EpistemicTypes/SurrealBridge.agda
   src/EpistemicTypes/Warrant.agda
 )
@@ -42,11 +48,16 @@ expected_rejection_fixtures=(
   tests/reject/FinalStateProvesNoTouch.agda
   tests/reject/ForgedAcceptance.agda
   tests/reject/ForgedResidue.agda
+  tests/reject/ForgetfulResidueSufficient.agda
   tests/reject/ForkedHistory.agda
   tests/reject/InventedMigration.agda
   tests/reject/LyingVerifier.agda
   tests/reject/MismatchedSource.agda
+  tests/reject/ObserverRevealsSecret.agda
+  tests/reject/OffImageStatusHidden.agda
   tests/reject/PartialSuccessProvesImage.agda
+  tests/reject/QueryIgnoresCollision.agda
+  tests/reject/QuerySuccessInventsSource.agda
   tests/reject/ReplayedArtifact.agda
   tests/reject/ReplayedHolder.agda
   tests/reject/ResealApprovesChange.agda
diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh
index 984014b..e05871c 100644
--- a/tests/check-rejections.sh
+++ b/tests/check-rejections.sh
@@ -8,11 +8,34 @@ fixtures=(LyingVerifier ForgedAcceptance ReplayedArtifact ReplayedHolder \
   StaleSample FakeFreshness ForkedHistory ForgedResidue MismatchedSource \
   UnderstatedBound InventedMigration UncheckedSkip BeliefIsKnowledge \
   AgentChangesAnchor FinalStateProvesNoTouch ResealApprovesChange RestoreErasesHistory \
-  CollidingPartialRecovery PartialSuccessProvesImage)
+  CollidingPartialRecovery PartialSuccessProvesImage \
+  QueryIgnoresCollision QuerySuccessInventsSource ObserverRevealsSecret \
+  OffImageStatusHidden ForgetfulResidueSufficient)
 expected_files=$(printf 'tests/reject/%s.agda\n' "${fixtures[@]}" | sort)
 actual_files=$(rg --files tests/reject -g '*.agda' | sort)
 [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; }
+prefix_dir=$(mktemp -d)
+trap 'rm -rf "$prefix_dir"' EXIT
 for fixture in "${fixtures[@]}"; do
+  case "$fixture" in
+    QueryIgnoresCollision|QuerySuccessInventsSource|ObserverRevealsSecret|OffImageStatusHidden|ForgetfulResidueSufficient)
+      [[ $(rg -c '^-- EXPECTED-REJECTION$' "tests/reject/$fixture.agda") == 1 ]] || {
+        printf 'FAIL: %s must have exactly one rejection boundary\n' "$fixture"
+        exit 1
+      }
+      awk '/^-- EXPECTED-REJECTION$/ {exit} {print}' "tests/reject/$fixture.agda" > "$prefix_dir/$fixture.agda"
+      status=0
+      diagnostic=$(agda --no-libraries --safe --without-K --cubical-compatible \
+        --exact-split --no-sized-types --no-guardedness --double-check --ignore-interfaces \
+        -W error -W noUnsupportedIndexedMatch -i src -i "$prefix_dir" \
+        "$prefix_dir/$fixture.agda" 2>&1) || status=$?
+      if [[ $status -ne 0 ]]; then
+        printf 'FAIL: %s valid prefix failed (exit %s)\n%s\n' "$fixture" "$status" "$diagnostic"
+        exit 1
+      fi
+      printf 'PASS: %s valid prefix accepted\n' "$fixture"
+      ;;
+  esac
   status=0
   # Source warning locations are audited by check-proofs.sh; this suppression
   # only lets each negative fixture reach the exact mismatch asserted below.
@@ -39,6 +62,8 @@ for fixture in "${fixtures[@]}"; do
     FinalStateProvesNoTouch) expected='true != .*false' ;;
     ResealApprovesChange|RestoreErasesHistory) expected='sealBroken != .*accepted' ;;
     CollidingPartialRecovery|PartialSuccessProvesImage) expected='false != .*true' ;;
+    QueryIgnoresCollision|QuerySuccessInventsSource|ObserverRevealsSecret|ForgetfulResidueSufficient) expected='false != .*true' ;;
+    OffImageStatusHidden) expected='just tt != nothing' ;;
   esac
   if [[ "$status" -ne 42 ]] || ! rg -q "$expected" <<< "$diagnostic" || \
       ! rg -q 'when checking' <<< "$diagnostic"; then
diff --git a/tests/reject/ForgetfulResidueSufficient.agda b/tests/reject/ForgetfulResidueSufficient.agda
new file mode 100644
index 0000000..202a928
--- /dev/null
+++ b/tests/reject/ForgetfulResidueSufficient.agda
@@ -0,0 +1,19 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module ForgetfulResidueSufficient where
+
+open import Agda.Builtin.Bool using (false; true)
+open import Agda.Builtin.Equality using (refl)
+open import EpistemicTypes.ResidueSufficiency using (RelativeReduction)
+open import EpistemicTypes.ResidueSufficiencyExamples using (silent; visibleSuppliesBit)
+
+control : RelativeReduction (λ b -> b) (λ b -> b) silent
+control = visibleSuppliesBit
+
+-- EXPECTED-REJECTION
+forged : RelativeReduction silent (λ b -> b) silent
+RelativeReduction.reduce forged _ _ = false
+RelativeReduction.realizes forged false = refl
+RelativeReduction.realizes forged true = refl
diff --git a/tests/reject/ObserverRevealsSecret.agda b/tests/reject/ObserverRevealsSecret.agda
new file mode 100644
index 0000000..50fdc50
--- /dev/null
+++ b/tests/reject/ObserverRevealsSecret.agda
@@ -0,0 +1,19 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module ObserverRevealsSecret where
+
+open import Agda.Builtin.Bool using (false; true)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Sigma using (_,_; fst)
+open import EpistemicTypes.QueryRecovery using (mapMaybe)
+open import EpistemicTypes.ObserverSafetyExamples using (transparentResult)
+
+control : mapMaybe fst (transparentResult (false , false)) ≡
+          mapMaybe fst (transparentResult (false , true))
+control = refl
+
+-- EXPECTED-REJECTION
+forged : transparentResult (false , false) ≡ transparentResult (false , true)
+forged = refl
diff --git a/tests/reject/OffImageStatusHidden.agda b/tests/reject/OffImageStatusHidden.agda
new file mode 100644
index 0000000..3b8f517
--- /dev/null
+++ b/tests/reject/OffImageStatusHidden.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module OffImageStatusHidden where
+
+open import Agda.Builtin.Bool using (false; true)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (just; nothing)
+open import Agda.Builtin.Unit using (tt)
+open import EpistemicTypes.ObserverSafetyExamples using (requestResult)
+
+reachable : requestResult false ≡ just tt
+reachable = refl
+
+unreachable : requestResult true ≡ nothing
+unreachable = refl
+
+-- EXPECTED-REJECTION
+-- Distinct caller-selected requests; this is not a private-source NI claim.
+forged : requestResult false ≡ requestResult true
+forged = refl
diff --git a/tests/reject/QueryIgnoresCollision.agda b/tests/reject/QueryIgnoresCollision.agda
new file mode 100644
index 0000000..756e226
--- /dev/null
+++ b/tests/reject/QueryIgnoresCollision.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module QueryIgnoresCollision where
+
+open import Agda.Builtin.Bool using (false; true)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (just)
+open import Agda.Builtin.Sigma using (_,_; snd)
+open import Agda.Builtin.Unit using (tt)
+open import EpistemicTypes.QueryRecovery using (QueryRecovery)
+open import EpistemicTypes.QueryRecoveryExamples using (publicRetention; publicQuery)
+
+control : QueryRecovery.answer publicQuery true tt ≡ just true
+control = refl
+
+-- EXPECTED-REJECTION
+-- The second component cannot be recovered after the retention drops it.
+forged : QueryRecovery publicRetention snd
+QueryRecovery.answer forged _ _ = just false
+QueryRecovery.adequate forged (_ , true) = refl
+QueryRecovery.adequate forged (_ , false) = refl
diff --git a/tests/reject/QuerySuccessInventsSource.agda b/tests/reject/QuerySuccessInventsSource.agda
new file mode 100644
index 0000000..832297c
--- /dev/null
+++ b/tests/reject/QuerySuccessInventsSource.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module QuerySuccessInventsSource where
+
+open import Agda.Builtin.Bool using (false; true)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Maybe using (just)
+open import Agda.Builtin.Sigma using (_,_)
+open import Agda.Builtin.Unit using (tt)
+open import EpistemicTypes.PartialRecovery using (Image)
+open import EpistemicTypes.PartialRecoveryExamples using (finiteRetention)
+open import EpistemicTypes.QueryRecovery using (QueryRecovery)
+open import EpistemicTypes.QueryRecoveryExamples using (constantQuery)
+
+control : QueryRecovery.answer (constantQuery finiteRetention) (false , true) tt ≡ just tt
+control = refl
+
+-- EXPECTED-REJECTION
+-- A successful constant answer cannot invent a source for an off-image pair.
+forged : Image finiteRetention (false , true) tt
+forged = false , refl