Skip to content

Commit e96cedc

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
Merge origin/main: Decoration Bridge (R5 exploratory) + Lane 3 head-Ω Slice 2 + CI updates
Resolves conflicts in CHANGELOG, CLAUDE, EXPLAINME, MAP, roadmap by preserving both my session work (Tier-1+2+3 + audience + suite + F5 FULL PASS) and the parallel-session ordinal track work (PRs #130/#131/#133/#134) + Decoration Bridge scaffold (PR #129) + CI updates (PRs #114/#116/#117). CLAUDE.md session arcs read top-to-bottom in reverse-chronological order: mine (Slice-2 adoption → broad-cleanup → F5 stages → Tier-2 → Tier-1+2 → keystone → audit follow-on), then upstream's Lane 3 head-Ω Slice 2 arc, then Lane 5 Walkthrough 3, then older arcs. Build: --safe --without-K, zero postulates, Smoke + All exit 0. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2 parents f3fdecd + 172b071 commit e96cedc

16 files changed

Lines changed: 1540 additions & 193 deletions

‎.github/workflows/mirror.yml‎

Lines changed: 3 additions & 133 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
# SPDX-License-Identifier: MPL-2.0
2-
# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
32
name: Mirror to Git Forges
43

54
on:
@@ -11,135 +10,6 @@ permissions:
1110
contents: read
1211

1312
jobs:
14-
mirror-gitlab:
15-
runs-on: ubuntu-latest
16-
if: vars.GITLAB_MIRROR_ENABLED == 'true'
17-
steps:
18-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
19-
with:
20-
fetch-depth: 0
21-
22-
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
23-
with:
24-
ssh-private-key: ${{ secrets.GITLAB_SSH_KEY }}
25-
26-
- name: Mirror to GitLab
27-
run: |
28-
ssh-keyscan -t ed25519 gitlab.com >> ~/.ssh/known_hosts
29-
git remote add gitlab git@gitlab.com:hyperpolymath/${{ github.event.repository.name }}.git || true
30-
git push --force gitlab main
31-
32-
mirror-bitbucket:
33-
runs-on: ubuntu-latest
34-
if: vars.BITBUCKET_MIRROR_ENABLED == 'true'
35-
steps:
36-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
37-
with:
38-
fetch-depth: 0
39-
40-
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
41-
with:
42-
ssh-private-key: ${{ secrets.BITBUCKET_SSH_KEY }}
43-
44-
- name: Mirror to Bitbucket
45-
run: |
46-
ssh-keyscan -t ed25519 bitbucket.org >> ~/.ssh/known_hosts
47-
git remote add bitbucket git@bitbucket.org:hyperpolymath/${{ github.event.repository.name }}.git || true
48-
git push --force bitbucket main
49-
50-
mirror-codeberg:
51-
runs-on: ubuntu-latest
52-
if: vars.CODEBERG_MIRROR_ENABLED == 'true'
53-
steps:
54-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
55-
with:
56-
fetch-depth: 0
57-
58-
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
59-
with:
60-
ssh-private-key: ${{ secrets.CODEBERG_SSH_KEY }}
61-
62-
- name: Mirror to Codeberg
63-
run: |
64-
ssh-keyscan -t ed25519 codeberg.org >> ~/.ssh/known_hosts
65-
git remote add codeberg git@codeberg.org:hyperpolymath/${{ github.event.repository.name }}.git || true
66-
git push --force codeberg main
67-
68-
mirror-sourcehut:
69-
runs-on: ubuntu-latest
70-
if: vars.SOURCEHUT_MIRROR_ENABLED == 'true'
71-
steps:
72-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
73-
with:
74-
fetch-depth: 0
75-
76-
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
77-
with:
78-
ssh-private-key: ${{ secrets.SOURCEHUT_SSH_KEY }}
79-
80-
- name: Mirror to SourceHut
81-
run: |
82-
ssh-keyscan -t ed25519 git.sr.ht >> ~/.ssh/known_hosts
83-
git remote add sourcehut git@git.sr.ht:~hyperpolymath/${{ github.event.repository.name }} || true
84-
git push --force sourcehut main
85-
86-
mirror-disroot:
87-
runs-on: ubuntu-latest
88-
if: vars.DISROOT_MIRROR_ENABLED == 'true'
89-
steps:
90-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
91-
with:
92-
fetch-depth: 0
93-
94-
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
95-
with:
96-
ssh-private-key: ${{ secrets.DISROOT_SSH_KEY }}
97-
98-
- name: Mirror to Disroot
99-
run: |
100-
ssh-keyscan -t ed25519 git.disroot.org >> ~/.ssh/known_hosts
101-
git remote add disroot git@git.disroot.org:hyperpolymath/${{ github.event.repository.name }}.git || true
102-
git push --force disroot main
103-
104-
mirror-gitea:
105-
runs-on: ubuntu-latest
106-
if: vars.GITEA_MIRROR_ENABLED == 'true'
107-
steps:
108-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
109-
with:
110-
fetch-depth: 0
111-
112-
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
113-
with:
114-
ssh-private-key: ${{ secrets.GITEA_SSH_KEY }}
115-
116-
- name: Mirror to Gitea
117-
run: |
118-
ssh-keyscan -t ed25519 ${{ vars.GITEA_HOST }} >> ~/.ssh/known_hosts
119-
git remote add gitea git@${{ vars.GITEA_HOST }}:hyperpolymath/${{ github.event.repository.name }}.git || true
120-
git push --force gitea main
121-
122-
mirror-radicle:
123-
runs-on: ubuntu-latest
124-
if: vars.RADICLE_MIRROR_ENABLED == 'true'
125-
steps:
126-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
127-
with:
128-
fetch-depth: 0
129-
130-
- name: Setup Rust
131-
uses: dtolnay/rust-toolchain@efa25f7f19611383d5b0ccf2d1c8914531636bf9 # stable
132-
with:
133-
toolchain: stable
134-
135-
- name: Install Radicle
136-
run: |
137-
# Install via cargo (safer than curl|sh)
138-
cargo install radicle-cli --locked
139-
echo "$HOME/.cargo/bin" >> $GITHUB_PATH
140-
141-
- name: Mirror to Radicle
142-
run: |
143-
echo "${{ secrets.RADICLE_KEY }}" > ~/.radicle/keys/radicle
144-
chmod 600 ~/.radicle/keys/radicle
145-
rad sync --announce || echo "Radicle sync attempted"
13+
mirror:
14+
uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@e6b2884722350515934d443daf23442f2195796f
15+
secrets: inherit

‎.github/workflows/scorecard.yml‎

Lines changed: 9 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,16 @@
11
# SPDX-License-Identifier: MPL-2.0
2-
name: OSSF Scorecard
2+
name: Scorecards supply-chain security
3+
34
on:
4-
push:
5-
branches: [main, master]
5+
branch_protection_rule:
66
schedule:
7-
- cron: '0 4 * * *'
8-
workflow_dispatch:
9-
10-
# Estate guardrail: cancel superseded runs so re-pushes don't pile up
11-
# queued analyses. Safe — Scorecard is read-only supply-chain analysis
12-
# with no publish or mutation (SARIF upload is idempotent).
13-
concurrency:
14-
group: ${{ github.workflow }}-${{ github.ref }}
15-
cancel-in-progress: true
7+
- cron: '23 4 * * 1'
8+
push:
9+
branches: [main]
1610

17-
permissions:
18-
contents: read
11+
permissions: read-all
1912

2013
jobs:
2114
analysis:
22-
runs-on: ubuntu-latest
23-
permissions:
24-
security-events: write
25-
id-token: write
26-
steps:
27-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
28-
with:
29-
persist-credentials: false
30-
31-
- name: Run Scorecard
32-
uses: ossf/scorecard-action@4eaacf0543bb3f2c246792bd56e8cdeffafb205a # v2.3.1
33-
with:
34-
results_file: results.sarif
35-
results_format: sarif
36-
37-
- name: Upload results
38-
uses: github/codeql-action/upload-sarif@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3.31.8
39-
with:
40-
sarif_file: results.sarif
15+
uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@e0caf11508a3989574713c78f5f444f2ce5e33ef
16+
secrets: inherit

‎CHANGELOG.md‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,68 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
2323
a two-level compositional convenience) — first slice of option
2424
(A) for the remaining `<ᵇ-+1` joint-bplus discharge; no
2525
rank-mono yet.
26+
- *Lane 3 head-Ω route — Slice 2 + Slice 2-omega + inversion + Slice 2-bplus
27+
ALL LANDED 2026-05-27.* Follow-on to the Slice 1 head-Ω landing above
28+
(PRs #130 + #131 + #133 + #134):
29+
- `Ordinal.Buchholz.RankPow` gains `ω-rank-pow-succ : OmegaIndex →
30+
Ord` with per-marker strict dominance at *both* branches
31+
(`ω-rank-pow-<-succ-fin` via `ω^-strict-mono-suc`;
32+
`ω-rank-pow-<-succ-omega` via the `Brouwer/OmegaPow.ω^-strict-mono-suc`
33+
template mirrored at `ω-rank-pow ω`) plus the unified
34+
`ω-rank-pow-<-succ : ∀ μ → ω-rank-pow μ <′ ω-rank-pow-succ μ`,
35+
plus atomic-rank factoring through `head-Ω`
36+
(`rank-pow-bOmega-via-head-Ω`, `rank-pow-bpsi-via-head-Ω`).
37+
- Slice 2-omega closes a Brouwer-encoding hazard the original
38+
CLAUDE.md proposal would have tripped: the proposed
39+
`ω-rank-pow-succ ω = olim (λ n → ω^(suc(suc n)))` is
40+
equi-ordinal with `ω-rank-pow ω = olim (λ n → ω^(suc n))`
41+
(both denote `ω^ω`), so cannot strictly dominate. The
42+
revised shape `olim (λ n → ω-rank-pow ω ·ℕ n)` denotes
43+
`ω^(ω+1)` and goes strictly higher via `X≤′oz⊕X` +
44+
`⊕-mono-<-right (ω-rank-pow-pos ω)`. Full record in
45+
`Ordinal.Buchholz.RankPow`'s "History note" block.
46+
- New module `Ordinal.Buchholz.HeadOmegaInversion` lands the
47+
option-(b) inversion lemmas `head-Ω-inv-bOmega` (strict) and
48+
`head-Ω-inv-bpsi` (non-strict). Both proved by structural
49+
recursion on the `<ᵇ` derivation; no rank-mono dependency.
50+
- New module `Ordinal.Buchholz.RankPowDomination` lands the
51+
Slice 2-bplus headline `rank-pow-dominated-by-head-Ω` by
52+
structural recursion on WfCNF, plus the supporting lemmas
53+
(`<′→≤′`, `≤′-<′-trans`, `<′-trans`, `ω-rank-pow-mono-≤Ω`,
54+
`ω-rank-pow-succ-pos`, `additive-principal-ω-rank-pow-succ`,
55+
`rank-y-bound`). PR #134 was the one-line explicit-implicit
56+
fix for the initial `ω≤ω` case of `ω-rank-pow-mono-≤Ω`.
57+
- *Decoration bridge — R5 exploratory entry scaffolded (PR #129).*
58+
`docs/echo-types/explorations/decoration-bridge/` lands a bounded
59+
exploration of whether the Choreo × Graded integration shape
60+
resembles adjacent-domain decoration constructions (CRDTs, gossip,
61+
local-first causal histories). Scope strictly the one axis pair
62+
`EchoIntegration.agda` already integrates; external candidates
63+
framed as analogies-with-falsifiers, never as evidence of recipe
64+
generalisation. Sits as `roadmap.adoc` § R5 (deferred research)
65+
with explicit termination criteria (Track A/B/C failure, all
66+
candidates retired, redundancy with retracted framing,
67+
forbidden-rebrandings register addition, retraction-watch trip).
68+
Companion Agda module `proofs/agda/EchoDecorationBridge.agda` —
69+
deliberately not in `All.agda`, classified as "Exploratory (not in
70+
All.agda)" in `docs/echo-types/echo-kernel-note.adoc` so CI's
71+
classification-drift lint stays green.
72+
- *Tier-1+2+3 spine + audience moves + suite + F5 FULL PASS
73+
LANDED 2026-05-27.* My session's contribution sitting on top of
74+
the parallel-session ordinal work above. See CLAUDE.md's
75+
"Slice-2 upstream adoption" + "broad-cleanup close" session arcs
76+
for the deliverable list; key headlines: `EchoTotalCompletion.A↔ΣEcho`,
77+
`EchoOrthogonalFactorizationSystem.ofs-witness`,
78+
`EchoNoSectionGeneric.no-section-of-collapsing-map`, the four
79+
Tier-2 classification-grid records (`ResidueForm` /
80+
`DecorationStructure` / function-side / observational), the
81+
Pillar F Gate F5 FULL PASS triple (F5-1 / F5-2 / F5-3) earning
82+
back the qualified OFS, four audience-facing modules
83+
(`EchoProvenance` / `EchoSecurity` / `EchoProbabilisticSupport`
84+
/ `EchoDifferential`), and the curated single-file entry
85+
`EchoCanonicalIdentitySuite`. Two consolidation narratives
86+
`docs/echo-types/{universal-property,fibration-package}.adoc`.
87+
Retraction follow-up F-2026-05-27a logged in `docs/retractions.adoc`.
2688
- *Lane 5 tutorial track — the originally-scaffolded triplet is
2789
complete.* `tutorial/` ships three worked walkthroughs with
2890
honest-bound disclosure at top + matched-negative `NotProved-*`

‎CLAUDE.md‎

Lines changed: 101 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1244,7 +1244,107 @@ explicitly scoped at the discrete / existence level — see each
12441244
module's companion-remark block before any "promote to universal"
12451245
work).
12461246

