// SPDX-License-Identifier: CC-BY-SA-4.0
= choreographic-types — Proof Status (K-CUT development, 2026-10-19)
:revdate: 2026-10-19

Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Every PROVEN line
names the module that discharges it under
`--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error`
on Agda 2.6.4.3 (Debian `agda-bin=2.6.4.3-1+b2`), with resource-algebra and
epistemic-types on the include path (same kernel; pinned by
`scripts/fetch-siblings.sh`) and, for the one module that needs it,
echo-types with `agda-stdlib=2.1-4`. The gate is
`.github/workflows/proofs.yml` running `scripts/check.sh` and
`scripts/minimal-laws.sh`; see "The gate" at the end.

Every name in a status cell is bound to the code by
`scripts/check-repository.mjs`: it must be a definition (or a file), and the
comment directly above that definition (or the file's header) must name the
row, as `-- Ledger K-1.`  A row cannot outlive its proof, and a proof cannot
be claimed by a row that does not point at it.

== Fragment formalised (scope, stated before the claims)

Finite graded global types with message and *binary* choice; endpoint
projection with *plain merge* (a non-participant's two branches must
project identically); cuts as frontiers (`stop` / `cont-*`); consistent
cuts = plain merge still holds on the truncated branches. Grades are drawn
from any `ResourceAlgebra`. *Not* in the fragment: recursion (μ-types),
full merge, delegation, n-ary choice (a fold of binary), queues as data,
and data-dependent warrants (the frame carries only what the type
determines). Both components of K-CUT-WARRANT — bound and transport — are
in, for this fragment. Asynchrony, with messages and selections in flight,
is a layer over the same fragment (section "Asynchrony" below).

== Keystone

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| K-1 | *K-CUT-LOSS*: for every party p, global G, cut c with `Consistent p c`, `grade↾ p (G ↾ c) ≡ lgrade (proj p G ↾ₗ cutproj p c)` — parametric in the resource algebra | PROVEN (`KCut.kcut-loss`)
| K-2 | `proj-cut`: projection commutes with cutting, `proj p (G ↾ c) ≡ proj p G ↾ₗ cutproj p c`, with no side-conditions and no algebra laws | PROVEN (`KCut.proj-cut`)
| K-3 | `grade-proj`: on a projectable G, the restricted global grade equals the grade of the projection | PROVEN (`KCut.grade-proj`)
| K-4 | K-CUT-LOSS uses exactly two laws: `𝟙 ⊗ x ≡ x` and `x ⊕ x ≡ x`. Associativity, commutativity, ⊗-right-unit, distributivity, order and annihilation are not used | TESTED (`scripts/minimal-laws.sh`: KCut checks against a Core with only those two fields)
| K-5 | `Projectable p G` is not a hypothesis of K-1: `Consistent p c` alone yields `Projectable p (G ↾ c)` (`cut-projectable`). The equality is local to the cut prefix; what happens after the frontier is irrelevant | PROVEN (`KCut.cut-projectable`)
| K-6 | Discharged at the three estate instances: `kcut-loss-Loss`, `kcut-loss-MaxPlus`, `kcut-loss-HWM` | PROVEN (`Instances.kcut-loss-Loss`, `kcut-loss-MaxPlus`, `kcut-loss-HWM`)
| K-7 | Both side-conditions are load-bearing: without `Projectable` the equality fails (restricted grade 1, local 2); without `Consistent` it fails (1 vs 2) | TESTED (`tests/reject/UnprojectableChoice`, `tests/reject/InconsistentCut`, each refused with `1 != 2`)
|===

== K-CUT-WARRANT, bound form (Kripke.agda, Bound.agda)

epistemic-types' `Warrant.agda` is imported (same kernel, pinned commit
495db9c), not re-declared, so "SoundWarrant" below is their record.

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| W-1 | Kripke frame for a choreography: worlds are p-consistent cuts, p's standpoint is its view (local timeline up to the projected cut), two worlds are p-accessible when the views coincide; an equivalence relation | PROVEN (`Kripke.Frame`)
| W-2 | Knowledge is factive (reflexive frame), so every type-determined warrant is a `SoundWarrant` in epistemic-types' sense: the "global soundness of warrants" they leave unformalised, discharged for the warrants the choreography determines | PROVEN (`sound-warrant`)
| W-3 | LOSS ⇒ WARRANT: by K-CUT-LOSS the restricted grade is a function of the view, so p knows it at every world and holds a sound warrant for it | PROVEN (`knows-own-grade`, `own-grade-warrant`)
| W-4 | Bound: if every grade in G is ≽ 𝟙 then `grade↾ p G ≼ grade G`; if every grade is ≼ 𝟙 then `grade G ≼ grade↾ p G`. Uses ⊗-monotonicity (`IsOrdered`) and ⊕-monotonicity (every resource algebra): the first use of order in the keystone | PROVEN (`Bound.grade↾-≼`, `grade-≼↾`)
| W-5 | *K-CUT-WARRANT (bound form)*: at every world p considers possible, the global grade up to the cut is bounded by p's own known restricted grade; direction set by where 𝟙 sits in the order; a sound warrant | PROVEN (`knows-lower-bound`, `knows-upper-bound`, `lower-bound-warrant`)
| W-6 | Discharged: HWM unconditionally (𝟙 = 𝟘 is least), Loss unconditionally in the upper form (𝟙 = fin 0 is greatest), MaxPlus for bot-free types (bot = −∞ is the one grade below 𝟙) | PROVEN (`Instances.kcut-warrant-HWM`, `kcut-warrant-Loss`, `kcut-warrant-MaxPlus`)
| W-7 | "Cannot determine": two worlds party 2 cannot tell apart carry different global grades, and a claim to know the global grade is refused | TESTED (`Instances.Witness`; `tests/reject/GlobalGradeKnown`)
|===

