feat(applications): RapidNJ Q-criterion bound, generated skip warrants, ℤ instance

.machine_readable/descriptiles/STATE.a2ml

@@ -1,7 +1,7 @@
 [metadata]
 project = "epistemic-types"
 version = "0.1.0"
-last-updated = "2026-06-15"
+last-updated = "2026-09-27"
 status = "prototype"  # prototype | active | paused | archived
 
 [project-context]
@@ -29,6 +29,12 @@ aggregator = "src/EpistemicTypes/All.agda re-exports every module."
 # Agda modules under src/EpistemicTypes/.
 list = [
   "EpistemicTypes.Access",
+  "EpistemicTypes.Applications.IntegerModel",
+  "EpistemicTypes.Applications.OrderedGroup",
+  "EpistemicTypes.Applications.QCriterion",
+  "EpistemicTypes.Applications.RapidNJExamples",
+  "EpistemicTypes.Applications.RapidNJSkip",
+  "EpistemicTypes.Applications.SortedRow",
   "EpistemicTypes.All",
   "EpistemicTypes.Base",
   "EpistemicTypes.ContinuityExamples",
@@ -50,6 +56,12 @@ surreal-bridge = "SurrealAccess carrier + GradedSurrealModality + daySurrealAcce
 examples = "Worked instances exercising the interfaces."
 proof-transport = "proofSound derives Meaning holder artifact claim from an accepted sound checker. Receipts alone do not certify; transfer requires the target-holder meaning."
 proof-transport-example = "Boolean certificate checker with legitimate acceptance and refutations for false claims, changed artifacts and holder-sensitive replay."
+applications-ordered-group = "Minimal arithmetic budget for the applications layer: carrier with addition, negation, zero, order, reflexivity, transitivity, joint monotonicity and antitone negation; derived subtraction and Nat-indexed scaling."
+applications-integer-model = "The integers as difference pairs over Nat, with the cross-multiplied order, all four OrderedGroup laws, the instance 'ℤ-group', and a decision procedure for the order."
+applications-sorted-row = "Rows as entries (index, distance, row sum), the All predicate, membership, the sorted-row and running-maximum invariants, and prefix/suffix composition."
+applications-qcriterion = "Q and qBound over any OrderedGroup, the bound lemma qBound-≤-Q, the row lemma qBound-≤-suffix, claim weakening, and prefix/suffix composition."
+applications-rapidnj-skip = "Checkable (the exactness seam), scan state, skip evidence, the generated warrant and soundness map, the factive modality, the belief-only reading, and the declared-not-assumed cross-iteration obligation."
+applications-rapidnj-examples = "Executable integer check, refutation of an over-eager comparison, a worked four-taxon scan, and the runtime status mirror (Factive / Belief / Collapsed / SansFibre)."
 
 [route-to-mvp]
 milestones = [
@@ -59,6 +71,8 @@ milestones = [
   { name = "Concrete Kripke-style semantics", completion = 0 },
   { name = "Evidence-state and observation-rule examples", completion = 0 },
   { name = "Richer day-bounded surreal fragments as SurrealAccess instances", completion = 0 },
+  { name = "Applications layer: RapidNJ Q-criterion bound and skip warrants", completion = 100 },
+  { name = "Rational (ℚ) instance and the common-denominator rescaling transport", completion = 0 },
   { name = "Lawful instances (only after proving or explicitly assuming laws)", completion = 0 },
 ]
 
@@ -69,10 +83,12 @@ items = [
   "Add richer day-bounded surreal fragments as instances of the abstract SurrealAccess interface.",
   "Add lawful instances only after proving or explicitly assuming laws.",
   "Extend the echo bridge without importing a full graded comonad.",
+  "Add a rational carrier instance for the applications layer, or prove the common-denominator rescaling transport.",
+  "Model the row-insertion update that maintains the scan invariants, and cross-iteration bound reuse.",
 ]
 
 [progress-summary]
-note = "Prototype. The base interface and all eleven modules typecheck under 'just check' (Agda 2.6.4.3, --safe --without-K, --no-libraries, no postulates). The endofunctor/Modality formers, Warrant, Access transport, EchoBridge residue, SurrealBridge tower, ProofTransport, and its K9-SVC/A2ML attestation example are in place. Remaining work is semantics and lawful instances — see [roadmap]."
+note = "Prototype. The base interface and all seventeen modules typecheck under 'just check' (Agda 2.6.4.3, --safe --without-K, --no-libraries, no postulates), against twelve rejection fixtures. The endofunctor/Modality formers, Warrant, Access transport, EchoBridge residue, SurrealBridge tower, ProofTransport, its K9-SVC/A2ML attestation example, and the applications layer (RapidNJ Q-criterion bound, generated skip warrants, discharged integer instance) are in place. Remaining work is semantics, lawful instances, and the rational/rescaling obligation — see [roadmap]."
 
 [blockers-and-issues]
 # No active blockers.

AUDIT.adoc

@@ -18,9 +18,11 @@ The owner authorized proof/security CI and protected-main enforcement on
 billing incident are superseded. Existing GitHub workflows already run; their
 current proof coverage is extended by this change.
 
-* The eleven-module core is checked with Agda 2.6.4.3, safe mode, without-K,
-  internal double checking and warnings as errors. Each source module is checked.
-* Eleven deliberate rejection fixtures must fail for their intended type mismatch.
+* Every module under `src/EpistemicTypes/` -- seventeen at the time of writing,
+  including the applications layer -- is checked with Agda 2.6.4.3, safe mode,
+  without-K, internal double checking and warnings as errors. Each source
+  module is checked.
+* Twelve deliberate rejection fixtures must fail for their intended type mismatch.
 * Canonical Echo residue correspondence is checked against pinned sibling source.
 * CodeQL analyzes Actions workflows, and the shared scanner checks secrets.
 * Main receives changes through PRs with required proof/security checks. Signed

CHANGELOG.adoc

@@ -12,6 +12,29 @@ the changelog records what is actually proved, not what is aspired to.
 
 === https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD[Unreleased]
 
+[[added--2026-09-27]]
+==== Added — 2026-09-27
+
+* New applications section, `src/EpistemicTypes/Applications/`, with the
+  RapidNJ per-row Q-criterion bound as its first worked example:
+  `OrderedGroup` (minimal arithmetic budget), `IntegerModel` (the integers as
+  difference pairs, with all four laws and a decidable order), `SortedRow`
+  (rows, invariants, prefix/suffix composition), `QCriterion` (the bound lemma
+  `qBound-≤-Q` and the row and composition lemmas), `RapidNJSkip` (checkability
+  seam, generated warrant and soundness, the factive modality, and the belief
+  reading), and `RapidNJExamples` (the executable integer check, a worked scan,
+  a refutation of over-eager comparisons, and the runtime status mirror).
+* Skipping a matrix quadrant now *generates* a valid warrant whose soundness
+  map is proved from the bound; no soundness is assumed, and the bound consumes
+  no ring, multiplication or division laws. Rational input is an explicitly
+  stated obligation, documented in `docs/applications/rapidnj-q-criterion.adoc`.
+* New rejection fixture `UncheckedSkip`: a recorded check the numbers do not
+  meet is refused, so the rejection manifest is now twelve fixtures.
+* `EchoBridge`'s `_≤ℕ_` gained an `infix 4` declaration at its definition site.
+  A fixity declaration only; no definition changed.
+* New documentation: `docs/applications/rapidnj-q-criterion.adoc`, plus README,
+  documentation-index, proof-status and machine-readable state updates.
+
 [[fixed--2026-09-07]]
 ==== Fixed — 2026-09-07
 

EXPLAINME.adoc

@@ -91,6 +91,29 @@ claims. The theorem remains relative to the specified meaning and checker
 proof; it does not establish cryptography or physical facts. See
 link:docs/proof-transport.adoc[].
 
+=== Skipping a search quadrant generates a warrant, not an assumption
+
+How this is implemented::
+`src/EpistemicTypes/Applications/` formalizes the per-row bound RapidNJ uses
+when searching for the neighbour-joining minimum. `QCriterion.qBound-≤-Q`
+proves the bound over an arbitrary `OrderedGroup` using only monotonicity,
+antitonicity, transitivity and `Nat`-indexed scaling. `RapidNJSkip` turns a
+skip certificate (sorted-row invariant, running-maximum invariant, accepted
+exact check) into a `Warrant`, proves its soundness from the bound
+(`skip-known`), and instantiates `FactiveModality.reflect` with that soundness
+map; held without it, the same run is belief
+(`no-receipt-reflection`).
+
+Caveat::
+The rational case is a *stated obligation*, not a theorem. What is discharged
+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
+link:docs/applications/rapidnj-q-criterion.adoc[].
+
 == Dogfooded Across The Account
 
 [cols="1,2,2", options="header"]
@@ -112,6 +135,16 @@ link:docs/proof-transport.adoc[].
 
 == Known gaps
 
+[CAUTION]
+====
+**The applications layer has no rational instance yet.** The RapidNJ
+Q-criterion bound is proved order-generically and discharged for the integers;
+a rational carrier (or the common-denominator rescaling transport) is stated as
+an obligation in `docs/applications/rapidnj-q-criterion.adoc`, together with the
+row-insertion update and cross-iteration bound reuse.
+====
+
+
 [CAUTION]
 ====
 **No Kripke semantics.** The prototype defines the syntactic/type-theoretic interfaces for modalities but does not model them against a Kripke frame semantics. This is the largest open theoretical gap.

PROOF-STATUS.adoc

@@ -8,6 +8,35 @@ Verification status of the epistemic-types Agda formalisation. The whole library
 self-contained (`--no-libraries`: it imports only `Agda.Builtin.*` /
 `Agda.Primitive`). This records a reproduced `agda` run, not a "looks fine" reading.
 
+== Applications layer — 2026-09-27
+
+`src/EpistemicTypes/Applications/` adds the first worked application: the
+per-row Q-criterion bound used by RapidNJ when searching for the
+neighbour-joining minimum. Five modules and one example module pass the same
+gate (`--safe --without-K --no-libraries --double-check -W error`, no
+postulates):
+
+* `QCriterion.qBound-≤-Q` proves the row bound over an arbitrary
+  `OrderedGroup`, using only reflexivity, transitivity, monotone addition,
+  antitone negation and `Nat`-indexed scaling -- no ring law, no multiplication
+  or division of carrier elements.
+* `RapidNJSkip` generates a warrant from a skip certificate (sorted-row
+  invariant, running-maximum invariant, accepted exact check) and proves
+  `skip-known`: the skipped quadrant's entries cannot beat the incumbent. The
+  soundness map is `FactiveModality.reflect = sound-epi`; without it the same
+  run is belief (`no-receipt-reflection`).
+* `IntegerModel` discharges the arithmetic budget for the integers, and
+  `RapidNJExamples` turns `dec-≤ℤ` into a `Checkable`, runs a worked four-taxon
+  scan by computation, and refutes an over-eager comparison
+  (`no-always-true`).
+* One new rejection fixture (`UncheckedSkip`) refuses a recorded check that the
+  numbers do not meet.
+
+Not claimed: any rational (ℚ) instance, the rescaling transport from a rational
+matrix to its common-denominator integer form, the row-insertion update that
+maintains the invariants, and cross-iteration bound reuse. These are stated as
+obligations in link:docs/applications/rapidnj-q-criterion.adoc[].
+
 == Current continuity-foundations correction — 2026-09-07
 
 `ReadView` now entails equality with the indexed store contents. Cached-read
@@ -19,8 +48,9 @@ and migration have explicit obligations. The collision theorem refutes every
 migration requiring a distinction discarded by the retained pair. Resource
 bounds require measure inequalities; arbitrary grade retagging is removed.
 
-The eleven-module core and eleven deliberate rejection fixtures pass with
-Agda 2.6.4.3 under `--safe --without-K --no-libraries`, without warnings.
+The eleven-module core and eleven deliberate rejection fixtures (the counts at
+that date; `just check` now reports seventeen modules and twelve fixtures) pass
+with Agda 2.6.4.3 under `--safe --without-K --no-libraries`, without warnings.
 The additional canonical Echo integration proves both representation round
 trips and agreement of lowering; its standard-library dependencies emit Cubical
 compatibility warnings. See link:docs/continuity-foundations.adoc[] for commands,

README.adoc

@@ -98,6 +98,36 @@ See link:docs/continuity-foundations.adoc[the breaking API correction and proof
 boundaries]. An optional integration gate proves correspondence with the actual
 sibling `EchoResidue.EchoR`; the core remains dependency-free.
 
+== Applications: the RapidNJ Q-criterion
+
+The `Applications/` tree is where the core interfaces are exercised against
+algorithmic claims that arrive with their own arithmetic. Its first example is
+the per-row branch-and-bound rule used by RapidNJ (Simonsen, Mailund, Pedersen
+2008) when searching for the neighbour-joining minimum: while scanning a row of
+distances in increasing order, the row is abandoned as soon as
+
+    qBound = (r - 2) * d(i,next) - t(i) - t_max
+
+is at least the incumbent `q_min`, because no unexamined entry can beat it.
+
+The development is order-generic: `Applications.QCriterion.qBound-≤-Q` proves
+the bound for any carrier with monotone addition, antitone negation and a
+transitive order -- no multiplication or division of carrier elements occurs
+anywhere, and the coefficient `(r - 2)` enters only as a `Nat`-indexed repeated
+sum. A skip certificate carries the sorted-row invariant, the running-maximum
+invariant and an accepted executable check; `Applications.RapidNJSkip` then
+*generates* a warrant for the skipped quadrant, and its soundness map is
+exactly the `reflect` of a `FactiveModality`:
+
+    run data -> skipWarrant -> skip-sound (the bound lemma) -> reflect -> the claim
+
+So skipping a quadrant yields knowledge only through a proved bound, never by
+assumption, and the same run held without the soundness map is belief. The
+integer model is discharged in full (`Applications.IntegerModel`,
+`Applications.RapidNJExamples`); the rational case is a *stated* obligation, not
+a claim -- see link:docs/applications/rapidnj-q-criterion.adoc[the applications
+note] for the rescaling argument and the exact-arithmetic seam.
+
 == Proof transport across trust boundaries
 
 `ProofTransport` is parameterised by agents, claim labels, artefacts,
@@ -150,6 +180,10 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[
 | Proof transport with explicit semantic soundness
 | **Novel formalisation**
 | `EpistemicTypes.ProofTransport`
+
+| Order-generic RapidNJ Q-criterion bound and skip warrants
+| Transcription of a documented algorithm; no novelty theorem
+| `EpistemicTypes.Applications.QCriterion`
 |===
 
 == What remains intentionally unformalized
@@ -164,6 +198,10 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
 * Proof irrelevance or decidability
 * Global soundness of warrants
 * Monadic (`bind`) or comonadic (`extract`) structure for `E`
+* A rational (ℚ) instance of the applications layer, and the rescaling
+  transport that would lift the integer certificate to rational input
+* Cross-iteration reuse of a skip bound, and the row-insertion update that
+  maintains the scan invariants (`Applications.RapidNJSkip.WeakeningObligation`)
 
 == Build
 
@@ -184,6 +222,7 @@ agda --no-libraries -i src src/EpistemicTypes/All.agda
 * link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps
 * link:docs/continuity-foundations.adoc[Continuity foundations] — store coherence, retained information, bounds, and next obligations
 * link:docs/proof-transport.adoc[Proof transport] — semantic verification across boundaries
+* link:docs/applications/rapidnj-q-criterion.adoc[Applications: the RapidNJ Q-criterion] — the bound, the skip warrant, the exact-arithmetic obligation
 
 == License
 

docs/README.adoc

@@ -23,6 +23,12 @@ authority.
   endofunctor (map only) and *not* a monad/comonad, and what "epistemically
   available at standpoint κ" is meant to capture.
 
+| `docs/applications/rapidnj-q-criterion.adoc`
+| The applications layer: the RapidNJ per-row Q-criterion bound, the skip
+  certificate's three invariants, the warrant/soundness chain through
+  `FactiveModality.reflect`, and the exact-arithmetic (ℚ) obligation stated
+  rather than assumed.
+
 | `docs/proof-transport.adoc`
 | Focused walkthrough of `EpistemicTypes.ProofTransport`: how `transmit`
   downgrades a sender's `Proof` to a receiver's `Receipt`, how `verify` upgrades
@@ -64,9 +70,19 @@ The core lives in `src/EpistemicTypes/`. `All.agda` checks `Base`, `Warrant`,
 publicly re-exported to avoid helper-name collisions. Every core module uses
 `--safe --without-K` and builtins only. Local checks use Agda 2.6.4.3.
 
+The applications layer lives beside the core in `src/EpistemicTypes/Applications/`:
+`OrderedGroup` (the arithmetic budget), `IntegerModel` (the discharged
+instance), `SortedRow` (rows and invariants), `QCriterion` (the bound lemma),
+`RapidNJSkip` (warrants, soundness, the factive modality), and
+`RapidNJExamples` (the worked scan and the runtime status mirror). It is
+checked by the same recursive gate as the core, and it is imported -- not
+publicly re-exported -- by `All.agda`. See
+link:applications/rapidnj-q-criterion.adoc[].
+
 == Notes
 
 * `Echo C y`, `BoundedEcho C measure budget y`, and `E κ A` have separate roles.
-* `just check` runs the core proof graph and eleven semantic rejection fixtures.
+* `just check` runs the proof graph (seventeen modules, including the
+  applications layer) and twelve semantic rejection fixtures.
 * `just check-canonical` separately checks correspondence against actual sibling
   Echo sources; it requires an explicit standard-library source path.