1247-
### Session arc 2026-05-27 evening — Lane 5 Walkthrough 3 landed (read this first)
1247+
### Session arc 2026-05-27 night — Lane 3 head-Ω Slice 2 landed (read this first)
1248+
1249+
*Where we started today (commit `65806f4` on `main`, post-#129):* the
1250+
PR #129 decoration-bridge scaffold landed under R5; Lane 3's head-Ω
1251+
domination route had Slice 1 (`HeadOmega.agda`) but no Slice 2 work.
1252+
The `<ᵇ-+1` joint-bplus case remained open with `head-Ω` defined but
1253+
not yet consumed by any rank-mono primitive.
1254+
1255+
*Where we ended today (commit `bf9ee6e` on `main`, post-#130):* Slice 2
1256+
lands the abstraction (`ω-rank-pow-succ` + the fin-branch strict
1257+
dominance) plus an honest obstruction note on the ω branch:
1258+
1259+
1. *`Ordinal.Buchholz.RankPow.agda` additions.*
1260+
* `ω-rank-pow-succ : OmegaIndex → Ord` — the per-marker "next
1261+
ω-power up" target. Fin branch is `ω^(suc(suc n))`; ω branch
1262+
reuses the original CLAUDE.md proposal `olim (λ n →
1263+
ω^(suc(suc n)))` so the abstraction is in place for follow-on
1264+
slices to inspect and (if needed) override.
1265+
* `ω-rank-pow-succ-fin` — definitional sanity at the fin branch.
1266+
* `ω-rank-pow-<-succ-fin` — per-marker strict dominance at fin
1267+
via `ω^-strict-mono-suc (suc n)`.
1268+
* `rank-pow-bOmega-via-head-Ω`, `rank-pow-bpsi-via-head-Ω` —
1269+
atomic-rank `refl`-shape primitives factoring `rank-pow` through
1270+
`head-Ω` for the two non-bplus, non-bzero `BT` constructors.
1271+
1272+
2. *`Ordinal.Buchholz.Smoke.agda` pinning.* Five headlines pinned
1273+
under their own `using` block with a header comment, per CLAUDE.md
1274+
Working rules.
1275+
1276+
*Obstruction note.* The originally-proposed CLAUDE.md shape
1277+
`ω-rank-pow-succ ω = olim (λ n → ω^(suc(suc n)))` represents the
1278+
**same** ordinal as `ω-rank-pow ω = olim (λ n → ω^(suc n))` — both
1279+
are `sup{ω^(n+1) : n ∈ ℕ} = ω^ω`, with different ℕ-indexings of the
1280+
same tail. Strict dominance at the ω branch therefore cannot hold
1281+
under that shape. Inline `RankPow.agda` comments document two
1282+
follow-on slices:
1283+
1284+
* *Slice 2-omega.* Replace the ω branch with a genuinely
1285+
strictly-larger ordinal. Candidate: `ω^(ω+1)` encoded as
1286+
`olim (λ n → (ω-rank-pow ω) ·ℕ n)`. Three cross-checks
1287+
documented inline before committing (closure under ordinal
1288+
addition; the consumer's actual additive-principal need; sanity-
1289+
check of the indexing's leading `oz ⊕` which is NOT definitionally
1290+
`ω-rank-pow ω` under Brouwer's right-recursing `_⊕_`).
1291+
* *Slice 2-bplus.* Prove the full
1292+
`rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t →
1293+
rank-pow t <′ ω-rank-pow-succ (head-Ω t)` by structural recursion
1294+
on WfCNF. The bplus case needs a `rank-pow-mono-≤ᵇ` companion for
1295+
the original `_<ᵇ_` (the WfCNF tail bound is `_≤ᵇ_`, not `_≤ᵇ⁰_`).
1296+
Marked `TODO(slice-2-bplus)` inline. Option (b) — head-Ω inversion
1297+
that does not transitively depend on rank-mono — is preferred
1298+
because it keeps `rank-pow-dominated-by-head-Ω` independent of
1299+
the companion so signature changes don't silently propagate.
1300+
1301+
Build invariant held: `proofs/agda/All.agda` + `proofs/agda/Smoke.agda`
1302+
+ `Ordinal/Buchholz/Smoke.agda` all exit 0 under `--safe --without-K`,
1303+
zero postulates, no funext. `scripts/kernel-guard.sh` PASS.
1304+
1305+
PR #130 was admin-merged before CI green at user direction; CI was
1306+
still all-12-queued at merge time. No CI failures have surfaced
1307+
since (treat any later red as authoritative if it does).
1308+
1309+
*Plan for the next Claude.*
1310+
1311+
Within this same session (2026-05-27 night, PR #131), items (1) and
1312+
(2) from the original plan also landed:
1313+
1314+
* *(1) Option (b) head-Ω inversion lemma — LANDED* (commit `560f904`).
1315+
New module `Ordinal.Buchholz.HeadOmegaInversion` ships
1316+
`head-Ω-inv-bOmega : bOmega ν <ᵇ y → ν <Ω head-Ω y` (strict) and
1317+
`head-Ω-inv-bpsi : bpsi ν α <ᵇ y → ν ≤Ω head-Ω y` (non-strict —
1318+
tracks the `<ᵇ-ψΩ≤` constructor). Pinned in
1319+
`Ordinal/Buchholz/Smoke.agda` under its own `using` block. Wired
1320+
into `All.agda`. No rank-mono dependency — that was the
1321+
load-bearing dependency-graph invariant the design called for.
1322+
* *(2) Slice 2-omega — LANDED* (commit `07abc15`). ω branch of
1323+
`ω-rank-pow-succ` replaced with `olim (λ n → ω-rank-pow ω ·ℕ n)`
1324+
(= `ω^(ω+1)`); per-marker strict dominance proved at the ω
1325+
branch via a mirror of `Brouwer/OmegaPow.ω^-strict-mono-suc`
1326+
(branch-index-2 + `X≤′oz⊕X` + `⊕-mono-<-right (ω-rank-pow-pos ω)`).
1327+
Unified `ω-rank-pow-<-succ : ∀ μ → ω-rank-pow μ <′
1328+
ω-rank-pow-succ μ` covers both branches.
1329+
1330+
Only one item remains open:
1331+
1332+
3. *Slice 2-bplus* — prove the full domination lemma
1333+
`rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t →
1334+
rank-pow t <′ ω-rank-pow-succ (head-Ω t)` by structural recursion
1335+
on the WfCNF carrier. Both per-marker dominances now hold; the
1336+
atomic cases discharge via `rank-pow-{bOmega,bpsi}-via-head-Ω` +
1337+
`ω-rank-pow-<-succ`. The bplus case consumes
1338+
`head-Ω-inv-{bOmega,bpsi}` from `HeadOmegaInversion` to pull
1339+
`head-Ω` bounds from the WfCNF tail's `<ᵇ` witness. No further
1340+
inversion-via-rank-mono dependency is introduced — that's what
1341+
option (b) bought.
1342+
1343+
DO NOT reopen: the closed 11/13 Buchholz constructors; the W1/W2/W3
1344+
walkthroughs; the R-2026-05-18 narrowings; the closed fin-branch /
1345+
ω-branch / unified dominances; the head-Ω inversion family.
1346+
1347+
### Session arc 2026-05-27 evening — Lane 5 Walkthrough 3 landed
12481348

12491349
*Where we started today (commit `4d77d75` on `docs/consolidate-roadmaps-
12501350
and-sigma-skepticism-2026-05-26`, post-#123):* the consolidation branch

‎EXPLAINME.adoc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ Per `.machine_readable/6a2/STATE.a2ml`:
3333
Ongoing tracks at a glance (point-in-time, see `roadmap.adoc` for the live status):
3434

3535
* *Identity claim.* `docs/retractions.adoc` R-2026-05-18 narrows the public claim to a *loss-graded reindexing modality* over a thin poset (not a graded comonad). Every newer artefact is stated within those narrowings.
36-
* *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. Remaining open case `<ᵇ-+1` joint-bplus has the `Ordinal.Buchholz.HeadOmega` first slice landed; rank-mono follow-ons designed. See `docs/echo-types/buchholz-rank-obstruction.adoc`.
36+
* *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. The remaining `<ᵇ-+1` joint-bplus case is now FULLY CLOSED (2026-05-27) via the head-Ω domination route: `head-Ω` (Slice 1) + `ω-rank-pow-succ` with per-marker strict dominance at both branches (Slice 2 + Slice 2-omega) + the option-(b) head-Ω inversion lemmas (`Ordinal.Buchholz.HeadOmegaInversion`) + the WfCNF-carrier structural recursion (Slice 2-bplus, `Ordinal.Buchholz.RankPowDomination.rank-pow-dominated-by-head-Ω`). See `docs/echo-types/buchholz-rank-obstruction.adoc`.
3737
* *Tutorial track (Lane 5).* Three worked walkthroughs under `tutorial/` (certified region-exit audit, epistemic erasure, provenance/debugging echo); each carries an honest-bound disclosure at the top and a matched-negative block at the bottom. The tutorial tree builds with the repo root added to the Agda include path; see `tutorial/README.adoc`.
3838
* *Establishment track (Pillar E).* Internal programme (Pillars A–D) complete since 2026-05-17. The paper (`docs/echo-types/paper.adoc`) is a living draft with remaining `[EXPAND]` tags; the venue + Zenodo + outreach plan sits in `docs/echo-types/pillar-e-offline.adoc` (author-driven).
3939

0 commit comments

Comments
 (0)