== K-CUT-WARRANT, transport component (Transport.agda)

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| T-1 | Truncating a local type is injective in the cut (`↾ₗ-injective`); injectivity of local constructors is by projections, since matching `refl` on an abstract `Grade` would need K | PROVEN (`Transport.↾ₗ-injective`)
| T-2 | *The local frontier is known*: at every world p knows exactly its projected cut, hence every fact about its own frontier — receiving is knowing it was received; synchronously, sending is knowing it was sent | PROVEN (`knows-local-cut`, `knows-local`; `receiver-knows`, `sender-knows`)
| T-3 | p-accessibility is exactly sameness of p's projected cut (both directions) | PROVEN (`knows-local-cut`, `local-cut-determines`)
| T-4 | Party access `p ⊑ q` ("q sees at least what p sees") is a preorder — epistemic-types' `Preorder` record, instantiated — and knowledge is monotone along it | PROVEN (`party-access`, `knows-mono`)
| T-5 | A silent party is below every party; knowledge flows up the preorder only — `1 ⊑ 2` for the witness protocol is refused | PROVEN (`silent-⊑`, `inherited`); TESTED (`tests/reject/AccessWrongWay`)
| T-6 | epistemic-types' `AccessibleModality` cannot be instantiated as stated: its `E : K → Set → Set` has no world index, and world-free knowledge collapses to the proposition itself (reflexivity). With `E : K → (World → Set) → (World → Set)` — field for field otherwise identical (`IndexedAccessible`) — the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); epistemic-types has since added the same world-indexed records (its Kripke/Indexed module), so the mismatch is resolved upstream; this repository still carries its own copy of the indexed record rather than importing theirs
|===

== Asynchrony (Async.agda, AsyncKnowledge.agda, AsyncBound.agda)

