From ca45767ad1b2c3613d94142eab93e74a12377c4a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:29:09 +0000 Subject: [PATCH 1/4] docs(proofs): correct the float argument, fixture claims and receipt status MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A statement-level review (2026-11-09) compared the ledger and docs with the Agda. This commit changes comments, ledger and doc text only; no proof term changes. - The floating-point exclusion argument was wrong: round-to-nearest is monotone, and no-always-true only refutes an always-true comparison. Float64 is excluded because it is not a model of the OrderedGroup laws (non-associative +, unordered NaN) and because the bound would be about float-computed Q. Corrected in EXPLAINME, the RapidNJ doc, OrderedGroup and RapidNJSkip comments. - ReplayedHolder and UnderstatedBound fail on an index mismatch, not on the property they are named for; their headers now say so and point to the positive theorems that carry that evidence. - PROOF-STATUS gains an audit note: the 2026-11-07 local receipts live under the gitignored _build/ and cannot be retrieved (hosted Proof Safety on dcd4648 is the receipt to record); OS-1 and RS-1 are partly definitional; C-2 round-trips with EchoR, not the Echo fibre; every theorem is `ungraded` under PROOF-POLICY §8. Checked: tests/check-proofs.sh (31 modules, 23 warning spans unchanged), tests/check-rejections.sh and tests/check-policy.sh pass on Agda 2.7.0.1 (CI pins 2.6.4.3). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- EXPLAINME.adoc | 7 +++-- PROOF-STATUS.adoc | 28 +++++++++++++++++++ docs/applications/rapidnj-q-criterion.adoc | 14 ++++++---- .../Applications/OrderedGroup.agda | 6 ++-- .../Applications/RapidNJSkip.agda | 4 +-- tests/reject/ReplayedHolder.agda | 3 ++ tests/reject/UnderstatedBound.agda | 3 ++ 7 files changed, 53 insertions(+), 12 deletions(-) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index d8d6a1b..8a15a78 100644 --- a/EXPLAINME.adoc +++ b/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 +(`+` is not associative, NaN is not ordered) 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 diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 0e662ba..7296e48 100644 --- a/PROOF-STATUS.adoc +++ b/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. diff --git a/docs/applications/rapidnj-q-criterion.adoc b/docs/applications/rapidnj-q-criterion.adoc index ea8d17b..a7e7920 100644 --- a/docs/applications/rapidnj-q-criterion.adoc +++ b/docs/applications/rapidnj-q-criterion.adoc @@ -218,11 +218,15 @@ 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: addition is not associative and NaN is unordered. +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. diff --git a/src/EpistemicTypes/Applications/OrderedGroup.agda b/src/EpistemicTypes/Applications/OrderedGroup.agda index 40f4cd3..1645a77 100644 --- a/src/EpistemicTypes/Applications/OrderedGroup.agda +++ b/src/EpistemicTypes/Applications/OrderedGroup.agda @@ -29,9 +29,9 @@ -- -- * 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: `+` is not +-- associative and NaN is unordered (round-to-nearest itself is +-- monotone; corrected 2026-11-09). 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. diff --git a/src/EpistemicTypes/Applications/RapidNJSkip.agda b/src/EpistemicTypes/Applications/RapidNJSkip.agda index 1e01e59..167de6a 100644 --- a/src/EpistemicTypes/Applications/RapidNJSkip.agda +++ b/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 diff --git a/tests/reject/ReplayedHolder.agda b/tests/reject/ReplayedHolder.agda index ac63a0a..972408b 100644 --- a/tests/reject/ReplayedHolder.agda +++ b/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 diff --git a/tests/reject/UnderstatedBound.agda b/tests/reject/UnderstatedBound.agda index f1cf084..d21c53f 100644 --- a/tests/reject/UnderstatedBound.agda +++ b/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 From 2f2bf1f92872360605cc39e8ab38f1a662fc0128 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:04:39 +0000 Subject: [PATCH 2/4] docs: drop associativity from the Float64 exclusion MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit OrderedGroup does not ask for associativity, so non-associative float addition is not why Float64 fails to be a model. The obstruction is that NaN is unordered, so ≤-refl fails. Corrects OrderedGroup.agda, EXPLAINME.adoc and the RapidNJ Q-criterion note. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- EXPLAINME.adoc | 2 +- docs/applications/rapidnj-q-criterion.adoc | 4 +++- src/EpistemicTypes/Applications/OrderedGroup.agda | 7 ++++--- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 8a15a78..0a2c422 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -114,7 +114,7 @@ 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. Floating point is excluded because a Float64 carrier is not a model of the four `OrderedGroup` laws -(`+` is not associative, NaN is not ordered) and because the bound would be +(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[]. diff --git a/docs/applications/rapidnj-q-criterion.adoc b/docs/applications/rapidnj-q-criterion.adoc index a7e7920..541acce 100644 --- a/docs/applications/rapidnj-q-criterion.adoc +++ b/docs/applications/rapidnj-q-criterion.adoc @@ -219,7 +219,9 @@ and neither is claimed here: seam. *What is excluded.* Floating point. A Float64 carrier is not a model of the -four `OrderedGroup` laws: addition is not associative and NaN is unordered. +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 diff --git a/src/EpistemicTypes/Applications/OrderedGroup.agda b/src/EpistemicTypes/Applications/OrderedGroup.agda index 1645a77..b03dde9 100644 --- a/src/EpistemicTypes/Applications/OrderedGroup.agda +++ b/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 is not a model of these laws: `+` is not --- associative and NaN is unordered (round-to-nearest itself is --- monotone; corrected 2026-11-09). 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. From 5778d4b16b276eb46261777469e3809fd5089d25 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:26:08 +0000 Subject: [PATCH 3/4] tests(reject): make two fixtures fail for the property they name MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ReplayedHolder and UnderstatedBound failed on an index mismatch (holder, budget) that would reject them whatever the meaning or cost measure (2026-11-09 audit). Both now carry an EXPECTED-REJECTION boundary with a checked valid prefix: - ReplayedHolder re-certifies Alice's accepting checker for Bob and fails at its soundness obligation `Bob ≡ Alice`, the holder-sensitive meaning. Under a holder-independent meaning the same term would type-check. - UnderstatedBound builds a bounded echo at budget finite 0 with the proof that fits finite 1 and fails at the `within` obligation `1 ≤ 0`. check-rejections.sh checks both prefixes and matches the new diagnostics; PROOF-STATUS records the resolution. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- PROOF-STATUS.adoc | 7 +++++-- tests/check-rejections.sh | 6 +++--- tests/reject/ReplayedHolder.agda | 20 +++++++++++++------- tests/reject/UnderstatedBound.agda | 18 ++++++++++++------ 4 files changed, 33 insertions(+), 18 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 7296e48..f4169be 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -87,8 +87,11 @@ This document uses the estate proof-policy vocabulary: * *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. + 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, diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh index e05871c..b9ff4b0 100644 --- a/tests/check-rejections.sh +++ b/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' ;; diff --git a/tests/reject/ReplayedHolder.agda b/tests/reject/ReplayedHolder.agda index 972408b..4ba36d5 100644 --- a/tests/reject/ReplayedHolder.agda +++ b/tests/reject/ReplayedHolder.agda @@ -1,12 +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. --- 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 +-- 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) diff --git a/tests/reject/UnderstatedBound.agda b/tests/reject/UnderstatedBound.agda index d21c53f..c0c48f1 100644 --- a/tests/reject/UnderstatedBound.agda +++ b/tests/reject/UnderstatedBound.agda @@ -1,12 +1,18 @@ {-# 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 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≤)) From f9866096aa732162c8a86ce2a246ed31a4ac5a3f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:07:05 +0000 Subject: [PATCH 4/4] docs: receipt scope, Float64 overview, exact-comparison rule Review on epistemic-types#53: - PROOF-STATUS: run 42395802116 at dcd4648 is historical evidence for the earlier fixtures, not for the rewritten ones; the index-mismatch sentence is now in the past tense. - RapidNJSkip overview: inexact arithmetic fails in two places (not an OrderedGroup model, NaN; not a sound Checkable for exact Q), matching the later comment and OrderedGroup.agda. - rapidnj-q-criterion: an "exact comparison" must use values recomputed from exact inputs or bounded by a proved error term. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- PROOF-STATUS.adoc | 9 ++++++--- docs/applications/rapidnj-q-criterion.adoc | 4 +++- src/EpistemicTypes/Applications/RapidNJSkip.agda | 5 +++-- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index f4169be..864b13e 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -80,11 +80,14 @@ This document uses the estate proof-policy vocabulary: * *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 + 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` fail on an index +* *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 diff --git a/docs/applications/rapidnj-q-criterion.adoc b/docs/applications/rapidnj-q-criterion.adoc index 541acce..f513263 100644 --- a/docs/applications/rapidnj-q-criterion.adoc +++ b/docs/applications/rapidnj-q-criterion.adoc @@ -231,7 +231,9 @@ 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 diff --git a/src/EpistemicTypes/Applications/RapidNJSkip.agda b/src/EpistemicTypes/Applications/RapidNJSkip.agda index 167de6a..ca700d5 100644 --- a/src/EpistemicTypes/Applications/RapidNJSkip.agda +++ b/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