docs+feat+fix: roadmap consolidation + Echo-vs-Σ Track A/B/C + Lane 1+2 close-out + paper.adoc P0 fix#118
Merged
hyperpolymath merged 10 commits intoMay 27, 2026
Conversation
…ote Echo-vs-Σ skepticism into reviewer-facing answer Roadmap consolidation - Delete 4 overlapping roadmap docs (docs/echo-types/roadmap.md, docs/PRIORITIZED_PROOF_ROADMAP.md, docs/ProofRoadmap.md, docs/WORK_PLAN.md). - Rewrite roadmap.adoc as the single canonical roadmap: 5-lane tracker with falsifiable close-out criteria audited at every rung consolidation, gates summary, pillar status, M1-M13 historical milestone log, R1-R4 deferred research preserved, lane discipline rules, retraction-watch lines per lane. - Lane 1 (load-bearing) = expeditious type-theoretic grounding alongside choreographic / linear / graded modal types. Lane 3 (Ordinal/Buchholz) explicitly parallel-independent: Echo Core does NOT depend on it. README + readme.adoc Status Snapshot restructure - Split into "Echo Core" and "Ordinal / Buchholz" as parallel- independent tracks with explicit non-dependency banner. Buchholz modules marked experimental until unbudgeted wf-<ᵇʳᶠ_ closure lands. Roadmap section points only at roadmap.adoc and its companion docs (roadmap-gates.adoc, establishment-plan.adoc, buchholz-plan.adoc, taxonomy.md, composition.md). Echo-vs-Σ identity claim (Track A) - Promote core/skepticisms/is-this-just-sigma-types.md from 14-line stub into canonical Echo-vs-Σ map. Five sections mirroring the sceptic demands: irreversibility-as-theorem-family, algebra of loss, categorical identity + bridges, abstraction barrier (consumer-side), canonical examples. Each section cross-links Agda lemmas + Smoke pins + adjacency notes. - Add docs/echo-types/sigma-distinctness-map.adoc as reviewer-facing AsciiDoc companion (same 5-section structure, heavier cross-refs to gates and pillars). - Add no-section family and degrade-laws aggregate rows to docs/theorem-index.md. - Cross-link from roadmap-gates.adoc Gate 2 and docs/characteristic.adoc §"Inherited spec". Cross-ref sweep - 17 files redirected from the 4 deleted roadmap docs to roadmap.adoc (or to more specific surviving docs where the original reference was content-specific). Covers CLAUDE.md, READMEs, MAP.adoc, decision docs, Agda module comments, bridge docs. Retraction discipline - All prose stays inside R-2026-05-18 narrowed claims: no full universal property (only funext-relative pointwise mediator), no graded comonad (only thin-poset reindexing modality), no model- independence (only carrier-parametricity over a fixed grade poset), no Reynolds parametricity (only consumer-side free theorem at the affine instance, planned in Track B). Net diffstat: +711 / -1937 across 25 files. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
5 tasks
…out updates (#119) ## Summary Stacked on top of #118 (consolidation). Closes 2 of 3 Lane 1 close-out items from the new `roadmap.adoc`. The third (paper.adoc `[EXPAND]` tag 2 — related-work pass) remains open; the background-primer tag was confirmed already cleared by PR #73 (2026-05-20). ## Track B — Consumer-side abstraction barrier New `proofs/agda/EchoAbstractionBarrier.agda` with two theorems: - **`affine-consumer-cannot-distinguish`** (positive): any consumer at affine mode assigns the same value to weakened images of the two known-distinct linear echoes. Direct corollary of `affine-all-equal` (the affine residue carrier is contractible). - **`sigma-distinguishes`** (negative companion): the raw Σ-projection `proj₁` IS a consumer that distinguishes `echo-true` from `echo-false`. Exhibits the concrete behaviour the affine interface refuses to export. Together: hiding `proj₁` at affine mode is a structural guarantee, not a convention. Original sketch's Theorem 1 dropped as degenerate. **Build verification:** `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` both exit 0 under `--safe --without-K`, zero postulates, zero funext. Pinned in `Smoke.agda` under own `using` block; wired into `All.agda`. Companion essay `docs/echo-types/abstraction-barrier.adoc` explains the narrow scope: consumer-side free theorem at the headline affine instance — **NOT** general Reynolds parametricity, **NOT** higher-order, **NOT** a categorical universal property. ## Comparators New `docs/echo-types/comparators.adoc` — single-page axis-by-axis comparison of Echo (narrowed) vs four neighbours: Granule, Atkey QTT, Hirsch et al. choreographic types, Linear Haskell. Six axes (primary discipline / judgmental level / categorical anchor / composition law shape / what enforced / what NOT enforced) plus per-comparator subsections plus explicit "What Echo does NOT do" section foregrounding the R-2026-05-18 narrowings. ## Roadmap Lane 1 close-out updates Items 2 (EchoAbstractionBarrier) and 3 (comparators) marked **LANDED 2026-05-26**. Item 1 (paper.adoc tag 2 — related-work) remains the sole open requirement for Lane 1 close-out. ## Retraction discipline R-2026-05-18 respected throughout: no new prose introduces graded-comonad, full-universal-property, model-independence, or general-parametricity claims. EAB essay foregrounds the three narrowings; comparators.adoc "What Echo does NOT do" lists all four retracted framings. ##⚠️ Separate P0 issue flagged (NOT addressed here) `docs/echo-types/paper.adoc` has **unresolved git merge-conflict markers** at lines 557, 1137, 1156 from merge commit `cab99f1`, with the `== Reframing note (2026-05-18)` section duplicated at lines 1158-1194 and 1207-1243. Currently broken on `main`. Needs its own scoped PR with owner-decision on which chunk to keep (HEAD vs `docs/rule-out-2cat-and-roadmap-correction`). ## Test plan - [x] `agda proofs/agda/EchoAbstractionBarrier.agda` exits 0 under `--safe --without-K` - [x] `agda proofs/agda/Smoke.agda` exits 0 (pin verified) - [x] `agda proofs/agda/All.agda` exits 0 (wire verified) - [ ] AsciiDoc rendering of `docs/echo-types/abstraction-barrier.adoc` and `docs/echo-types/comparators.adoc` is well-formed - [ ] No new postulates introduced (grep) Net diffstat: +585 / -14 across 6 files. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
changed the title
7 tasks
…red + Track C land (#120) ## Summary Stacked on #118. Closes the three remaining session items from the user-prioritised batch: 1. **🔴 P0 — `paper.adoc` merge-conflict resolution** 2. **Lane 1 close-out item 1** — `paper.adoc` `[EXPAND]` tag 2 (related-work pass) cleared 3. **Lane 2 close-out item 2** — Track C (per-example raw-Σ counter-programs) landed ## 1. P0 conflict resolution Three unresolved git conflict markers at `paper.adoc:557,1137,1156` from merge commit `cab99f1` (`reframe/retraction-2026-05-18`). Resolution: - **HEAD chunk** (579 lines, lines 558-1136): substantive proof-size + threats-to-validity + related-work analysis. **Kept verbatim.** - **Incoming chunk** (17 lines, lines 1138-1155): `[EXPAND]` note + 2-cat ruleout note. **Kept verbatim.** - **Conflict markers stripped**, no content lost. - **Duplicate `== Reframing note (2026-05-18)`** at lines 1207-1243 deleted; single canonical copy at lines 1158-1194 retained. Net: paper.adoc 1278 → 1238 lines. Now well-formed AsciiDoc on `main`. ## 2. Related-work `[EXPAND]` tag 2 cleared Discovered both stale TODO notes (related-work expansion + 2-cat ruleout fold-in) had their content **silently delivered** in substantive subsections of `== Related work`: - `=== HoTT homotopy fibres` - `=== Graded comonads, coeffects, and QTT (the lineage we are motivated by, but explicitly not an instance of)` - `=== Lenses and optics (the witness-transport leg)` — already contains the 2-categorical rule-out at lines 948-953 Replaced both stale notes with a single explanatory NOTE pointing at the delivered subsections + `docs/echo-types/comparators.adoc` companion. Lane 1 close-out: only the ordinal-appendix `[EXPAND]` (tag 4) remains, correctly gated on the Bachmann-Howard milestone per design. ## 3. Track C — `proofs/agda/examples/EchoVsSigma.agda` Three lemmas pairing each headline example with the small raw-Σ counter-program the Echo interface refuses to export at affine mode: | Lemma | Distinguishes | |---|---| | `parser-sigma-distinguishes` | `echo-parse-nested` vs `echo-parse-pair` at `parses ≡ true` (via `proj₁` + `paren-nested≢paren-pair`) | | `provenance-sigma-distinguishes` | `echo-prov-true` vs `echo-prov-false` at `project ≡ 0` (via `prov ∘ proj₁` + `true≢false`) | | `absint-sigma-distinguishes` | `echo-pos-p1` vs `echo-pos-p2` at `α ≡ pos` (via `proj₁` + `p1≢p2`) | Mirrors `EchoAbstractionBarrier.sigma-distinguishes` at the per-example level. Together with `EchoAbstractionBarrier.affine-consumer-cannot-distinguish`, establishes the Gate 3 matched-positive + matched-negative pair discipline ("raw Σ would leak; Echo blocks it"). **Build verification:** `agda proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, `proofs/agda/examples/All.agda` all exit 0 under `--safe --without-K`, zero postulates. Wired into `examples/All.agda`; pinned in `Smoke.agda` under own `using` block. ## Roadmap updates - Lane 1: item 1 (related-work) now LANDED; only ordinal-appendix EXPAND tag remains (correctly out-of-scope). - Lane 2: item 2 (Track C) now LANDED. Only item 3 (Gate-2 nominee re-audit ≥3/4 surviving) remains for full Lane 2 close-out. ## Retraction discipline (R-2026-05-18) respected throughout No new prose introduces graded-comonad, full-universal-property, model-independence, or general-parametricity claims. ## Test plan - [x] `agda proofs/agda/All.agda` exits 0 under `--safe --without-K` - [x] `agda proofs/agda/Smoke.agda` exits 0 (new Track C pins verified) - [x] `agda proofs/agda/examples/All.agda` exits 0 (new EchoVsSigma wired) - [x] `agda proofs/agda/examples/EchoVsSigma.agda` typechecks in isolation - [x] Zero conflict markers remain in paper.adoc (`grep -nE '^<<<<<<<|^=======|^>>>>>>>'`) - [x] Single `== Reframing note` section (no duplicate) - [ ] AsciiDoc rendering of paper.adoc + roadmap.adoc is well-formed Net diffstat: +140 / -65 across 5 files. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
changed the title
6 tasks
…fold (#121) ## Summary In-repo close-out work across all four currently-open lanes per `roadmap.adoc`. Stacked on PR #118 (consolidation); merges into that branch and will land on `main` together when #118 squashes. - **Lane 1 (Pillar E in-repo).** Status NOTE in `paper.adoc` + `types-abstract.adoc` declaring tags 1/2/3 cleared; tag 4 (ordinal appendix) is gated on Bachmann–Howard per `roadmap.adoc` §Lane 3 — not a missing deliverable for the in-repo half of Pillar E. Honest about the offline boundary (venue choice, Zenodo DOI, library packaging, outreach). - **Lane 2 (Gate 2 re-audit).** `docs/characteristic.adoc` Revision 5: re-checks 4/4 surviving against everything post-Rev-4 (EI-2 termination via PATH B, `characteristic.NonTruncatable` Q2.1 PARTIALLY REDUCIBLE caveat, deliberately-broken `characteristic.N5Falsifier`). Comfortable threshold (≥3/4) met by margin of one. Candidate N5 remains unadopted on the same logic as Rev 4. Closes the Lane 2 close-out criterion (3). - **Lane 4 [PARKED] (bridges-CI scope).** `docs/echo-types/decisions/lane-4-bridges-ci-scope.adoc` adopts option A (separate `echo-bridges-ci` repo with submodules) over option B (in-tree submodules). Three load-bearing reasons; three override triggers; unpark-time playbook. Lane stays PARKED. - **Lane 5 [PARKED] (tutorial track).** `tutorial/README.adoc` scaffolds three walkthroughs at design-doc level: (1) certified region-exit audit tied to ephapax L3 = killer-app candidate; (2) epistemic erasure with the in-memory-bytes-vs-type-level disclosure as the opening sentence; (3) provenance/debugging echo. No Agda lands. Lane stays PARKED. - **`roadmap.adoc`**: Lane 2 close-out item (3) marked LANDED; Lane 4 + Lane 5 sections gain pre-resolved-decision/scaffold pointers. Build invariant held: `agda All.agda` + `agda Smoke.agda` both exit 0 under `--safe --without-K`, zero postulates / escape pragmas / funext (no Agda touched in this commit). ## Test plan - [x] `agda --library-file=/tmp/agda-libs -i proofs/agda proofs/agda/All.agda` → exit 0 - [x] `agda --library-file=/tmp/agda-libs -i proofs/agda proofs/agda/Smoke.agda` → exit 0 - [x] No new postulates / escape pragmas (docs-only commit) - [x] GPG-signed - [ ] CI: governance + Hypatia + agda jobs green - [ ] Auto-merge enabled (squash, delete branch) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
8 tasks
…llar E offline prep + packaging (#122) ## Summary Four follow-on workstreams from the four design decisions on 2026-05-26. Stacked onto PR #118's consolidation branch (lands with #118 on the final squash to main). **Lane 5 [UNPARKED] — Walkthrough 1 landed** - `tutorial/region_exit_audit/RegionExitAudit.agda`: ephapax-L3-style region exit. `LEcho linear` = LiveHandle, `LEcho affine` = AuditReceipt, `exit = weaken`, `audit-no-recovery = no-section-weaken` aliased per-region. Honest-bound disclosure (NOT a byte-zeroing claim) opens the file; matched-negative block at bottom names the four properties NOT proved. - Per-walkthrough Smoke + All; tutorial-track aggregator; `tutorial/README.adoc` unpark status updated. **Lane 3 [ACTIVE PUSH] — ψ-admissibility rank refinement slice** - `proofs/agda/Ordinal/Buchholz/RankAdm.agda`: admissibility-aware rank with α-discriminating bpsi shape `ω-rank-pow ν ⊕ rank-pow α`. Closes 1 of 2 deferred ψ constructors via `rank-mono-<ᵇ⁺-ψα-from-pow`. The `<ᵇ-ψΩ≤` ν=μ boundary case is *re-classified* from "admissibility" to "encoding mismatch" (a real structural gap surfaced by the slice); two design follow-ups documented inline. - Score in `buchholz-rank-obstruction.adoc`: 9/13 → 10/13. **Gate 2 N5 falsifier — sharpened & resolved** - `characteristic/N5Falsifier.agda`: unsolved metas resolved by pinning the implicit role+grade params at the four `applyRole`/`applyGrade` call sites. The 2026-05-18 broken status was *inference*, not content (Agda cannot recover the role from `RoleGEcho r keep = Echo (obs r) true` because `obs` is not injective). Now in `characteristic/All.agda` CI green closure. - `docs/characteristic.adoc` Rev 5b: N5-not-adopted decision UNCHANGED on the cosmetic-only-marginal-evidence logic. **Pillar E offline prep — all three sub-tasks** - `docs/echo-types/pillar-e-offline.adoc`: venue matrix (TYPES first recommended), Zenodo DOI mint plan, library packaging update, three outreach drafts (Granule/QTT, choreographic, Linear Haskell). - `echo-types.agda-lib`: include path extended to repo root (for tutorial tree). - `CITATION.cff` + `.zenodo.json`: pre-staged with placeholder DOIs and ORCID fields left blank (not invented) for author to add post-mint. ## Test plan - [x] `agda --library=echo-types proofs/agda/All.agda` → exit 0 - [x] `agda --library=echo-types proofs/agda/Smoke.agda` → exit 0 - [x] `agda --library=echo-types proofs/agda/characteristic/All.agda` → exit 0 (N5Falsifier now included) - [x] `agda --library=echo-types tutorial/All.agda` → exit 0 - [x] All under `--safe --without-K`, zero postulates / escape pragmas / funext - [x] GPG-signed - [ ] CI: governance + Hypatia + agda jobs green - [ ] Auto-merge enabled (squash, delete branch) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
6 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 26, 2026
… Pillar E packaging README
Three follow-ups in one slice, all on top of the consolidation branch.
Lane 3 (follow-on slice, 2026-05-27):
- Ordinal.Buchholz.RankLex: RankLex record over Ord × Ord, _<lex_
data type (first-strict / second-strict-with-shared-implicit-a),
rank-lex : BT → RankLex (bOmega ν seeds the second component
with ω-rank-pow ν as a placeholder), and headline
rank-mono-<ᵇ-ψΩ≤-lex covering both ν<μ (first-strict via
ω-rank-pow-mono) and ν=μ (second-strict via the admissibility
bound rank-pow α <′ ω-rank-pow ν).
- Pinned in proofs/agda/Ordinal/Buchholz/Smoke.agda (own block per
CLAUDE.md Working rules), wired into proofs/agda/All.agda.
- docs/echo-types/buchholz-rank-obstruction.adoc per-constructor
verdict bumped 10/13 → 11/13; <ᵇ-ψΩ≤ flips from "encoding
mismatch" to "closed (Lane 3 follow-on)" with the lex pair
explanation. Open work narrowed to just <ᵇ-+1 joint-bplus.
Lane 5 (Walkthrough 2 LANDED):
- tutorial/epistemic_erasure/EpistemicErasure.agda — concrete
KDF (4-seed → 2-key), two distinct echoes of the same key,
no-section-via-residue lifted from EchoResidue's existing
Bool-collapse no-section. Honest-bound disclosure at top
(NOT a byte-zeroing claim). Matched-negative block at
bottom (NotProved-byteZeroing / cryptographicOneWayness /
collisionResistance / seedDistribution as ⊤-aliases so a
grep NotProved catches every category-error claim).
- tutorial/epistemic_erasure/Smoke.agda, All.agda, README.adoc.
- Wired into tutorial/All.agda; tutorial/README.adoc unpark
status updated to "1 + 2 LANDED, 3 still at design-doc level".
Pillar E offline (pre-staging beyond gates):
- README.md gains §"Installing as a library" (under Build) +
§"Citation". Both consistent with the existing CITATION.cff
placeholder DOI and pillar-e-offline.adoc activation sequence.
- docs/echo-types/pillar-e-offline.adoc §"Zenodo DOI mint" and
§"Library packaging" gain "Pre-staging status" subsections
recording what is landed (CITATION.cff, .zenodo.json, README
sections, echo-types.agda-lib) and what is deferred (CI
install-self job + GitHub→Zenodo workflow — both gated on
user authorising the Zenodo integration; bundling them avoids
a transient CI red).
Build verification: All four entry points exit 0 under
--safe --without-K with zero postulates:
- proofs/agda/All.agda
- proofs/agda/Smoke.agda
- proofs/agda/Ordinal/Buchholz/Smoke.agda
- tutorial/All.agda
Based off the in-flight PR #118 consolidation branch (which carries
RankAdm + the previous session's Lane 3 active-push, Lane 5
Walkthrough 1, N5 sharpening, and Pillar E pre-staging).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… + Pillar E README (#123) ## Summary Three follow-ups in one slice, all atop PR #118's consolidation branch. ### Lane 3 — lex-pair slice closes \`<ᵇ-ψΩ≤\` ν=μ boundary - New \`Ordinal.Buchholz.RankLex\`: \`RankLex\` record over \`Ord × Ord\`, \`_<lex_\` with first-strict and shared-implicit second-strict constructors, \`rank-lex : BT → RankLex\` (\`bOmega ν\` seeds second component with \`ω-rank-pow ν\`), and headline \`rank-mono-<ᵇ-ψΩ≤-lex\` covering both ν<μ (first-strict via \`ω-rank-pow-mono\`) and ν=μ (second-strict via admissibility bound \`rank-pow α <′ ω-rank-pow ν\`). - Implements option (A) from \`RankAdm.agda\` §"<ᵇ-ψΩ≤-still-open". - \`docs/echo-types/buchholz-rank-obstruction.adoc\` per-constructor score 10/13 → 11/13. - Open work now narrowed to just \`<ᵇ-+1\` joint-bplus. ### Lane 5 — Walkthrough 2 LANDED (epistemic erasure) - \`tutorial/epistemic_erasure/\`: concrete 4-seed → 2-key KDF, two distinct echoes of the same key, no-section-via-residue lifted from \`EchoResidue.no-section-collapse-to-residue\`. - Honest-bound disclosure at top (NOT a byte-zeroing claim) + matched-negative block at bottom (\`NotProved-*\` ⊤-aliases so a \`grep NotProved\` catches every category-error claim). - \`tutorial/All.agda\` and \`tutorial/README.adoc\` updated: walkthroughs 1+2 LANDED, walkthrough 3 still design-doc. ### Pillar E offline — README pre-staging - \`README.md\` gains §"Installing as a library" + §"Citation" sections (consistent with existing \`CITATION.cff\` placeholder DOI). - \`docs/echo-types/pillar-e-offline.adoc\` updates "Pre-staging status" subsections under §"Zenodo DOI mint" and §"Library packaging" to record landed vs deferred items. CI install-self + Zenodo workflow deferred until user authorises the Zenodo integration (avoids transient CI red). ## Test plan - [x] \`agda --library-file=/tmp/agda-libs -i proofs/agda proofs/agda/All.agda\` exits 0 - [x] \`agda --library-file=/tmp/agda-libs -i proofs/agda proofs/agda/Smoke.agda\` exits 0 - [x] \`agda --library-file=/tmp/agda-libs -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agda\` exits 0 - [x] \`agda --library-file=/tmp/agda-libs -i . -i proofs/agda tutorial/All.agda\` exits 0 - [x] \`--safe --without-K\` throughout, zero postulates - [x] CITATION.cff DOI placeholder + ORCID-commented preserved (no invented metadata) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ction + layer-2 no-section contrast Lane 5 Walkthrough 3 lands; the originally-scaffolded Lane 5 triplet (region-exit audit, epistemic erasure, provenance / debugging) is now complete in Agda. Domain: 4-element `State` with two orthogonal sign bits. Visible output `firstSign : State → Bool`; class predicate `secondSign : State → Bool` is injective within each firstSign-fibre. Three residue layers walked: full echo (Layer 0), class residue with secondSign (Layer 1), trivial residue (Layer 2). Headlines (all pinned in tutorial/provenance_debugging/Smoke.agda): * `states-distinct-at-true` — Layer 0 distinguishes pp vs pn at the same visible output. * `classes-remain-distinct` — Layer 1 still distinguishes them. * `recover-section-at-layer-1` (POSITIVE) — Layer 1 has a section; `recover-from-class` is a right inverse of `state-to-class`. * `trivials-collapse` — Layer 2 collapses the two echoes. * `no-recovery-from-trivial` (NEGATIVE) — Layer 2 has no section; structural mirror of EchoResidue.no-section-collapse-to-residue. * `provenance-walk-contrast` — section / no-section pair as a Σ. New pedagogical shape: W1 and W2 each ship a one-sided no-section; W3 ships BOTH a section (Layer 1) and its absence (Layer 2), exhibiting the boundary at which type-level recovery flips. The mechanical load is that secondSign is injective within each fibre. Honest-bound + matched-negative discipline inherited from W2 — Agda file and README both open with the type-level disclosure (NOT a runtime debugger), `NotProved-*` block at the file's bottom catalogues out-of-scope properties. Build invariant held: All.agda + Smoke.agda + tutorial/All.agda + tutorial/provenance_debugging/Smoke.agda all exit 0 under --safe --without-K, zero postulates, no funext. Files: * tutorial/provenance_debugging/ProvenanceDebugging.agda (worked example) * tutorial/provenance_debugging/Smoke.agda (headline pins) * tutorial/provenance_debugging/All.agda (aggregator) * tutorial/provenance_debugging/README.adoc (narrative) * tutorial/All.agda — registers W3 * tutorial/README.adoc — W3 flipped from design-doc to LANDED * CLAUDE.md — Session arc 2026-05-27 entry Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…tion for joint-bplus closure First slice of option (A) per `RankPow.agda`'s preamble and `docs/echo-types/buchholz-rank-obstruction.adoc` §"What remains open": discharge the last open per-constructor case `<ᵇ-+1` joint-bplus by dominating `rank-pow t` with an additive-principal ω-power indexed by the leading Ω-marker of `t`. This slice lands the *head-Ω abstraction itself*, no rank-mono. The domination lemma and the headline discharge are explicitly deferred to follow-on slices so the abstraction stands on its own. New module `Ordinal.Buchholz.HeadOmega`: * `head-Ω : BT → OmegaIndex` — leftmost-deepest Ω marker. `bzero ↦ fin 0` (default; future rank-mono guards via non-bzero premise), `bOmega ν ↦ ν`, `bplus x _ ↦ head-Ω x` (leftmost), `bpsi ν _ ↦ ν`. * Four definitional sanity lemmas, one per `BT` constructor (each `refl`), so downstream rewrites don't need to unfold the function. * `head-Ω-bplus-left` — two-level compositional convenience for the WfCNF left-spine pattern that future slices will walk. Pinned in `Ordinal/Buchholz/Smoke.agda` under own `using` block with header comment per CLAUDE.md "Working rules"; wired into `proofs/agda/All.agda` between `RankLex` and `RankMonoUmbrella`. Build invariant held: HeadOmega + Buchholz/Smoke + top-level Smoke + top-level All all exit 0 under --safe --without-K, zero postulates, no funext. Follow-on slices (documented in HeadOmega.agda preamble): * Slice 2 — `ω-rank-pow-succ` + the domination lemma `rank-pow t <′ ω-rank-pow-succ (head-Ω t)` for non-bzero WfCNF terms. * Slice 3 — `rank-mono-<ᵇ-+1-via-head-Ω` headline discharge. * Slice 4 — full `rank-pow-mono-<ᵇ⁻` umbrella. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… 3 head-Ω slice in README/W2-README Cleanup pass before PR #118 merge. * docs/echo-types/echo-kernel-note.adoc — adds EchoAbstractionBarrier (Lane 1 / Lane 2 Track B artefact, landed 2026-05-26 via PR #119) to the Tier-2 derived-modules list with a note pointing at its load and import set. Was previously missing; the kernel-guard.sh CI gate (`scripts/kernel-guard.sh` step B) was failing with "unclassified Echo* module(s): EchoAbstractionBarrier". Now passes. * README.md — adds two one-line status updates: * Lane 5 tutorial triplet LANDED 2026-05-27 under tutorial/ (region-exit audit, epistemic erasure, provenance / debugging), with build command. * Buchholz rank-monotonicity matrix at 11/13 closed via the WfCNF- restricted `_<ᵇ⁻_` umbrella; the last open `<ᵇ-+1` joint-bplus case opens via Ordinal.Buchholz.HeadOmega's first slice landed 2026-05-27. * tutorial/epistemic_erasure/README.adoc — fixes the stale "W3 remains at scaffold/design-doc level" claim; W3 also landed 2026-05-27. Local verification: kernel-guard.sh, tools/check-guardrails.sh, and the full agda sequence (All / Smoke / characteristic/All / examples/ All / tutorial/All) all exit 0 under --safe --without-K, zero postulates, no funext. This is the canonical CI sequence per .github/workflows/agda.yml. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
deleted the
docs/consolidate-roadmaps-and-sigma-skepticism-2026-05-26
branch
3 tasks
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,101 @@ | |||
| {-# OPTIONS --safe --without-K #-} | |||
| @@ -0,0 +1,215 @@ | |||
| {-# OPTIONS --safe --without-K #-} | |||
| @@ -0,0 +1,301 @@ | |||
| {-# OPTIONS --safe --without-K #-} | |||
| @@ -0,0 +1,148 @@ | |||
| {-# OPTIONS --safe --without-K #-} | |||
🔍 Hypatia Security ScanFindings: 43 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 secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/provenance_debugging/ProvenanceDebugging.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/region_exit_audit/RegionExitAudit.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/proofs/agda/EchoThermoCollapseImpossible.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (3 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/proofs/agda/EchoPullbackUnivF4.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/proofs/agda/EchoGradedComonadF1.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/proofs/agda/EchoAbstractionBarrier.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
## Summary Single doc-refresh slice covering 2026-05-27 work (mine + parallel session) now that PR #118 has landed on main. - **CHANGELOG.md** — 2026-05-27 Added/Changed entries (RankAdm/RankLex/HeadOmega slices, Walkthroughs 1+2+3, Pillar E packaging, Gate 2 Rev 5+5b, roadmap consolidation, N5 promotion, per-constructor score 10→11/13). - **docs/echo-types/MAP.adoc** — Buchholz entry updated with new modules + obstruction-doc pointer; new "Tutorial / pedagogy [REAL]" top-level section. - **EXPLAINME.adoc** — "Ongoing tracks at a glance" + "Where to look first" subsections. - **roadmap.adoc** — Lane 3 bottleneck 10/13 → 11/13 with named slices, narrowed close-out criterion to head-Ω domination route; Lane 5 "Walkthroughs landed (2026-05-26/27)" subsection (lane still PARKED at policy level); Pillar E pillar-status row updated with pre-staging detail + owner-action list. Wiki Home.md refreshed in parallel: echo-types.wiki @ 3798dc9. CLAUDE.md left unchanged — parallel session already added 2026-05-27 session arcs for Walkthrough 3 and head-Ω. ## Test plan - [x] No Agda touched; build invariants unchanged - [x] All doc cross-references resolve to files that exist on main - [x] Wiki commit pushed 🤖 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
2 participants
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
Single batched landing for the full session. Now contains four logical units:
roadmap.adocwith lane discipline.EchoAbstractionBarrier.agda(typechecks--safe --without-K) + companion essay + comparators table + paper.adoc related-work[EXPAND]cleared.examples/EchoVsSigma.agda) + resolution of three unresolved git conflict markers in paper.adoc.1. Roadmap consolidation
docs/echo-types/roadmap.md,docs/PRIORITIZED_PROOF_ROADMAP.md,docs/ProofRoadmap.md,docs/WORK_PLAN.md).roadmap.adocas the single canonical roadmap: 5-lane tracker (cap=5; falsifiable close-out criteria audited at every rung consolidation), gates summary, pillar status, M1–M13 historical log, R1–R4 deferred research preserved, lane discipline rules, retraction-watch lines.2. Track A — Echo-vs-Σ synthesis
core/skepticisms/is-this-just-sigma-types.mdpromoted from 14-line stub to canonical answer doc organised under 5 sceptic demands.docs/echo-types/sigma-distinctness-map.adoc— reviewer-facing AsciiDoc companion.docs/theorem-index.mdgains no-section family and degrade-laws aggregate rows.roadmap-gates.adocGate 2 anddocs/characteristic.adoc.3. Track B + Lane 1 close-out
proofs/agda/EchoAbstractionBarrier.agda— two theorems:affine-consumer-cannot-distinguish(positive) +sigma-distinguishes(negative companion). Together: hidingproj₁at affine mode is a structural guarantee, not a convention. Companion essaydocs/echo-types/abstraction-barrier.adoc.docs/echo-types/comparators.adoc— single-page axis-by-axis comparison of Echo (narrowed) vs Granule / Atkey QTT / Hirsch et al. choreographic / Linear Haskell, with explicit "What Echo does NOT do" section.paper.adocrelated-work[EXPAND]cleared — content was already delivered in 8 substantive subsections; stale TODO notes removed; explanatory closure note added.4. Track C + paper.adoc P0 fix
proofs/agda/examples/EchoVsSigma.agda— three per-example raw-Σ counter-programs:parser-sigma-distinguishes,provenance-sigma-distinguishes,absint-sigma-distinguishes. Mirrors Track B at the per-example level for Gate 3.cab99f1) stripped, both chunks preserved, duplicate Reframing note deleted. paper.adoc: 1278 → 1238 lines, now well-formed.Build verification
agda proofs/agda/All.agda,proofs/agda/Smoke.agda,proofs/agda/examples/All.agdaall exit 0 under--safe --without-K, zero postulates, zero escape pragmas.Retraction discipline (load-bearing)
All prose stays inside R-2026-05-18 narrowed claims: no full universal property (only funext-relative pointwise mediator), no graded comonad (only thin-poset reindexing modality), no model-independence (only carrier-parametricity over a fixed grade poset), no Reynolds parametricity (only consumer-side free theorem at the affine instance). Each lane carries an explicit retraction-watch line.
Lane state after this PR
[EXPAND](tag 4) remains, correctly gated on Bachmann-Howard milestone per design.What this PR does NOT do
Test plan
agda proofs/agda/All.agdaexits 0 under--safe --without-Kagda proofs/agda/Smoke.agdaexits 0agda proofs/agda/examples/All.agdaexits 0EchoAbstractionBarrier.agda,examples/EchoVsSigma.agda)grep -nE '^<<<<<<<|^=======|^>>>>>>>')== Reframing notesection in paper.adocNet diffstat: +1625 / -2016 across 32 files.
🤖 Generated with Claude Code