Ladder increment I3a, pre-registered before any proof in
link:docs/pre-registration-addendum-2026-10-19.adoc[]. A cut is still a
prefix of the global type's tree, but each message and each selection in it
is delivered or in flight, and the receiver of anything in flight does
nothing later in the prefix (`Causal`). The sender pays an interaction's
grade at send, the receiver at receipt (`grade↾ₐ`). Worlds are causal cuts
consistent for every party; accessibility is sameness of view, as in W-1.
All eight claims came out as pre-registered.

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| Y-1 | Conservativity: synchronous cuts are exactly the asynchronous cuts with nothing in flight (`Settled`). Embedding lands in them, and on them completion (deliver everything in flight) is its inverse. Embedding preserves projection, consistency, causality and the restricted grade | PROVEN (`Async.embed-settled`, `complete-embed`, `embed-complete`, `acutproj-embed`, `embed-consistent`, `embed-causal`, `grade↾ₐ-embed`)
| Y-2 | *Asynchronous K-CUT-LOSS*: for every causal cut κ consistent for p, `grade↾ₐ p G κ ≡ lgrade (aview p G κ)`, parametric in the resource algebra and discharged at the three instances. It uses the same two laws as K-1: a receiver still waiting is quiet, so its continuation contributes 𝟙 | PROVEN (`Async.akcut-loss`; `Instances.akcut-loss-Loss`, `akcut-loss-MaxPlus`, `akcut-loss-HWM`); TESTED (`scripts/minimal-laws.sh` checks Async.agda against the two-law Core)
| Y-3 | In-flight invisibility: delivering a message or selection in flight changes no party's local cut but its receiver's | PROVEN (`Async.flight-invisible`, `flight-invisible-choice`)
| Y-4 | The asynchronous frame. LOSS ⇒ WARRANT survives: p knows its own restricted grade and holds a sound warrant for it in epistemic-types' interface. p also knows its own frontier (T-2) | PROVEN (`AsyncKnowledge.AFrame`, `aknows-own-grade`, `asound-warrant`, `aknows-local-cut`)
| Y-5 | *Receiver knows sent*: at every world where a protocol's first message s → r (s ≢ r) is delivered, its receiver knows it was delivered, and so that it was sent | PROVEN (`AsyncKnowledge.receiver-knows-delivered`, `receiver-knows-sent`)
| Y-6 | *Sender does not know receipt*, the pre-registered falsifier, confirmed. At every world where the first message is delivered and its receiver has done nothing since, the world where it is still in flight looks the same to every party but the receiver, so the sender does not know it was received. In the synchronous frame the same proposition is a theorem | PROVEN (`AsyncKnowledge.only-receiver-sees`, `sender-cannot-know-receipt`, `sync-sender-knows-receipt`); TESTED (`Instances.sender-blind`, `receiver-sees`, `sender-cannot-know`; `tests/reject/SenderKnowsReceipt`)
| Y-7 | Both bounds survive against the sent-so-far grade `gradeₛ` (the completion's): if every grade is ≽ 𝟙, p's restricted grade is a known lower bound; if every grade is ≼ 𝟙, a known upper bound. A receiver that lags has paid 𝟙 where the completion pays g, which is on the side each bound needs. Discharged as W-6 | PROVEN (`AsyncBound.grade↾ₐ-≼`, `≼-grade↾ₐ`, `grade↾ₐ-≼ₛ`, `gradeₛ-≼↾ₐ`, `aknows-lower-bound`, `aknows-upper-bound`; `Instances.async-warrant-HWM`, `async-warrant-Loss`, `async-warrant-MaxPlus`)
| Y-8 | *A reply restores the knowledge.* In `0 → 1 : a . 1 → 0 : b`, for every resource algebra and grades a, b: once the reply has been received, 0 knows its message was delivered, because a reply can only come from a receiver that has acted. A reply still in flight is not enough | PROVEN (`Instances.reply-gives-knowledge`, `reply-in-flight-is-not-enough`)
|===

Not claimed: a statement for messages other than a protocol's first (they
reduce to it through delivered prefixes, but the position-indexed theorem is
not written), the general form of Y-8 (knowledge of receipt exactly when a
chain of messages leads back from it), and a received-so-far global grade,
which would drop messages from the middle of the prefix and so is not a
prefix of the global type.

== Applications: the two-thread diamond (Swap.agda)

