docs: add RapidNJ K-CUT application target

.machine_readable/6a2/STATE.a2ml

@@ -145,5 +145,22 @@ title = "State K-CUT-LOSS as the first Agda signature, against [ResourceAlgebra
 status = "open"
 priority = "high"
 
+# ---- Application proof targets (added after pre-registration) ----
+
+[[application-targets]]
+id = "app-rapidnj-002"
+name = "two-thread RapidNJ K-CUT-LOSS square"
+status = "OPEN TARGET (not a proof; application note only)"
+frontier = "two selected events e1/e2 with Independent₂ witness"
+minimum-lemma = "localGrade p (localStep p e2 (localStep p e1 (project p s))) ≡ transportLoss p (globalGrade (step e2 (step e1 s)))"
+prerequisite = "canonical state diamond for disjoint read/write footprints"
+non-claim = "Does not assert upstream RapidNJ exposes this batch interface; does not address K-CUT-WARRANT"
+
+[[application-targets]]
+id = "app-rapidnj-001"
+name = "two-thread RapidNJ canonical state diamond"
+status = "OPEN TARGET (algorithmic prerequisite, not K-CUT)"
+statement = "step e2 (step e1 s) ~= step e1 (step e2 s) under Independent₂"
+
 [blockers]
 note = "K-CUT cannot be typed until the repo is git-init'd + licensed by the owner. Everything below na-001 waits on that."

EXPLAINME-new.adoc

@@ -16,11 +16,16 @@ ____
 A global choreographic type G is read as a partial causal order. It is projected to local types (endpoint projection), where each edge is graded by an echo loss-grade and an epistemic standpoint-warrant.
 ____
 
-How this is implemented::
-`link:src/ChoreographicTypes/[]` defines `GlobalType`, the partial causal order structure, the grading by `EchoGrade` (imported from `echo-types`) and `EpiGrade` (imported from `epistemic-types`), and the `EndpointProjection` mapping.
+How this is intended to be implemented::
+The planned `link:src/ChoreographicTypes/[]` tree will define `GlobalType`, the
+partial causal order structure, the grading by `EchoGrade` (imported from
+`echo-types`) and `EpiGrade` (imported from `epistemic-types`), and the
+`EndpointProjection` mapping.
 
 Caveat::
-The definitions are present. The deep integration — proving that the grading laws hold under the projection mapping in the general case — is the content of K-CUT, which is open.
+The current checkout does not contain the planned `src/` tree. The deep
+integration — proving that the grading laws hold under the projection mapping
+in the general case — remains the open K-CUT problem.
 
 === K-CUT-LOSS holds as equality
 
@@ -29,8 +34,10 @@ ____
 K-CUT-LOSS: Grading commutes with projection as an equality. Loss is type-determined.
 ____
 
-How this is implemented::
-The statement of K-CUT-LOSS is formalised in this repo. The *only* existing proof is the degenerate single-static-edge base case in `echo-types` (`RoleGraded.choreo-grade-commute`). No proof for general cuts exists here.
+How this is intended to be implemented::
+The K-CUT-LOSS statement is a planned Agda target for this repo. The *only*
+existing proof is the degenerate single-static-edge base case in `echo-types`
+(`RoleGraded.choreo-grade-commute`). No proof for general cuts exists here.
 
 Caveat::
 **This is an open conjecture, not a theorem.** The base case suggests it is likely true, but compositionality across arbitrary antichains is unproved. This is the hardest open problem in the repo.
@@ -42,12 +49,26 @@ ____
 K-CUT-WARRANT: Warrant transport commutes with projection only as a bound, and only under a SoundWarrant side-condition. The type upper-bounds discoverability but cannot determine it.
 ____
 
-How this is implemented::
-The statement of K-CUT-WARRANT is formalised here, importing `SoundWarrant` from `epistemic-types`. No proof exists, not even a base case.
+How this is intended to be implemented::
+The K-CUT-WARRANT statement is a planned Agda target, importing
+`SoundWarrant` from `epistemic-types`. No proof exists, not even a base case.
 
 Caveat::
 **This is an open conjecture.** The directionality (bound, not equality) reflects the epistemic reality: an agent's local knowledge may exceed the type's requirements, so projection can only upper-bound the warrant, not determine it. This is the formal reflection of the `BeliefModality` / non-factive design in `epistemic-types`.
 
