Rejection fixtures: fail for the property they name

EXPLAINME.adoc

@@ -112,8 +112,11 @@ is the integer model: `IntegerModel` proves every law the bound consumes, and
 `RapidNJExamples` runs a worked scan by computation. Making rational input
 first-class needs either a rational carrier instance or the common-denominator
 rescaling transport; the bound itself never multiplies or divides carrier
-elements, so no field law is needed either way. Anything rounded cannot meet
-the `Checkable` reflection law, as `no-always-true` shows. See
+elements, so no field law is needed either way. Floating point is excluded
+because a Float64 carrier is not a model of the four `OrderedGroup` laws
+(NaN is not ordered, so `≤-refl` fails) and because the bound would be
+about float-computed Q, not exact Q. (`no-always-true` only refutes a
+comparison that always answers true; it says nothing about rounding.) See
 link:docs/applications/rapidnj-q-criterion.adoc[].
 
 == Dogfooded Across The Account

PROOF-STATUS.adoc

@@ -74,6 +74,40 @@ This document uses the estate proof-policy vocabulary:
   rechecked by this repository;
 * `OPEN` — not discharged.
 
+[NOTE]
+.Design and receipt audit (2026-11-09)
+====
+* *Receipts.* The "local receipt 2026-11-07" rows (C-1, C-3, C-4, PR-1,
+  PR-2, QR-1, OS-1, RS-1) cite logs and hashes kept under `_build/`, which
+  is gitignored, so those receipts cannot be retrieved from the repository.
+  Hosted Proof Safety passed on `main` at `dcd4648` (2026-11-07, run
+  42395802116). That run is historical evidence for the corpus at that
+  commit, including the earlier `ReplayedHolder` and `UnderstatedBound`
+  fixtures; it does not cover the rewritten fixtures, whose receipt is the
+  pinned-toolchain gate on the commit that carries them. Every
+  theorem is `ungraded` under PROOF-POLICY §8 (no per-theorem PWG-3
+  receipt; no Rocq or Lean leg).
+* *Fixtures.* `ReplayedHolder` and `UnderstatedBound` previously failed on an index
+  mismatch (holder, budget), not on the property they are named for; the
+  positive `noSilentHolderTransport` and `noUnderstatedBound` carry that
+  evidence. *Resolved 2026-11-09:* both fixtures now have an
+  `EXPECTED-REJECTION` boundary with a checked valid prefix. `ReplayedHolder`
+  fails at the checker's soundness obligation `Bob ≡ Alice` (the
+  holder-sensitive meaning), and `UnderstatedBound` fails at the `within`
+  obligation `1 ≤ 0`.
+* *Definitional results.* OS-1's equivalence holds for every decoder on
+  generated inputs (adequacy fixes the answer), and "noninterference" there
+  is a decoder-relative property, not information-flow noninterference,
+  which README lists as out of scope. RS-1's "least" holds by definition
+  (`Migration` and `RelativeReduction` have the same fields).
+  `status-of-skip-is-factive` is `refl` on a constant.
+* *C-2* round-trips with `EchoResidue.EchoR` (a certificate-carrying
+  residue), not with the canonical `Echo` fibre; the fibre correspondence
+  is C-4.
+* *Floating point.* The earlier argument that rounding is not monotone was
+  wrong; see `docs/applications/rapidnj-q-criterion.adoc`.
+====
+
 The separate cross-prover labels `AGDA-PENDING`, `AGDA-VERIFIED`,
 `COQ-CHECKED`, `LEAN-CHECKED`, `BRIDGE-PENDING`, and `RECONCILED` describe
 verification legs; they do not strengthen the proof-policy status.

docs/applications/rapidnj-q-criterion.adoc

@@ -218,14 +218,22 @@ and neither is claimed here:
   four group laws, plus the `Checkable` obligation. More proof work, same
   seam.
 