`applications/rapidnj-two-thread.agda` states the first application target
operationally (events, steps, a state diamond, `twoThreadKCutLoss`).  Its
type-level counterpart:

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| A-1 | Two interactions between disjoint party pairs swap without changing any endpoint's projection (`swap-proj`) or restricted grade (`swap-grade↾`); ⊗-left-unit only | PROVEN (`Swap.swap-proj`, `swap-grade↾`)
| A-2 | The unrestricted global grade swaps iff the two grades commute under ⊗ (`swap-grade`); Loss and MaxPlus commute | PROVEN (`Diamond.loss-commutes`, `maxplus-commutes`)
| A-3 | The high-water mark does not commute: independent threads have an order-dependent peak (3 vs 5) invisible at every endpoint | TESTED (`Diamond.hwm-order-sensitive`)
| A-4 | Operational reading (`Operational.agda`): `Step` fires an interaction at the head or beneath independent heads; a global step is a local step at every endpoint (`step-proj`, `step-grade↾`); `StateEq` is projection-equivalence | PROVEN (`Operational.step-proj`, `step-grade↾`)
| A-5 | `twoThreadDiamond` as a theorem: two independent events fired in either order reach projection-equivalent states (`two-thread-diamond`) | PROVEN (`Operational.two-thread-diamond`)
| A-6 | `twoThreadKCutLoss` as a theorem once `transportLoss` takes the state: after two steps the local grade at a projectable state is the restricted global grade (`two-thread-kcut-loss`, i.e. K-3) | PROVEN (`Operational.two-thread-kcut-loss`)
| A-7 | `transportLoss : Role → Grade → Grade` is unsatisfiable: no function of the global grade returns the local grade (two states of global grade `val 1` give party 0 `val 1` and `val 0`) | TESTED (`Instances.NoTransportLoss`)
| A-8 | `globalGradeRespectsStateEq` is false for occupancy: projection-equivalent states with peaks 3 and 5 — `StateEq` must be finer than swap-equivalence for HWM, as predicted | TESTED (`Instances.GradeNotStateInvariant`)
|===

What stays postulated in `applications/rapidnj-two-thread.agda` after this:
`Independent2` and `independentToAntichain` (the implementation's read/write
and phase-safety conditions), which are RapidNJ's, not the type's.

== Base case correspondence (Base/RoleGraded.agda)

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| B-1 | echo-types' three-grade order `keep ≤g residue ≤g forget` embeds into Loss by keep ↦ fin 0, residue ↦ fin 1, forget ↦ inf, and `a ≤g b` iff `embed b ≼ embed a` (the converse of the absorption order) — both directions | PROVEN (`≤g→≼`, `≼→≤g`)
| B-2 | The base lattice is closed under alternatives (min) | PROVEN (`alt-closed`)
| B-3 | The base lattice is not closed under sequence (`fin 1 +g fin 1 = fin 2`): why RoleGraded could only grade one edge | PROVEN (`seq-escapes`)
| B-4 | `EGrade`/`_≤g_` are EchoGraded's: the transcription matches the original constructor by constructor, and the order in both directions | PROVEN (`EchoAdditive.transcribe`, `≤g-transcribe`, `≤g-original`; echo-types is imported at its pin, with agda-stdlib, in that one root)
| B-5 | RoleGraded's *role transport* (`applyRole`, Client ⊑ Server) is reproduced | OPEN — that is the transport/warrant side, K-CUT-WARRANT territory, not graded loss
|===

== Echo-additive instance (Base/EchoAdditive.agda)

echo-types' `experimental/echo-additive/Grade.agda` (pinned commit
`da140cc2`) is imported, not transcribed. This is the "echo-additive ℕ ∪ {∞}
instance" of the ladder's increment I0, and it makes resource-algebra's L-2
("textually identical, reviewed by eye") a checked theorem for this
repository's use.

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| E-1 | `EchoAdditive` is a `ResourceAlgebra` with ⊕ = `⊓g` (min), ⊗ = `+g`, 𝟘 = `inf`, 𝟙 = `fin 0`, filled from echo-types' own lemmas; `IsDioid` (right distributivity from the left law and `+g-comm`), hence `IsOrdered`; `IsAnnihilating` | PROVEN (`EchoAdditive`, `EchoAdditive-dioid`, `EchoAdditive-ordered`, `EchoAdditive-annihilating`)
| E-2 | `EchoAdditive` and resource-algebra's `Loss` are the same algebra: `toLoss` / `fromLoss` are inverse and `toLoss` carries ⊕, ⊗, 𝟘 and 𝟙 across (the standard library's `⊓` and the Prelude's `min` agree clause for clause) | PROVEN (`toLoss∘fromLoss`, `fromLoss∘toLoss`, `toLoss-⊕`, `toLoss-⊗`, `toLoss-𝟘`, `toLoss-𝟙`, `⊓-min`)
| E-3 | echo-types' own `embed : EchoGraded.Grade → Grade` and RoleGraded's `embed` agree through `toLoss` | PROVEN (`embed-agrees`)
| E-4 | `EchoAdditive` is not imported by `Choreographic.All`: the keystone development stays builtins-only, and the standard library enters only through this root | TESTED (`scripts/check.sh` checks `All.agda` with no stdlib path, then this module with one)
|===