+=== The RapidNJ application isolates the first non-degenerate target
+
+[quote, applications/rapidnj-two-thread.adoc]
+____
+The smallest non-degenerate K-CUT lemma is a two-event loss-grade commuting square for a disjoint antichain frontier.
+____
+
+How this is implemented::
+`link:applications/rapidnj-two-thread.adoc[]` defines the application boundary and records the target in `link:applications/rapidnj-two-thread.agda[]`. The target names global and local reduction steps, projection, loss grading, transport, and an `Independent₂` witness. `Independent₂` is deliberately stronger than antichain membership: it must cover read/write disjointness, phase safety, and deterministic tie handling.
+
+Caveat::
+The accompanying Agda file contains open interfaces and postulated target signatures so that the proof obligation has a stable shape. It is not imported into the build and proves nothing. The RapidNJ state diamond (serialising two independent updates in either order) is an algorithmic prerequisite, separate from K-CUT-LOSS. No claim is made about the upstream implementation exposing this exact batch interface.
+
 === The tropical resource-dioid is re-proved in-site
 
 [quote, README.adoc]
@@ -94,7 +115,12 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4
 
 [CAUTION]
 ====
-**No non-degenerate compositionality.** The repo currently defines the objects (global types, projections, grades, cuts) but does not compose them. All composition theorems are deferred pending K-CUT.
+**No non-degenerate compositionality.** The repository's planned interfaces name the objects (global types, projections, grades, cuts) but the current checkout does not yet contain the canonical `src/` definitions or compose them. All composition theorems are deferred pending K-CUT.
+====
+
+[CAUTION]
+====
+**The RapidNJ target is not a proof.** `applications/rapidnj-two-thread.agda` is a standalone typed target with open interfaces and postulates. It is not imported into `All.agda`; the two-thread state diamond, projection square, and K-CUT-LOSS equality remain to be proved.
 ====
 
 [CAUTION]
@@ -109,7 +135,13 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4
 | Path | Proves
 
 | `src/ChoreographicTypes/`
-| Definitions of global types, projection, grades, cuts, K-CUT statements
+| Planned definitions of global types, projection, grades, cuts, K-CUT statements
+
+| `applications/rapidnj-two-thread.adoc`
+| RapidNJ application boundary and the two-event proof decomposition
+
+| `applications/rapidnj-two-thread.agda`
+| Open Agda signatures for the state diamond and two-thread K-CUT-LOSS target
 
 | `echo-types` (sibling)
 | `RoleGraded.choreo-grade-commute` (K-CUT-LOSS base case)

GLOSSARY.adoc

@@ -64,6 +64,48 @@ K-CUT-WARRANT::
   *Classification:* **project-specific** (conjecture).
   *Status:* **OPEN**.
 
+== Applications
+
+[[rapidnj-reduction]]
+RapidNJ reduction::
+  In this repository's application note, one already-selected
+  RapidNJ-style neighbour-joining update over a global state. The note does
+  not claim that upstream RapidNJ has the same two-thread batch interface.
+  *Classification:* **application-specific**.
+  *See also:* <<two-thread-diamond>>, <<independent-frontier>>
+
+[[independent-frontier]]
+Independent frontier (`Independent₂`)::
+  A two-event frontier that is an antichain and additionally satisfies the
+  implementation's read/write disjointness, phase-safety, and deterministic
+  tie-policy conditions. Antichain membership alone is not enough to justify
+  concurrent mutation of a RapidNJ state.
+  *Classification:* **project-specific application predicate**.
+  *Status:* **OPEN** until instantiated and proved for a concrete reduction
+  representation.
+  *See also:* <<cut>>, <<rapidnj-reduction>>
+
+[[two-thread-diamond]]
+Two-thread state diamond::
+  The algorithmic equality, up to canonical state equivalence, that applying
+  two independent reductions in either serialisation gives the same observed
+  RapidNJ state: `step e2 (step e1 s) ~= step e1 (step e2 s)`. It is a
+  prerequisite for the K-CUT application, not K-CUT itself.
+  *Classification:* **application-specific proof target**.
+  *Status:* **OPEN**.
+  *See also:* <<k-cut-loss>>
+
+[[two-thread-k-cut-loss]]
+Two-thread K-CUT-LOSS::
+  The first non-degenerate K-CUT-LOSS target in the RapidNJ application. For
+  every endpoint `p` and witnessed independent two-event frontier, the local
+  grade after the two projected steps equals the transported global loss grade
+  after the two global steps. The conclusion is an equality of loss grades;
+  it is not the warrant bound.
+  *Classification:* **project-specific application conjecture**.
+  *Status:* **OPEN**.
+  *See also:* <<k-cut>>, <<k-cut-warrant>>
+
 == Patterns
 
 [[port-and-reprove]]