-*What is excluded.* Floating point. `Checkable.decide-true` is a reflection
-law, and rounded arithmetic does not satisfy it in general; the abstract
-obstruction is made precise by `RapidNJExamples.no-always-true`, which shows
-that a comparison answering `true` for every pair would prove that every
-integer is below every other. The practical rule for the runtime is therefore:
+*What is excluded.* Floating point. A Float64 carrier is not a model of the
+four `OrderedGroup` laws: NaN is unordered, so `≤-refl` fails. (The
+record does not ask for associativity, so non-associative float addition is
+not itself the obstruction.)
+The bound would also be about float-computed Q rather than exact Q. (An
+earlier version of this paragraph said rounding is not monotone and cited
+`RapidNJExamples.no-always-true`. Round-to-nearest *is* monotone, and
+`no-always-true` only shows that a comparison answering `true` for every
+pair would prove that every integer is below every other; it says nothing
+about rounding. Audit note 2026-11-09.) The practical rule for the runtime
+is therefore:
 the moment a rounding-tolerant `Float64` value participates in a *bound
 comparison*, the claim cannot be `:Factive`; record it as `:Belief` until an
-exact comparison decides it.
+exact comparison decides it. "Exact" means recomputed from the exact inputs
+(or bounded by a proved error term), not an exact comparison of values that
+were already rounded: `2^53 + 1` and `2^53` round to the same Float64.
 
 == What is proved, and what is not
 

src/EpistemicTypes/Applications/OrderedGroup.agda

@@ -29,9 +29,10 @@
 --
 --  * Any model of these four laws certifies the bound, so the bound does not
 --    depend on the *representation* of rationals, only on exactness.
---  * A Float64 implementation does not satisfy `≤-⊕`: rounding is not
---    monotone for every pair of operands, so `x ≤ y` can hold while
---    `x + z > y + z` holds under rounding.  That is the seam documented in
+--  * A Float64 implementation is not a model of these laws: NaN is not
+--    ordered, so `≤-refl` fails at NaN (round-to-nearest itself is
+--    monotone; corrected 2026-11-09).  The bound would also be about
+--    float-computed Q, not exact Q.  That is the seam documented in
 --    link:docs/applications/rapidnj-q-criterion.adoc[], and the reason the
 --    reflection lemma in `RapidNJSkip` is the single non-negotiable
 --    obligation of an executable implementation.

src/EpistemicTypes/Applications/RapidNJSkip.agda

@@ -22,8 +22,9 @@
 -- arithmetic fact consumed is the order-monotonicity budget of
 -- `OrderedGroup` (no ring identities, hence no ℚ-specific law).  The
 -- resulting knowledge is therefore valid in any exact model, and an
--- implementation whose arithmetic is not exact fails at exactly one place:
--- supplying `Checkable` (see the Float64 seam in
+-- implementation whose arithmetic is not exact fails in two places: it is
+-- not a model of `OrderedGroup` (IEEE order is not reflexive at NaN), and its
+-- comparison is not a sound `Checkable` for exact Q (see the Float64 seam in
 -- link:docs/applications/rapidnj-q-criterion.adoc[]).
 --
 -- The same run, held without a soundness map, is belief: `Epi` packages a
@@ -71,8 +72,8 @@ module Skip (G : OrderedGroup) where
   -- A decision procedure whose `true` verdicts *reflect* the order.  This is
   -- the single seam between the proof and a running program: an
   -- implementation with exact arithmetic (integers, or rationals with
-  -- cross-multiplied comparisons) can supply it; one with rounding cannot,
-  -- because rounding is not monotone for every pair of operands.
+  -- cross-multiplied comparisons) can supply it; a Float64 one is excluded
+  -- because Float64 is not a model of the OrderedGroup laws (2026-11-09).
   record Checkable : Set₁ where
     field
       decide      : (x y : Carrier) -> Bool

tests/check-rejections.sh

@@ -18,7 +18,7 @@ prefix_dir=$(mktemp -d)
 trap 'rm -rf "$prefix_dir"' EXIT
 for fixture in "${fixtures[@]}"; do
   case "$fixture" in