Not claimed: that echo-types' `Grade.agda` is checked by echo-types' own CI
(at `da140cc2` no root there imports it; this gate is its only check), and
nothing about the direction resource-algebra chooses for its L-2 import.

== Echo-graded projection commuting square (Base/EchoProjection.agda)

The choreographic analog of echo-types' `choreo-grade-commute`.  echo-types'
`RoleGEcho` is a 2D family indexed by Role and Grade: at keep grade it
carries `RoleEcho r true` (a type that genuinely varies with the role); at
residue and forget grades it collapses to `⊤`.  `choreo-grade-commute` says
role transport and grade degradation commute — 18 cases, all `refl`, with
one non-trivial case (`c⊑s, keep≤keep`) where both sides compute to
`client-to-server e`, a function between different types.

The choreographic analog defines two 2D families indexed by Party and
EGrade: one carrying the restricted grade (grade-indexed), the other the
projected local type (local-indexed), both collapsing to `⊤` at residue
and forget grades.  The party transport requires the restricted grades
(grade version) or projections (local version) to agree.

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| EP-1 | `echo-grade-commute`: grade degradation and party transport commute on the grade-indexed 2D family `CGEchoGrade`, for any parties with the same restricted grade.  Closes by `refl` in all six cases | PROVEN (`EchoProjection.echo-grade-commute`)
| EP-2 | `echo-local-commute`: grade degradation and party transport commute on the local-type-indexed 2D family `CGEchoLocal`, for any parties with the same projection.  Closes by `refl` in all six cases | PROVEN (`EchoProjection.echo-local-commute`)
| EP-3 | Two-event case (`msg 0 1 g₁ (msg 2 3 g₂ end)`): the grade transport exists between sender and receiver of the same message (`same-grade-01`, `same-grade-23`, both `refl`); the local transport exists only between outside parties (`same-proj-45`, `refl`); sender and receiver do NOT have the same projection (`proj-0≢proj-1`).  The square is trivial in ALL cases because the transport is the identity on equal values — there is no choreographic analog of `client-to-server` between different projections | PROVEN (`TwoEvent`); the trivialisation is the result
|===

What EP-3 says about the keystone: echo-types' commuting square has a
non-trivial case because `RoleEcho Client true` and `RoleEcho Server true`
are different types, and `client-to-server` is a genuine function between
them.  The choreographic projection `proj p G` is a value of the fixed type
`Local`, and `grade↾ p G` is a value of the fixed type `Grade`; their
singleton wrappers are contractible, so the only transport between equal
values is the identity.  The B-5 open item (role transport) cannot be
closed by this route: the echo-grade commuting square trivialises before
it reaches the transport/warrant structure.

== K-CUT-WARRANT precise statement (WarrantClaim.agda)

The warrant component of the keystone, stated as a reviewed theorem
statement with every hypothesis and side condition explicit.  Three
components: grade equality (C1, proven from K-CUT-LOSS and frame
factivity), grade bound (C2, proven with a grade-ordering hypothesis
H4), and data warrant (C3, conditional on a receiver-local side
condition H5).  The gap between type-determined and data-dependent
warrants is documented precisely: the type provides the warrant
structure and type-determined evidence (Kripke knowledge) but not
data-dependent evidence or soundness.

