// SPDX-License-Identifier: MPL-2.0
= Choreographic Types — EXPLAINME
:toc: preamble
:toc-title: Contents
:icons: font
:doctype: article

This file backs every factual claim in link:README.adoc[README.adoc] with
code paths and honest caveats. Read it if you are doing due diligence on
whether the story matches the code. The ledger of every claim with its
status is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]; this file says where
each README sentence comes from.

== Claim-to-implementation map

=== The global type G is a partial causal order with echo and epistemic grades

[quote, README.adoc]
____
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::
`src/Choreographic/Global.agda` defines finite global types with message
and binary choice, every interaction carrying a grade from a parametric
`ResourceAlgebra`; cuts are frontiers (`Cut`). `src/Choreographic/Local.agda`
is the local side, `src/Choreographic/Projection.agda` endpoint projection
with plain merge, cut projection and `Consistent`.

Caveat::
The fragment is finite, binary-choice and plain-merge. There is no
recursion, no full merge, no delegation. Asynchrony is a layer over the same
fragment (`src/Choreographic/Async.agda`): messages and selections in
flight, not queues as data. Warrants are what the type determines (`src/Choreographic/Kripke.agda`); data-dependent
warrants are outside the model.

=== K-CUT-LOSS holds as equality

[quote, README.adoc]
____
K-CUT-LOSS: Grading commutes with projection as an equality. Loss is type-determined.
____

How this is implemented::
`src/Choreographic/KCut.agda`, `kcut-loss`, parametric in any
`ResourceAlgebra`; discharged at `Loss`, `MaxPlus` and `HWM` in
`src/Choreographic/Instances.agda`. `scripts/minimal-laws.sh` certifies the
proof uses only ⊕-idempotence and ⊗-left-unit.

Caveat::
**Proved for the fragment only**, synchronously and, with the sender paying
at send and the receiver at receipt, asynchronously (`akcut-loss` in
`src/Choreographic/Async.agda`, from the same two laws). Beyond it
(recursion, full merge) K-CUT-LOSS is open and pre-registered with its
falsifiers (`docs/pre-registration-addendum-2026-10-12.adoc`).

=== K-CUT-WARRANT holds as a bound, with its transport component

[quote, README.adoc]
____
K-CUT-WARRANT: Warrant transport commutes with projection only as a bound, and only under a SoundWarrant side-condition.
____

How this is implemented::
`src/Choreographic/Kripke.agda` (the frame over consistent cuts;
epistemic-types' `Warrant` / `SoundWarrant` imported, not imitated),
`src/Choreographic/Bound.agda` (the one-sided bound and its direction),
`src/Choreographic/Transport.agda` (the local frontier is known; party
access as epistemic-types' `Preorder`; a world-indexed `AccessibleModality`).

Caveat::
**Same fragment.** `SoundWarrant` is discharged only for warrants the
choreography determines; for anything about payloads it stays an
assumption. Asynchronously the transport result is directional, as
pre-registered (`docs/pre-registration-addendum-2026-10-19.adoc`): the
receiver of a protocol's first message knows it was sent, and its sender
does not know it was received while the receiver has done nothing since
(`src/Choreographic/AsyncKnowledge.agda`); a reply restores that knowledge
in the two-message protocol only (`Instances.Acknowledgement`), the
position-indexed and general-chain forms being open. The bound survives against the sent-so-far grade
(`src/Choreographic/AsyncBound.agda`).

=== The resource algebra is imported, the tropical bridge is named

[quote, README.adoc]
____
The tropical algebra was re-proved in-site, in resource-algebra, rather than imported across kernels.
____

How this is implemented::
`scripts/fetch-siblings.sh` pins `resource-algebra`, `epistemic-types` and
`echo-types` to full commit SHAs. `src/Choreographic/Base/EchoAdditive.agda`
imports echo-types' `experimental/echo-additive/Grade.agda`, packages it as
a `ResourceAlgebra` and proves it is `Loss` operation for operation.

Caveat::
The Lean→Agda bridge is resource-algebra's open row M-2 and is inherited
here as provenance only; nothing mechanical links `MaxPlus` to the Lean
development (`docs/pre-registration-addendum-2026-10-13.adoc`).

=== 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::
`src/Choreographic/Swap.agda` and `src/Choreographic/Operational.agda` prove
the diamond and the two-step cut-loss equality at the type level.
`applications/rapidnj-two-thread.agda` states the operational target with
postulates and is not part of the gate.

Caveat::
`Independent₂` and `independentToAntichain` are RapidNJ's read/write and
phase-safety conditions, not the type's; they stay postulated. Two of the
file's original declarations were shown unsatisfiable as typed
(PROOF-STATUS A-7, A-8).

== The gate

Every PROVEN line in PROOF-STATUS is checked by `.github/workflows/proofs.yml`
running `scripts/check.sh` in a digest-pinned Debian 13 container with the
distribution's Agda 2.6.4.3 and standard library 2.1, under
`--safe --without-K --no-libraries --ignore-interfaces --double-check
-W error`. The four `tests/reject/` fixtures must each fail at their
`invalid` declaration, so the side-conditions are seen to be load-bearing.
The documentation integrity check (`scripts/check-repository.mjs`) is
structural and is never evidence that anything is proved.

== Known gaps

[CAUTION]
====
**K-CUT is open beyond the fragment.** Recursion, full merge and
data-dependent warrants are pre-registered, not proved. Asynchrony is in
for messages in flight; its knowledge results are stated for a protocol's
first message (PROOF-STATUS, "Asynchrony").
====

[CAUTION]
====
**The RapidNJ target is not a proof.** `applications/rapidnj-two-thread.agda`
is a postulated target; its type-level counterparts are in `src/`.
====

[CAUTION]
====
**Cross-kernel consistency is manual.** `MaxPlus` and tropical-types' Lean
definition are kept in agreement by review (resource-algebra M-2).
====

[CAUTION]
====
**echo-types' `Grade.agda` is checked only here.** At the pinned commit no
echo-types CI root imports it.
====

== Evidence Index

[cols="2,3", options="header"]
|===
| Path | Evidence or intent

| `src/Choreographic/All.agda`
| Checks the whole builtins-only development

| `src/Choreographic/KCut.agda`
| K-CUT-LOSS (`kcut-loss`, `proj-cut`, `grade-proj`, `cut-projectable`)

| `src/Choreographic/Kripke.agda`, `src/Choreographic/Bound.agda`, `src/Choreographic/Transport.agda`
| K-CUT-WARRANT, bound form and transport component

| `src/Choreographic/Base/EchoAdditive.agda`
| echo-types' ℕ ∪ {∞} grade as a `ResourceAlgebra`, equal to `Loss`

| `src/Choreographic/Base/RoleGraded.agda`
| The echo-types base case recovered inside `Loss`

| `tests/reject/`
| Side-conditions shown load-bearing by expected rejections

| `applications/rapidnj-two-thread.agda`
| Postulated RapidNJ target (not a proof)

| link:PROOF-STATUS.adoc[]
| The ledger

| link:docs/pre-registration.adoc[Pre-registration record]
| Pre-registration state and provenance ledger
|===