-    QueryIgnoresCollision|QuerySuccessInventsSource|ObserverRevealsSecret|OffImageStatusHidden|ForgetfulResidueSufficient)
+    QueryIgnoresCollision|QuerySuccessInventsSource|ObserverRevealsSecret|OffImageStatusHidden|ForgetfulResidueSufficient|ReplayedHolder|UnderstatedBound)
       [[ $(rg -c '^-- EXPECTED-REJECTION$' "tests/reject/$fixture.agda") == 1 ]] || {
         printf 'FAIL: %s must have exactly one rejection boundary\n' "$fixture"
         exit 1
@@ -51,11 +51,11 @@ for fixture in "${fixtures[@]}"; do
   case "$fixture" in
     LyingVerifier|ForgedAcceptance) expected='false != .*true' ;;
     ReplayedArtifact) expected='true != .*false' ;;
-    ReplayedHolder) expected='Alice != .*Bob' ;;
+    ReplayedHolder) expected='Bob != .*Alice' ;;
     StaleSample|ForkedHistory|ForgedResidue|MismatchedSource) expected='false != .*true' ;;
     UncheckedSkip) expected='false != .*true' ;;
     FakeFreshness) expected='initial .*false !=' ;;
-    UnderstatedBound) expected='1 != 0' ;;
+    UnderstatedBound) expected='suc _[^ ]* != zero of type Nat' ;;
     InventedMigration) expected='true != .*false' ;;
     BeliefIsKnowledge) expected='w₁ != .*w₀' ;;
     AgentChangesAnchor) expected='0 != 1' ;;

tests/reject/ReplayedHolder.agda

@@ -1,9 +1,18 @@
 {-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ReplayedHolder where
 open import Agda.Builtin.Bool using (true)
+open import Agda.Builtin.Equality using (refl)
 open import EpistemicTypes.ProofTransportExample using (Bob; ArtifactIsTrue; module HolderBoundary)
-open HolderBoundary using (module Local; aliceLocalProof)
+open HolderBoundary using (module Local)
 
--- Holder-sensitive evidence cannot silently acquire a different holder.
-replay : Local.View Bob true Local.Proof ArtifactIsTrue
-replay = aliceLocalProof
+-- Holder-sensitive evidence cannot be re-certified for a different holder.
+-- `LocalMeaning holder _ _` is `holder ≡ Alice`.  The forgery below
+-- replays Alice's accepting checker with Bob as the holder; it fails
+-- exactly at the checker's soundness obligation, `Bob ≡ Alice`.  Under a
+-- holder-independent meaning the same term would type-check, so the
+-- rejection is evidence about the meaning, not about the `View` index.
+-- (Rewritten 2026-11-09; the earlier fixture failed on the index alone.)
+
+-- EXPECTED-REJECTION
+bobCheck : Local.CertificateCheck Bob true ArtifactIsTrue
+bobCheck = Local.certificateCheck (λ _ -> true) (λ _ _ -> refl)

tests/reject/UnderstatedBound.agda

@@ -1,9 +1,18 @@
 {-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module UnderstatedBound where
-open import Agda.Builtin.Bool
 open import Agda.Builtin.Nat
+open import Agda.Builtin.Bool
 open import EpistemicTypes.EchoBridge
 import EpistemicTypes.ContinuityExamples as Examples
-open Examples.Residues using (identityRetention; constantCost; boundedTrue)
+open Examples.Residues using (identityRetention; constantCost; identityTrue)
+
+-- A bounded echo must prove its cost is within the budget.  The residue
+-- costs `finite 1`; the forgery claims budget `finite 0` and supplies the
+-- proof that worked for budget `finite 1`.  It fails at the `within`
+-- obligation, `1 ≤ 0`, not at an index.  (Rewritten 2026-11-09; the
+-- earlier fixture retyped a finished value and failed on the budget
+-- index whatever the cost measure was.)
+
+-- EXPECTED-REJECTION
 forged : BoundedEcho identityRetention constantCost (finite zero) true
-forged = boundedTrue
+forged = bounded identityTrue (finite≤ (suc≤ zero≤))