epistemic-types' `SoundWarrant` (pinned commit `495db9cc`) is imported,
not re-declared: `Warrant` carries an `Evidence` type; `SoundWarrant`
adds `sound : Evidence → A`.  The receiver-local side condition is
exactly the provision of `Evidence` and `sound` for data-dependent
claims.

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| WC-1 | Grade equality warrant: at every world w, p holds a `SoundWarrant` for `grade↾ p (G ↾ cut w) ≡ grade↾ p (G ↾ cut w)`, with evidence token `knows-own-grade p w`. Hypotheses: H1–H3 only | PROVEN (`Claim.grade-equality-warrant`, `grade-equality-evidence`)
| WC-2 | Grade bound warrant (lower): if `Each (𝟙 ≼_) G`, p holds a `SoundWarrant` for `grade↾ p (G ↾ cut w) ≼ grade (G ↾ cut w)`, with evidence token `knows-lower-bound G p e w`. Hypotheses: H1–H4 | PROVEN (`Claim.grade-bound-warrant-lower`, `grade-bound-evidence-lower`)
| WC-3 | Grade bound warrant (upper): if `Each (_≼ 𝟙) G`, p holds a `SoundWarrant` for `grade (G ↾ cut w) ≼ grade↾ p (G ↾ cut w)`, with evidence token `knows-upper-bound G p e w`. Hypotheses: H1–H4 | PROVEN (`Claim.grade-bound-warrant-upper`, `grade-bound-evidence-upper`)
| WC-4 | Data warrant: for data-dependent φ, p holds a `SoundWarrant` for φ w IF p provides `ReceiverLocalSideCondition p φ w` (Evidence + sound). This is the receiver-local side condition; NOT type-determined | PROVEN as a conditional (`Claim.data-warrant`); the side condition is an external assumption
| WC-5 | Complete K-CUT-WARRANT record: packages C1 and C3; C2 stated separately (direction depends on algebra). `mkComplete` populates from the side condition | PROVEN (`Claim.KCutWarrantComplete`, `mkComplete`)
|===

What WC-4 says about the keystone: the pre-registration's "SoundWarrant
at the receiver (ASSUMED local soundness, not type-determined)" applies
to data-dependent claims only (C3).  The grade claims (C1, C2) are fully
type-determined: evidence is Kripke knowledge, soundness is frame
factivity, and no external assumption is needed.  The gap is precisely
the boundary between what the choreographic type determines (grades,
projections, bounds) and what it does not (payload properties,
authenticity, cryptographic evidence).  epistemic-types'
`ProofTransport.CertificateCheck` provides the vocabulary for the
receiver-local side condition but does not derive it from the type.

== Grading semantics for bounds under interaction (GradingSemantics.agda)

Defines the grading semantics using the algebraic vocabulary of
tropical-types (Resource/Algebra/Interface.lean, read-only provenance
reference; Dioid.lean, read-only proof witnesses).  Keeps grade,
measure, and index distinct.  Derives one-step bound propagation
theorems and the projection theorem from the declared semantics.
Records a checked negative result for non-commutative ⊗.

tropical-types' Lean 4 proof witnesses (canonicalLe partial order,
monotonicity of both operations, ResourceAlgebra.ofIdempotentAdd) are
provenance, not imports.  The Agda IsOrdered record carries the local
verification.  Bridge obligation M-2 is recorded, not discharged.

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| GS-1 | One-step bound propagation for messages: if `grade↾ p G ≼ x`, then `grade↾ p (msg s r g G) ≼ at (role p s r) g ⊗ x`.  Uses ⊗-monotonicity (tropical-types Dioid.lean `canonicalLe_mul_le_mul_left`, provenance; Agda `IsOrdered.⊗-mono`, local verification) | PROVEN (`bound-step-msg`, `bound-step-msg-outsider`)
| GS-2 | One-step bound propagation for choices: if `grade↾ p G₁ ≼ x₁` and `grade↾ p G₂ ≼ x₂`, then `grade↾ p (choice s r g G₁ G₂) ≼ at (role p s r) g ⊗ (x₁ ⊕ x₂)`.  Uses ⊗-monotonicity and ⊕-monotonicity | PROVEN (`bound-step-choice`)
| GS-3 | Two-step bound propagation (composition of GS-1); projection theorem: `restricted-measure p G ≡ local-measure (proj p G)` for projectable types (K-3 restated); bound transfer through projection in both directions | PROVEN (`bound-two-step`, `projection-theorem`, `bound-projection-lower`, `bound-projection-upper`)
| GS-4 | Negative result: the unrestricted measure is NOT compositional under reordering for non-commutative ⊗.  Consequence of A-1 (restricted measure is order-independent for disjoint interactions) and A-3 (HWM unrestricted measure is order-dependent).  Abstract right-cancellation from `(a ⊗ b) ⊗ grade G ≡ (b ⊗ a) ⊗ grade G` to `a ⊗ b ≡ b ⊗ a` requires ⊗-right-unit or right-cancellation, neither in the base algebra.  Concrete witness at HWM (A-3).  No postulates introduced | RECORDED (consequence of A-1, A-3; concrete witness `Instances.Diamond.hwm-order-sensitive`)
|===

