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

[arena-ai-coding-agent]

feat(applications): the RapidNJ Q-criterion as an application of the core

Adds an applications section, src/EpistemicTypes/Applications/, and uses the
RapidNJ per-row branch-and-bound rule as its first worked example. The point is
to show the core doing work on a claim that arrives with its own arithmetic,
rather than only on examples internal to the core.

The mapping

FactiveModality.reflect is the soundness map of the generated skip warrant,
and its proof is the bound lemma:

run data (numbers, cursor, suffix, verdict)
  -- skipWarrant ............-> Warrant κ "nothing skipped beats q(min)"
  -- skip-sound (qBound-≤-Q) -> SoundWarrant κ (same claim)
  -- reflect = sound-epi .....-> the claim itself

skip-known packages that chain: given the sorted-row invariant, the
running-maximum invariant and an accepted exact check, every entry of the
skipped quadrant is proved non-improving. Held without reflect, the same run
is belief (no-receipt-reflection). The same pipeline reproduces the runtime's
four readings of evidence (Factive / Belief / Collapsed / SansFibre),
matching EpistemicTypes.jl's epi_status.

What is in the tree

• OrderedGroup — the arithmetic budget: order laws, joint monotonicity,
  antitone negation, Nat-indexed scale.
• IntegerModel — ℤ as difference pairs, cross-multiplied order, all four
  laws, the ℤ-group witness, a decidable order.
• SortedRow — rows, both invariants, prefix/suffix composition.
• QCriterion — qBound = (r−2)·d_next − t_i − t_max and qBound-≤-Q, which
  uses only reflexivity, transitivity, monotonicity, antitonicity and scaling:
  no ring law, and no multiplication or division of carrier elements anywhere.
• RapidNJSkip — the Checkable seam, the generated warrant and its soundness,
  the factive and belief readings, and the declared-not-assumed cross-iteration
  obligation.
• RapidNJExamples — the executable integer check, a worked four-taxon scan
  discharged by computation, the no-always-true refutation, the status mirror.

Rational input is stated, not assumed

The bound never multiplies carrier elements, so ℚ-as-ordered-group suffices and
the only exactness seam is Checkable.decide-true. The integers are discharged
in full; the rational case is left as an explicit obligation with the
common-denominator rescaling argument written out (it needs three scaling laws
the record deliberately does not assume). Rounded arithmetic is excluded by
proof, not by convention.

Two latent defects this fixes

• tests/check-proofs.sh searched non-recursively, so any module in a
  subdirectory was silently ungated — it reported 11 modules while 13 existed.
  It now reports 17 (12 core + All + 5 new modules), which is the point of the
  gate.
• EchoBridge._≤ℕ_ had no fixity declaration, so it sat at level 20 and bound
  tighter than _+_. Declared at the definition site; a fixity declaration
  only, no definition changed.

One new rejection fixture (UncheckedSkip) refuses a recorded check the numbers
do not meet, so the manifest is twelve.

Evidence

Local, Agda 2.6.4.3: PASS: 17 source modules and 12/12 fixtures, under
--safe --without-K --double-check --ignore-interfaces -W error --no-libraries, no postulates, no holes. No standard library is used. Sibling
repos were checked and left alone: neither Protoctist.jl nor
MetaManifold-WebUI contains distance-matrix NJ code, so no coupling is
invented here.

Not claimed

Tree correctness for NJ/RapidNJ; the row-insertion update that maintains the
invariants; cross-iteration bound reuse; any rational instance; and the tighter
ERapidNJ/NINJA bounds. docs/applications/rapidnj-q-criterion.adoc lists these
as open obligations alongside the proof inventory.

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: f9ebe521-0473-4411-b538-f36570cf8cf2

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}