agda(B3): _<ᵇ⁺_ shared-binder lex constructors + WF design note + docs refresh#26
Merged
Merged
Conversation
Adds the two K-restricted shared-binder lex constructors that the top-of-Order.agda comment block flagged as "the next follow-up on top of WF-0": * <ᵇ⁺-ψα : bpsi ν α <ᵇ⁺ bpsi ν β when α <ᵇ β * <ᵇ⁺-+2 : bplus x y₁ <ᵇ⁺ bplus x y₂ when y₁ <ᵇ y₂ Each constructor carries an explicit equality witness for the shared binder so the four constructor implicits stay pairwise distinct — this avoids the reflexive ν=ν (or x=x) equation a shared-binder shape would force the K-free unifier through. The equality is matched on `refl` only inside `<ᵇ⁺-trans`, where both sides are fresh pattern variables (Cockx–Sjöberg criterion); in `<ᵇ⁺-irrefl` the equality is discarded as `_` because by then the LHS/RHS have been unified to a common carrier. Also fixes a dangling reference in commit e0f67cb: `All.agda` was updated to `open import Ordinal.Buchholz.OrderExtended` but the file itself was never committed. This commit ships the file. Headlines (pinned in Smoke.agda): * _<ᵇ⁺_ — extended order * <ᵇ⁺-base, <ᵇ⁺-ψα, <ᵇ⁺-+2 — constructors * <ᵇ⁺-irrefl, <ᵇ⁺-trans — proofs (mixed cases via four private extension helpers `bpsi-extend-{lhs,rhs}`, `bplus-extend-{lhs,rhs}`) * <ᵇ⁺-ψα-refl, <ᵇ⁺-+2-refl — convenience wrappers Well-foundedness for `_<ᵇ⁺_` is OPEN — see the new design note `docs/echo-types/buchholz-extended-wf.md` for the two routes (single-mutual restructure failed twice today; rank-embedding into Brouwer is the recommended next attempt and has scaffolding via `RankBrouwer.agda` from the parallel session). Verification: agda proofs/agda/All.agda and agda proofs/agda/Smoke.agda both exit 0 under --safe --without-K. No postulates introduced. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Five docs updated to reflect today's chain (C1, A2, A1, B3 — three
already merged, B3 in this PR):
* CLAUDE.md — current rung state replaced with the 4-rung
digest. Open list now flags _<ᵇ⁺_ WF (two failed Route-A
attempts, Route B recommended), Brouwer Phase 1.3 limit
case, unbudgeted _<ᵇʳᶠ_ WF.
* docs/echo-types/overview.md — Buchholz "what is not claimed"
paragraph refreshed: K-free core has WF, shared-binder lex
cases now internalised in `_<ᵇ⁺_`, WF for `_<ᵇ⁺_` is the
next open step.
* docs/echo-types/roadmap.md — cancel-iso marked landed (PR
#25); five-decoration sweep marked closed (PR #24);
Landauer/Bennett marked partial-landed for finite-domain
case (PR #23); _<ᵇ⁺_ marked partial.
* docs/echo-types/buchholz-extended-wf.md (NEW) — design note
explaining why `wf-<ᵇ` does not extend to `_<ᵇ⁺_` and the
two design routes (Route A: single-mutual block with widened
bundle, attempted twice today and blocked on Agda
termination; Route B: rank-embedding into Brouwer ordinals,
recommended next attempt with scaffolding via
RankBrouwer.agda). Pragmatic interim: `_<ᵇ_` and `_<ᵇ⁺_`
coexist as separate relations.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Records the full session chain with decisions made and why:
* C1 — `FiberSize-fin` defined as pure recursive enumeration
(no stdlib `count` shim); `bennett-reversible` parameterised
by `FiberSize-fin ≡ 1` rather than a `Bijection f` typeclass
input; infinite-domain `ProgramState = ℕ → ℕ` explicitly out
of scope.
* A2 — `_⊑c_` defined as a one-way order on roles (Client →
Server only) rather than an equivalence — keeps the join
structure non-trivial.
* A1 — packaged via stdlib's `Function.Bundles._↔_` and
`mk↔ₛ′`; per-fiber `(y : C) → ↔` rather than a global
equivalence object.
* B3 — separate relation `_<ᵇ⁺_` rather than extending `_<ᵇ_`
(preserves WF on the K-free core); explicit equality witness
on shared-binder constructors (sidesteps K-restriction);
four `extend-{lhs,rhs}` helpers for the mixed-shape trans
cases.
Plus a "what I'd do differently" retrospective: try Route B
first for `_<ᵇ⁺_` WF (rank-embedding has a clearer failure
mode than Agda's structural-decrease checker); always force
clean Agda rebuild via `find -name '*.agdai' -delete` before
each task switch.
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
1 participant
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
Why
Two parallel sessions today both attempted to add `<ᵇ-ψα` and `<ᵇ-+2` directly to `<ᵇ` and rebuild the WF proof as a single mutual block. Both attempts produce code that scope-checks but fails Agda's termination checker on the same cycle through `wf-<ᵇ`. The pragmatic interim is to keep the K-free core `<ᵇ` (with proven `wf-<ᵇ`) intact and define the lex extension in a sibling relation `<ᵇ⁺` whose well-foundedness is documented as the next open step.
What is NOT in this PR
Compile-verification
```
agda -i proofs/agda proofs/agda/All.agda
agda -i proofs/agda proofs/agda/Smoke.agda
```
Both exit 0 under `--safe --without-K`. No postulates introduced.
Test plan
🤖 Generated with Claude Code