What GS-4 says about the keystone: tropical-types' Interface.lean does
not assume `mul_comm` in the base `ResourceSemiring`; `CommResourceSemiring`
is an optional refinement.  The negative result is structural: for any
algebra satisfying the base interface but not the commutative refinement,
the unrestricted measure is order-sensitive while the restricted measure
is not (for disjoint interactions).  This is the precise sense in which
"an occupancy reading is not a cost reading" (P-3).

== Independent₂ and the two-event experiment (Independent2.agda)

Makes Independent₂ explicit for the two-event K-CUT-LOSS experiment:
disjoint footprints (I1), phase safety (I2), cross-stepping (I3).
Deterministic tie-breaking (I4) is a scheduler concern, not a type
concern, and is not included.

[cols="1,3,1",options="header"]
|===
| ID | Claim | Status
| I2-1 | Commuting square under Independent₂: two disjoint events fired in either order reach projection-equivalent states. Restatement of A-5 with explicit conditions | PROVEN (`commuting-square`, via `two-thread-diamond`)
| I2-2 | K-CUT-LOSS across the diamond: after two steps, the local grade at a projectable state is the restricted global grade. Restatement of A-6 | PROVEN (`kcut-loss-across-diamond`, via `two-thread-kcut-loss`)
| I2-3 | A party outside an event sees no change in projection (`outside-invisible`). Structural lemma: under disjoint footprints, each party is outside at least one event, so the commuting square is vacuous from every party's viewpoint | PROVEN (`outside-invisible`)
| I2-4 | Second projection pattern: shared sender (`msg 0 1 g₁ (msg 0 2 g₂ end)` vs swapped) and shared receiver (`msg 0 2 g₁ (msg 1 2 g₂ end)` vs swapped) both fail projection-equivalence. `proj 0 G ≢ proj 0 G'` and `proj 2 G ≢ proj 2 G'` by constructor inequality | PROVEN (`SharedSender.proj-0-G≢proj-0-G'`, `SharedReceiver.proj-2-G≢proj-2-G'`)
|===

What I2-3 and I2-4 say about the keystone: the disjointness condition
(I1) is NECESSARY for the two-event commuting square.  Under I1, each
party participates in at most one event, so the commuting is vacuous
from every party's viewpoint (I2-3).  Dropping I1 breaks the result:
shared parties create ordering dependencies in the local type that
break projection-equivalence (I2-4).  The degeneracy is ESSENTIAL,
not incidental.  This narrows the two-event K-CUT-LOSS claim to
disjoint events.  The general K-CUT claim (arbitrary events, arbitrary
cuts, non-disjoint interactions) remains OPEN.

== Worked protocol (Instances.agda, computed)

Client 0, broker 1, server 2: `0→1:a . 1→2:b . 0→2 chooses {2→1:c | 2→1:c}`.

[cols="1,3,1",options="header"]
|===
| ID | Reading | Status
| P-1 | Loss (1,2,5): broker's restricted grade `fin 8`; at the cut before the server answers, `fin 3` | TESTED (`loss-broker`, `loss-broker-cut`)
| P-2 | MaxPlus (1,2,5): broker `val 8` | TESTED (`maxplus-broker`)
| P-3 | HWM peaks (1,2,5), nothing held: broker's peak `5`, at the cut `2` — an occupancy reading is not a cost reading, inside one protocol | TESTED (`hwm-broker`, `hwm-broker-cut`)
| P-4 | `Projectable 1 G` and `Consistent 1 c₁` are inhabited (by `refl` at the merge) and K-1 instantiates to `broker-cut` | PROVEN (`Worked.projectable-1`, `consistent-1`, `broker-cut`)
|===

== Open (honest — NOT proved)

* *Data-dependent warrants.* The frame carries only what the type
  determines; warrants about payloads are outside it, and there
  `SoundWarrant` stays an assumption — with a precise scope (W-2, T-2).
* *Asynchrony beyond I3a.* Messages in flight are in (Y-1 to Y-8), and the
  pre-registered falsifier came out as predicted (Y-6). Still open: the
  position-indexed form of Y-5 and Y-6, the general form of Y-8 (knowledge
  of receipt needs a chain of messages back), queues as data, and
  asynchrony combined with recursion.
