From d460adf9fd26affc6efae5383d87ee60cd4bee59 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 22 Sep 2026 21:38:05 +0100 Subject: [PATCH] docs(type-connections): re-cite the residual receipt at run 35781018563 The hub cited the 2026-09-09 receipt (run 34400282291 at 4325198c). The residual repository's sibling pins are now the current echo-types and epistemic-types heads, and the main run for that merge (35781018563 for 938a7a57) is the receipt whose pins are current. The first receipt is kept as history. Closes the citation half of #115; the Echo->Residual and Epistemic->Residual obligations keep their Phase 3 acceptance. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57 --- docs/TYPE-CONNECTIONS.adoc | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/docs/TYPE-CONNECTIONS.adoc b/docs/TYPE-CONNECTIONS.adoc index c403e36..3a5c973 100644 --- a/docs/TYPE-CONNECTIONS.adoc +++ b/docs/TYPE-CONNECTIONS.adoc @@ -171,10 +171,15 @@ Both actual sibling interfaces are imported by the comparison modules: Echo's fibre packaging round-trips, and Epistemic's `SoundWarrant` requires explicit actual-world premises. -https://github.com/hyperpolymath/residual-evidence-types/blob/4325198c10e2e689f084c2f64a27213685a1ffd2/PROOF-STATUS.adoc[The proof record at the checked revision] +https://github.com/hyperpolymath/residual-evidence-types/blob/7ffd4d25a4f3f652f71311609be73e391b25c7cd/PROOF-STATUS.adoc[The proof record] lists the theorem names, commands, pinned sibling revisions and standard-library -warnings. The https://github.com/hyperpolymath/residual-evidence-types/actions/runs/34400282291[hosted Agda proof job] -passed the core, all three rejection controls and both comparisons on 2026-09-09. +warnings. The https://github.com/hyperpolymath/residual-evidence-types/actions/runs/35781018563[hosted Agda proof job] +passed the core, all three rejection controls and both comparisons on 2026-09-22 +for commit `938a7a5764ac18f08b1b7f332378b4d29c32aa37`, with the sibling pins at +the current `echo-types` (`9c4b72b5`) and `epistemic-types` (`dd948fbd`) heads, +inside a digest-pinned Debian 13 container with Agda 2.6.4.3 and no third-party +action. The first receipt, run 34400282291 on 2026-09-09, checked the same core +at the original pins. This is newly written work; the separate starter archive mentioned in the imported assessment has not been recovered.