Knowledge Contracts, Version 2: A Typed Substrate for Inter-Agent Knowledge Transfer, with Its Algebraic Laws Proved or Refuted

Systems of cooperating LLM agents exchange state as prose. Prose handoffs lose deontic force, invert relation directions, invite readers to fill gaps with defaults, and leave a knowledge store’s internal wholeness uncheckable. We present a knowledge substrate in which the unit of exchange is a context — a finite set of typed, scoped assertions under a snapshot pin — carried on immutable, digest-pinned, append-only revisions, with every algebraic law of the transfer operations proved or refuted on this carrier rather than assumed. The substrate is implemented and mutation-tested — a refusal catalog of 27 codes at the 2026-08-30 evidence pin, each proven red and growing since only through that same door (§8.10); sixteen invariants enforced at honestly labeled tiers; the reduction ladder R0–R3 with exactness certificates — and exercised on real work: a live store grown from 14 to 134 revisions at the §8.10 recount — organic dogfooding for the first stretch, then a bulk corpus lift (14→63, §8.8) and requirements work this paper does not describe (63→134, §8.10), named as what each stretch was rather than folded under one word (an adversarial review, 2026-09-09, found “dogfooding” over-general for growth this paper’s own §8.8/§8.10 attribute to two other causes) — an admission gate 4-for-4 on real tasks, two write races decided by the append-only law, and two contour defects the run itself surfaced — a truncating renderer and an ungoverned executor over-claim. The work refutes three of this line’s own claims — two facets of the token-economy claim and one store-debt figure, the last felled by the parallel run rather than the evaluation — and narrows the delta claim; the refutations are the headline result. On a stage-snapshot-dominated corpus — session-to-session handoffs, where the pilot’s largest reductions (43.1%, 36.4%) lived, are excluded from the systematic sample and untested here — automated spec-only encoding inflates tokens 7.6% across 18 samples, while a structured-summary baseline under the same instruction reaches 14.8% losslessly on the same sources: reduction tracks the encoder, not the format, on this frame. Hand encoding lands within 0.1 percentage points of the pilot’s 38% on a 4-sample subset where the automated arm reduces only 2.2% — a single-point match against a pilot whose own per-artifact spread is about 12 points, stated as what it is rather than as reproduction. Recall of load-bearing source units — not fidelity in the full sense; this measure counts survival of what the source stated and cannot see a fabricated addition (§1.1’s second failure class), a limit an adversarial review found unstated (2026-09-09) — measured jointly: automated packets preserve 99.3% of 437 semantic units, but the hand encoding behind the 38% preserved only 82.7% — the token win and the completeness rule trade against each other, and token-matched compression across formats remains unmeasured. The delta claim narrows to within-task chains (4/4 counter-pairs); at near-lossless encoding, 144 blind downstream grades hit a 47/48 ceiling in every arm alike — no test with that little variance has the power to distinguish packet from honest prose, and none is claimed to. What the typed carrier exhibits, uncompared (an adversarial review, 2026-09-09, found “demonstrably earns” overstated — §8.7 item 4): machine-checkable recall of load-bearing source units after the fact — an observed MUST→SHOULD drift caught by the evaluation’s unit audit, checkable because modality is a field, and not a fidelity claim in the sense that would also catch a fabricated addition — admission gating, digest-decided concurrency, and projection focus. The co-evolution objection — that the corpus and its enforcing checks were built together — has two measured limits. A sensitivity replay, run in the store’s own append-only order, finds pre-enforcement source content for 10 of the 15 discriminable refusal codes; for the other 5 the objection stands, tested and unrefuted. A separate check-removal experiment finds three codes whose suppression admits a revision that subsequently crashes the unchanged Markdown renderer, with no pre-enforcement source witness for those three. This establishes necessity for that operation on those inputs, not independence of the corpus or failure of downstream LLM work. For the algebraic laws of §4 and the invariants of §5 the objection is untested — none of Theorem 1, Proposition 5, I4 or I5 is among the 26 codes the earlier 86-code sensitivity replay reached (§8.7 item 9); membership in the current replay’s 31 witnessed codes was not re-checked. What the design is not compared against is named to the same standard rather than conceded in a phrase: retrieval-augmented handoff, standard graph serializations under shape validation, and token-matched baselines are unmeasured, each carrying the result that would falsify the design. The method itself is adapted rather than invented — specification mutation and vacuity detection, credited in §2.10, where the analogy to weak-versus-strong mutation is withdrawn as wrong. A measurement instrument fabricated a number twice; only recomputation-from-source in CI held.

What this paper is for, stated so it can be quoted against us: it reports what a typed, digest-pinned substrate for inter-agent knowledge transfer exhibits, uncompared — and the measured answer is refusal, not economy.