A pre-registration and research notebook for a graded multiparty-session and choreographic type theory, combining echo loss-grades and epistemic standpoint-warrants. Agda is the intended prover, not a completed formalisation. The central artefact is the open keystone K-CUT: the conjecture that grading and transport commute with projection across a consistent frontier.
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 (from
echo-types): the structured information loss at that interaction. -
An epistemic standpoint-warrant (from
epistemic-types): the evidence required to authorise that interaction.
A cut is a consistent frontier (antichain) across the causal order. Loss is read modally: ∇ contingent (loss may occur) / △ non-contingent (loss is impossible), indexed by an ordinal loss value.
The sole purpose of this repository is to prove or falsify the keystone conjecture K-CUT: that grading and transport commute with projection across a cut.
K-CUT states: grading and transport commute with endpoint projection across a consistent frontier. It splits into two fragments:
- K-CUT-LOSS
-
Grading commutes with projection as an equality. Loss is type-determined: the grade of the global cut equals the grade computed locally at the endpoint. Status: OPEN (only degenerate single-static-edge base cases exist, proved in sibling repos).
- K-CUT-WARRANT
-
Warrant transport commutes with projection only as a bound, and only under a
SoundWarrantside-condition. The type upper-bounds discoverability but cannot determine it (an agent may know more than the type requires, but never less). Status: OPEN (no proof exists).
|
Caution
|
Nothing in this repo is proven yet. Only degenerate single-static-edge
base cases exist, located in sibling repositories ( |
Applications are kept in a separate, explicitly non-normative section so that an algorithm or UI does not get mistaken for a proof of K-CUT. The first case study is a two-thread RapidNJ-style reduction:
The smallest target in that case study is the two-event K-CUT-LOSS commuting
square under an Independent₂ witness. The witness must strengthen
antichain membership with disjoint read/write footprints, phase safety, and a
deterministic tie policy. The application note separates this algorithmic
state diamond from the K-CUT equality and records the warrant component as
deferred.
| Concept | Status | Home |
|---|---|---|
Multiparty session / choreographic types |
Standard (Honda–Yoshida–Carbone, Montesi, Hirsch–Garg, Bocchi–Yoshida) |
Core definitions (planned) |
Endpoint projection from global to local types |
Standard |
Projection module (planned) |
Dioid/tropical grading of sessions |
Standard (various timed/costed session works) |
Re-proved in-site (planned) |
Echo loss-grades on choreographic edges |
Imported from |
|
Epistemic warrants on choreographic edges |
Imported from |
|
Assembly of echo + epistemic grades on partial causal orders |
Ours (assembly) |
Core definitions (planned) |
K-CUT (grading/transport commutes with projection across a cut) |
Ours (conjecture) |
The keystone — OPEN |
The planned formalisation will import from the estate’s Agda kernel:
-
echo-types— theℕ ∪ {∞}loss-dioid and thechoreo-grade-commutebase case. -
epistemic-types— the non-factiveWarrant/SoundWarrantinterface (the proof home for the warrant gap in K-CUT-WARRANT).
The tropical resource-dioid is planned to be re-proved in-site rather than imported
across kernels. This follows the estate’s port-and-reprove pattern (precedent:
typed-wasm/…/Tropical.idr). The goal is a self-contained resource-algebra
layer; consistency with tropical-resource-typing remains an explicit
bridge obligation, not an automatic consequence of porting.
The research intent, borrowed-vs-ours ledger and outstanding obligations are preserved in the pre-registration record.
-
NOT Gentzen cut-elimination. A cut here is a consistent frontier (antichain) of a causal order, not a proof-theoretic cut.
-
NOT a kernel or engine. Implementation belongs to
typell. -
NOT a subdirectory of
echo-typesorepistemic-types. It is a standalone repository registered innextgen-typing. -
NOT a claim about an upstream RapidNJ parallel implementation. The RapidNJ note is an application-shaped proof target and states its own refinement boundary.
| Path | Purpose |
|---|---|
|
Application notes and explicitly postulated Agda targets (not proofs) |
|
Research state, provenance and outstanding proof obligations |
|
Owner-only Actions policy repair and verification |
|
Documentation integrity and regression checks (not proof checking) |
There is no canonical Agda build in this checkout. The application target is an illustrative collection of postulates, not a checked proof or a substitute for the planned definitions. Do not treat successful documentation checks as mathematical verification.
With Node.js 22 or newer:
node scripts/check-repository.mjs
node --test tests/*.test.mjsCanonical definitions, endpoint projection, a parametric resource algebra, and the K-CUT statements must be developed before a prover build can be published. No placeholder source tree is provided to imply otherwise.
-
EXPLAINME — current claim-to-implementation map and known gaps
-
Applications — application index
-
RapidNJ case study — the two-thread base-case proof target
-
Glossary — terminology reference
-
Legacy resource-typing EXPLAINME — retained historical document
SPDX-License-Identifier: MPL-2.0 — see LICENSE.