Repository navigation
TYPE-CONNECTIONS.adoc: re-cite the residual receipt (run 35773288367 @ 8f3b46f) and give the Echo→Residual / Epistemic→Residual obligations acceptance criteria #115
Description
Activity
Acceptance 1 is on PR #116 (
docs/residual-receipt-35781018563, commit d460adf):docs/TYPE-CONNECTIONS.adoc:174–182now cite PROOF-STATUS at residualmain7ffd4d25and the hosted run 35781018563, themainrun for the merge of residual PR #7 (938a7a57), whose sibling pins are the current echo-types (9c4b72b5) and epistemic-types (dd948fbd) heads. The first receipt (run 34400282291, 2026-09-09) is kept as history. The interim "re-verified beside the original" step for run 35773288367 was not needed: the pin refresh landed first.Not merged: #116 carries the pre-existing
Hypatia neurosymbolic scanred (onmainsince run 35602727566) and the ruleset'scode_scanningrule sees 33 open Hypatia alerts at the merge ref, so it reportsBLOCKEDwith all required checks green. Triage with acceptance criteria: #117. This issue stays open for acceptance 2 and 3 (Echo→Residual, Epistemic→Residual), which land with the residual Phase 3 milestone.One measured fact for acceptance 3:
Warrant.agdaatdd948fbdis blob-identical to the version at the old pin3f4250f7and imports onlyAgda.Primitive, soEpistemicComparisonstill proves typing only. The issue's premise is unchanged by the refresh.🤖 Generated with Claude Code
- added a commit that references this issue
on Sep 22, 2026 Update: acceptance 1 is now on
main. #116 merged as86cb69e5(2026-09-22T20:56Z) through the ruleset with no bypass (rule-suite 4182119358, every rulepass) after the owner's ruling D84 re-scoped thecode_scanningrule to the tools that analyse PR refs.docs/TYPE-CONNECTIONS.adocnow cites residual-evidence-types receipt run 35781018563 at commit938a7a57with the sibling pins at the currentecho-typesandepistemic-typesheads. Acceptance 2 and 3 remain for the Phase 3 milestone; the two pre-existing reds live in #117.🤖 Generated with Claude Code
Status after residual-evidence-types' second milestone (landed 2026-09-30):
- Acceptance 1: met earlier (docs(type-connections): re-cite the residual receipt at run 35781018563 #116). PR docs(type-connections): record the second residual milestone (run 36740394802) #120 re-cites again: run 36740394802 for residual
befdf964, with PROOF-STATUS pinned ata9f3a9d2. - Acceptance 2: partly met.
ResidualEvidence.Compositionstates and provescompose-claims, with its reject module (FalseCoarsening) rejected in CI. It is proved on the residual side only. There is still no statement over the Echo comparison (tests/integration/EchoComparison.agdais unchanged since the first milestone). Stays open. - Acceptance 3: partly met.
ResidualEvidence.Revisionmakes retraction constructive (Refuted,survives-retraction,revise;FalseRetractionrejected).EpistemicComparisonhas not been extended, so the "more than typing" measurement is still open. Stays open. - Acceptance 4: 34400282291 is kept as history; the current run appears once docs(type-connections): record the second residual milestone (run 36740394802) #120 lands.
#120 is held green-except-for pre-existing Hypatia reds (#117, #121), under the 2026-09-22 ruling.
🤖 Generated with Claude Code
- Acceptance 1: met earlier (docs(type-connections): re-cite the residual receipt at run 35781018563 #116). PR docs(type-connections): record the second residual milestone (run 36740394802) #120 re-cites again: run 36740394802 for residual
- added a commit that references this issue
on Oct 5, 2026
Measured (2026-09-22, main = 1fa506c)
docs/TYPE-CONNECTIONS.adoc:174linksresidual-evidence-types/blob/4325198c…/PROOF-STATUS.adoc;:176links run 34400282291 (2026-09-09).8f3b46f0(2026-09-22T19:21Z); itsAgda proofsrun 35773288367 is green on the container recipe (Agda 2.6.4.3, stdlib 2.1,--double-check, zero third-party actions). The proof core is byte-identical to 4325198c, so the cited claims hold; the citation is stale, not wrong.:114"Echo → Residual Evidence" and:118–119"Epistemic → Residual Evidence: make the meaning and evidence obligations of candidate-wide claims explicit" are listed as obligations with no acceptance criteria.Acceptance criteria
:174–176re-cite the current receipt (commit and run) once the residual Phase 2 pin refresh lands (echo-types7a569b7→9c4b72b5, epistemic-types3f4250f→dd948fbd), so the hub cites a receipt whose sibling pins are current. Until then, the 8f3b46f run is added as "re-verified" beside the original.ResidualEvidence.Composition, Phase 3 item 2 of the family plan) states and provescompose-claimsover the Echo comparison, with its reject module rejected in CI.ResidualEvidence.Revision, Phase 3 item 3) makes retraction constructive andEpistemicComparisonproves more than typing (whetherSoundWarrantsits on a vacuous path is the open measurement).grep -c 34400282291 docs/TYPE-CONNECTIONS.adocis 1 today; after, the current run id appears and the old one is kept as history or removed.🤖 Generated with Claude Code