* *Recursion.* μ-types change `Cut` (a frontier through an unfolding) and need
  a coinductive or fuel-indexed grade. Not attempted.
* *Full merge.* Only plain merge. Full merge (branches may differ in labels
  the non-participant later distinguishes) would weaken `Merge`; K-3's
  idempotence step is exactly what would need to generalise.
* *Role transport* (B-5).
* *Operational `step` as a function.* Kept relational; a functional step on
  the quotient needs decidable grade equality or a canonical-form theorem
  for swap-equivalence. Not attempted.
* *Lean→Agda bridge (resource-algebra M-2).* `MaxPlus` is a port of
  tropical-types' Lean 4 `instance : CommSemiring Tropical`; no mechanical
  link exists or is claimed. Every MaxPlus discharge above (K-6, W-6, A-2)
  inherits that obligation: the Lean theorem is provenance, never an import.
* *Sibling pins.* resource-algebra at
  `b2c9f1f6bc7ed7cc83c7573014cdf88d49d2a881`, epistemic-types at
  `495db9cca003e12066a3cb9c9f2d7afa1a953aec`, echo-types at
  `da140cc26fd174b20d5d7fcfafcb4febd3276ff3` (`scripts/fetch-siblings.sh`,
  full SHAs verified after checkout). Correction to the 2026-10-12 entry: the
  `proofs.yml` that merged with #23 never ran on GitHub — all eight runs
  ended in `startup_failure` with no jobs, because its `actions/checkout@v6.0.3`
  is a tag ref and this repository's Actions policy requires SHA pinning. The
  green runs it cited were local. The gate below is the first that runs.

== What W-4 says about the keystone

The bound's direction is not a convention: it is the S-3 finding of
resource-algebra (opposite-running orders) surfacing in the keystone. In HWM
and MaxPlus p's view is a *lower* bound on the global grade; in Loss it is
an *upper* bound in ≼, i.e. numerically p's view accounts for no more loss
than the global total. Any K-CUT-WARRANT statement must say which.

== What Y-6 says about the keystone

Synchronously, a message is one event for both of its ends, and T-2's two
halves (receiving is knowing it was received; sending is knowing it was
sent) say the same thing twice. Asynchronously they come apart. The
receiver's knowledge that the message was sent survives (Y-5), because a
receive is causally after its send. The sender's knowledge that it was
received does not (Y-6), and comes back only when something the receiver
did after the receipt reaches the sender (Y-8). The transport component of
K-CUT-WARRANT is therefore directional, and synchrony was what hid the
direction. The loss component is not: Y-2 needs no new law.

== What K-4 says about the keystone

That K-CUT-LOSS survives with only idempotence and a left unit means the
*equality* half of the keystone is algebraically weak: it holds for
non-commutative, non-associative alternatives. The structure the family
cares about — order, monotone sequencing, the opposite-running orders of
Loss and MaxPlus — is first exercised by the *bound* half, K-CUT-WARRANT.
That is where the next proof effort belongs.

== The gate

`.github/workflows/proofs.yml`: container `debian:13-slim` by digest
(`sha256:a29215f6…`, resolved 2026-10-13), `apt-get install
agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4`, `actions/checkout` by full SHA
(`3d3c42e5…`, v7.0.1), `test "$(agda --version)" = 'Agda version 2.6.4.3'`,
then `scripts/fetch-siblings.sh`, `scripts/check.sh` (a trusted-base step:
no `postulate` under `src/` or `tests/`, exactly one block in the
application target, which `.cicd-hygiene-allow` sanctions; the core root
with no library path; the echo-additive root with echo-types and the standard library;
every `tests/reject/*.agda` must fail at its `invalid` declaration with a
type mismatch) and `scripts/minimal-laws.sh`. Flags on every check:
`--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error
-W noUnsupportedIndexedMatch` (the last because the standard library emits
that warning under `--without-K` and its `.agda-lib` flags are not read under
`--no-libraries`). Committed `.agdai` files were removed in the same change:
the gate never reads an interface it did not just write.

Pattern: epistemic-types `.github/workflows/agda.yml`. Not yet a required
status check on `main` (owner action after the first green run on `main`).