docs(roadmap): close Lane 5 (killer-app accepted) + refresh stale Lane 1 close-out annotation#157
Merged
Merged
Conversation
…e 1 close-out annotation
Two loose-end doc-sweeps surfaced during a repo health survey:
1. Lane 5 (Tutorial / pedagogy) — close via the killer-app branch.
`roadmap.adoc` §Lane 5's unblocking condition has two branches: either
Lane 1 closes, or "a single killer-application example emerges that
justifies a tutorial track on its own merit". The second branch fired
2026-05-26: `tutorial/region_exit_audit/RegionExitAudit.agda` is the
ephapax-L3-corroborated certified region-exit audit example, and
already carried the in-place self-description as the killer-app
candidate. The three walkthroughs (region-exit audit / epistemic
erasure / provenance debugging) all landed in May, build under
`--safe --without-K` with zero postulates via `tutorial/All.agda`,
and carry per-walkthrough Smoke pins + honest-bound + matched-negative
`NotProved-*` ⊤-aliases discipline.
Edits:
* `roadmap.adoc` — remove Lane 5 from active lanes, add a Lane 5
entry under §"Closed lanes" with the close-out route, closing
artefacts, and retraction-watch carried over. The "Why this counts
as a kill, not a deferral" subsection makes the second-branch
unparking case explicit so future audits don't reopen the lane on
"but Lane 1 isn't closed yet" grounds.
* `tutorial/README.adoc` — flip the [PARKED] status to CLOSED in the
section heading + IMPORTANT block; convert the "Killer-app close-out
check" subsection from a candidacy framing to an ACCEPTED record.
* `docs/echo-types/MAP.adoc` — update the two Lane 5 / killer-app
pointers (Walkthrough 1 bullet, track-level docs note) to point at
§"Closed lanes" instead of §"Lane 5 [PARKED]".
2. Lane 1 — refresh the stale close-out criterion.
The Lane 1 §"Close-out criterion (falsifiable)" had `[EXPAND]` tag 2
(related-work pass — Granule / QTT, Uustalu–Vene comonads, coeffects,
choreographic types, lens/optic vs witness-transport leg) listed
without a LANDED marker, even though the paper itself records that
tag 2 was cleared 2026-05-26 via PR #120 (see `paper.adoc:1183` —
"Related-work [EXPAND] cleared 2026-05-26"). Sections §"HoTT homotopy
fibres", §"Graded comonads, coeffects, and QTT", §"Lenses and optics
(the witness-transport leg)" + the 2-categorical rule-out
(`decisions/no-2-cat.adoc`) are live in the paper; the
`comparators.adoc` single-page companion table ships the
axis-by-axis summary.
Edits to Lane 1:
* Mark item 1 as LANDED 2026-05-26 with cross-references to the
three landed paper sections + the cleared tags (1 via PR #73,
3 via PR #84). Tag 4 (ordinal consumer-evidence appendix) is
explicitly flagged as gated on Lane 3 and NOT load-bearing for
Lane 1.
* Refresh the §Bottleneck statement: the in-repo half is closed;
the remaining bottleneck is the offline half of Pillar E (TYPES /
CPP submission, Zenodo DOI mint, library packaging, outreach)
per `pillar-e-offline.adoc`.
* Add a §"Lane-level status" footer: all three falsifiable in-repo
criteria hold, but Lane 1 stays open at lane-policy because the
load-bearing question (visible + defensible standing) cannot be
answered without the offline half. The lane is therefore
IN-REPO CLOSED, EXTERNALLY OPEN; promotion to fully CLOSED waits
on author-driven submission events.
Build invariant unaffected: doc-only sweep. `agda proofs/agda/All.agda`
+ `Smoke.agda` + the kernel-guard + the guardrail script were verified
clean earlier this session at the post-#156 main tip.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 58 issues detected
View findings[
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/echo-types/echo-types",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Issue in codeql.yml",
"type": "missing_workflow",
"file": "codeql.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action rpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "unknown",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "unknown",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "unknown",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "unknown",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
3 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
…oof-debt (#173) ## Summary - Adds `### Added (2026-05-30)` + `### Fixed (2026-05-30)` sections to `CHANGELOG.md` under `[Unreleased]` - Documents three cohorts that landed today: the Slice 3+4 Route A 6-PR arc + #171 doc sweep + #172 proof-debt; the cross-repo ephapax L3 bridge package (#161, #162, #163); the meta cohort (#156, #157, #158, #160) - Format matches 2026-05-28's depth ## Why The `CHANGELOG.md` hadn't been updated since 2026-05-28 — today's 15+ merged PRs were undocumented. Drift-correction. ## Test plan - [x] No code changes; only `CHANGELOG.md` edited - [x] Format follows the existing Keep-a-Changelog convention - [x] GPG-signed 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Two loose-end doc-sweeps surfaced during a repo-health survey:
1. Lane 5 — CLOSED via the killer-app branch
`roadmap.adoc` §Lane 5's unblocking condition has two branches: either Lane 1 closes, or "a single killer-application example emerges that justifies a tutorial track on its own merit". The second branch fired 2026-05-26: `tutorial/region_exit_audit/RegionExitAudit.agda` is the ephapax-L3-corroborated certified region-exit audit example, and already carried the in-place self-description as the killer-app candidate. The three walkthroughs (region-exit audit / epistemic erasure / provenance debugging) all landed in May.
Changes:
2. Lane 1 — refresh stale close-out criterion
Lane 1's close-out criterion had `[EXPAND]` tag 2 (related-work pass) listed without a LANDED marker, even though `paper.adoc:1183` already records "Related-work [EXPAND] cleared 2026-05-26" via PR #120. Sections §"HoTT homotopy fibres", §"Graded comonads, coeffects, and QTT", §"Lenses and optics (the witness-transport leg)" + the 2-categorical rule-out (`decisions/no-2-cat.adoc`) are live; `comparators.adoc` ships the single-page summary.
Changes to Lane 1:
Test plan
Honest scope
This PR does NOT touch the offline half of Pillar E (submission events, DOI mint, packaging, outreach). Those are author-driven per `pillar-e-offline.adoc` and remain owner-action items. Lane 1's full closure waits on those events.
🤖 Generated with Claude Code