docs(proofs): correct the float argument, fixture claims and receipt status

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,34 @@ 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), which
+  covers the current corpus; record that run here as the receipt. Every
+  theorem is `ungraded` under PROOF-POLICY §8 (no per-theorem PWG-3
+  receipt; no Rocq or Lean leg).
+* *Fixtures.* `ReplayedHolder` and `UnderstatedBound` fail on an index
+  mismatch (holder, budget), not on the property they are named for; the
+  positive `noSilentHolderTransport` and `noUnderstatedBound` carry that
+  evidence. C-1's "semantic type mismatch" holds for the error text, not
+  for every property named.
+* *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,11 +218,17 @@ 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.

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

@@ -71,8 +71,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/reject/ReplayedHolder.agda

@@ -5,5 +5,8 @@ open import EpistemicTypes.ProofTransportExample using (Bob; ArtifactIsTrue; mod
 open HolderBoundary using (module Local; aliceLocalProof)
 
 -- Holder-sensitive evidence cannot silently acquire a different holder.
+-- Audit 2026-11-09: this is rejected because `View` is indexed by holder,
+-- which would also reject it under a holder-independent `Meaning`; the
+-- holder-sensitivity evidence is the positive `noSilentHolderTransport`.
 replay : Local.View Bob true Local.Proof ArtifactIsTrue
 replay = aliceLocalProof

tests/reject/UnderstatedBound.agda

@@ -1,5 +1,8 @@
 {-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module UnderstatedBound where
+-- Audit 2026-11-09: this retypes `boundedTrue` (budget `finite 1`) at budget
+-- `finite 0`, so it fails on the budget index whatever the cost measure is.
+-- The bound check itself is shown by the positive `noUnderstatedBound`.
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Nat
 open import EpistemicTypes.EchoBridge