Skip to content

docs: canonical echo-types Master Map (discoverability SoT)#54

Merged
hyperpolymath merged 3 commits into
mainfrom
docs/echo-types-master-map
May 18, 2026
Merged

docs: canonical echo-types Master Map (discoverability SoT)#54
hyperpolymath merged 3 commits into
mainfrom
docs/echo-types-master-map

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Why

~50 docs, several overlapping roadmaps (ProofRoadmap.md, PRIORITIZED_PROOF_ROADMAP.md, WORK_PLAN.md, roadmap.adoc, docs/echo-types/roadmap.md), no authoritative entry point, README not a nav hub. Real work (e.g. the Thermodynamic / Landauer-Bennett line on main) was effectively unfindable — even by the author, because working clones drift behind origin/main.

What

  • docs/echo-types/MAP.adoc — single source of truth. Every direction status-tagged ([REAL]/[REAL*]/[ROADMAP]/[OPEN]/[RETRACTED]/[CLOSED-NEG]), back-linked to its Agda modules + canonical docs. Resolves roadmap fragmentation (canonical = earn-back-plan + retractions; the rest marked pre-R-2026-05-18 historical). Distinguished from INDEX.adoc (audit index, different role). Living-doc maintenance contract included.
  • README.md — prominent front-door pointer.

Links, does not duplicate. Doc-only; respects retraction R-2026-05-18 governance. Wiki Home will mirror this and point back as SoT (follow-up).

🤖 Generated with Claude Code

Single source of truth for project structure/discoverability. ~50 docs
with several overlapping roadmaps and no authoritative entry point made
real work (Thermodynamic, etc.) effectively unfindable — even by the
author. docs/echo-types/MAP.adoc indexes every direction status-tagged
([REAL]/[ROADMAP]/[OPEN]/[RETRACTED]/[CLOSED-NEG]) and back-links proofs
+ canonical docs; resolves the roadmap fragmentation (canonical vs
pre-R-2026-05-18 historical); respects retraction governance. README
now front-doors it. Links, does not duplicate. Living doc.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 18, 2026
…ned proper-strict criterion

The obligation flagged open in RecipeNonTriviality.agda was
`Mode-is-loss-only : ¬ NonLossOnly ModeAxis`. That literal claim is
FALSE: the un-refined NonLossOnly counts reflexive identity steps, so
it is vacuously satisfied by every multi-inhabitant axis. This proves
the vacuity explicitly (NonLossOnly-holds-vacuously-for-Mode), then
sharpens the criterion to the intended irreflexive reading
(ProperNonLossOnly) and discharges the obligation in its defensible
form:

  * ChoreoAxis-proper-non-loss-only  -- positive case retained
  * Mode-is-not-proper-non-loss-only -- Mode loss-only, discharged

All --safe --without-K, zero postulates, zero escape pragmas; full
characteristic lane typechecks. EI-2 remains [CLOSED-NEG]
(terminated-negative) -- verdict unchanged.

Replanted onto true origin/main (2ca3122); prior push had drifted
onto PR #54's base and bundled README/MAP.adoc. This commit is the
proof change only.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath
Copy link
Copy Markdown
Owner Author

Status-tag request for docs/echo-types/MAP.adoc (this PR owns the file; raising here rather than duplicating it into a proof PR).

Two characteristic/EI status updates landed on origin/main via sibling work and should be reflected in the Master Map's Characteristic / EI section when convenient. Suggested lines to append after the existing EI-2 is [CLOSED-NEG] bullet:

* `[REAL]` 2026-05-18: the abstract loss-only obligation flagged open
  in `RecipeNonTriviality.agda` is discharged (PR #55). The un-refined
  `NonLossOnly` is shown vacuous (`NonLossOnly-holds-vacuously-for-Mode`);
  the sharpened irreflexive `ProperNonLossOnly` certifies Choreo
  (`ChoreoAxis-proper-non-loss-only`) and refutes Mode
  (`Mode-is-not-proper-non-loss-only`). EI-2 verdict unchanged.
* EI-2 *obligation 2* (READING 1 vs READING 2) is **closed by
  supersession** — see `EI2_REPORT.adoc` (reconciliation in a separate
  PR). READING 2 rejected as overstrong; READING 1 adopted in revised
  form. Not a live decision.

Both are doc-status only; neither reopens or weakens the terminated-negative EI-2 verdict. Posting as a comment (not a push to this branch) to avoid writing into a concurrent workstream.

Replace the status *snapshot* ("Known structural-fidelity gap…")
with a pure back-link to the authoritative loci — earn-back ledger
row B and docs/retractions.adoc F-2026-05-18b. MAP.adoc now carries
no duplicated item-B status, so it needs no edit when the ledger
moves (earned-back / residual / etc.) and cannot drift. This also
removes the cross-PR add/duplication: the item-B status update lands
solely via the ledger PR; MAP.adoc just points at it.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 18, 2026
The two same-binder Buchholz-order sub-cases (bpsi ν α <ᵇ bpsi ν β
with α <ᵇ β; bplus x y₂ <ᵇ bplus x z₂ with y₂ <ᵇ z₂) were ledgered
as "not constructible pending a K-free reformulation". Reconfirmed
the obstruction on Agda 2.8 (Order.agda cited 2.6.3): the *naive*
<ᵇ-irrefl matches x <ᵇ x, forcing the shared-binder deletion
ν =?= ν, which --without-K rejects.

New module Ordinal.Buchholz.OrderExtendedDirect defines the
extended direct relation _<ᵇᵈ_ carrying *both* same-binder
constructors and proves, --safe --without-K, zero postulates /
zero escape pragmas:

  * <ᵇ-irrefl  via generalised <ᵇ⇒≢ (distinct indices) discharged
                by cong-projection injectivity + the K-free conflict
                rule; refl is never matched, so deletion is never
                invoked;
  * <ᵇ-trans   full extended transitivity;
  * embed      conservativity: core Order._<ᵇ_ ↪ _<ᵇᵈ_ (faithful
                strict extension, not a redefinition).

Wired into All.agda, pinned in Smoke.agda; full + smoke build green.

Strictly scoped: WF of the direct relation remains a
termination-checker matter (not K) delivered via the
ExtendedOrder._<ᵇ⁺_ measure, which stays load-bearing; trichotomy
out of scope. No paper/conservativity/abstract claim moves — item B
is off the paper critical path. Logged as retraction follow-up
F-2026-05-18b; ledger row B / order / Status updated. MAP.adoc
status line deferred (tracked, exact patch recorded) to PR #54
which introduces MAP.adoc.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 18, 2026
…n (obl 5 fwd) (#61)

**Stacked on #55** (base = \`feat/mode-loss-only-proper-strict\`).
Re-target to \`main\` after #55 squash-merges. Single file changed:
\`proofs/agda/characteristic/RecipeNonTriviality.agda\`.

Discharges two residual EI-2 obligations in their defensible form, in
the same formal shape as the existing n=2 exhibits:

### Obligation 4 — n=3 concrete enumeration
- \`rmg-cell-action\`, \`rmg-cell-action-equals-c2s\`,
\`RoleModeGrade-has-non-trivial-cell\`,
\`recipe-non-triviality-concrete-n3\`.
- Mechanical extension of the concrete enumeration to the 3D
\`RoleModeGrade\` construction. Reuses
\`RoleModeGrade.trace-non-trivial-cell\`; adds no new mathematical
content beyond the \`PreservesDistinct\` certificate + enumeration entry
(link, don't duplicate).

### Obligation 5 — generic FORWARD half
- \`ProperNonLossOnly⇒distinguishing-step\` and
\`generic-2cell-forward\` (composition with any **pointwise-identity**
second-axis step — no function extensionality).
- \`choreo-instantiates-generic-forward\` links the concrete cells to
the generic statement (non-vacuity witness).
- Shows the forward direction needs **neither** decidable equality on D
**nor** a live decoration — a *sharpening* of the file's own §abstract
meta-claim.
- The **reverse** half remains walled by extensionality under \`--safe\`
(unchanged; documented).

### Invariants
- EI-2 verdict **UNCHANGED** (\`[CLOSED-NEG]\` / PATH B): neither
reopened nor terminated. Residual obligations discharged exactly as the
proper-strict sharpening discharged the loss-only obligation.
- Honours retraction **R-2026-05-18** (no retracted vocabulary).
- Full \`characteristic\` lane typechecks \`agda --safe --without-K\`;
zero postulates, zero escape pragmas (verified).

MAP.adoc status delta posted as a comment on #54 (MAP.adoc is owned by
#54; not bundled here, to avoid cross-PR contamination).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 73f9345 into main May 18, 2026
10 of 11 checks passed
@hyperpolymath hyperpolymath deleted the docs/echo-types-master-map branch May 18, 2026 08:46
hyperpolymath added a commit that referenced this pull request May 18, 2026
…in O-THERMO-∞ (#58)

## What

Advances the **Thermodynamic — Landauer/Bennett** direction from its
~70% / C+ rating by closing the one concrete gap that drove that rating
and converting the residual into a single *falsifiable* obligation.

The C+ gap was specific: the only proved zero-cost (Bennett) instance
was `bennett-reversible-id-zero` — the **identity map, at index zero**.
`ThermodynamicOptimality(p) := fiber-erasure-bound p σ _≟_ T ≡ 0` was
otherwise unproved off that single point.

### Closed cases (proved)

All `--safe --without-K`, **zero postulates, zero escape pragmas**;
`proofs/agda/All.agda` + `proofs/agda/Smoke.agda` re-verify exit 0.

- `EchoFiberCount.FiberSize-fin-injective` — any injective
  `f : Fin n → B` that hits `y` has fiber size exactly `1`
  (generalises `FiberSize-fin-id-zero` off the identity *and* off
  index zero).
- `EchoThermodynamics.bennett-reversible-injective` — zero erasure
  bound for **every injective map** at every value it hits;
  `bennett-reversible-id-zero` is now a corollary.
- `EchoThermodynamicsFinite` (new) — names the exact blocker to
  generalising past `Fin n` (`fiber-erasure-bound` is routed through
  `FiberSize-fin`, whose totality is structural recursion on the `Fin`
  index bound) and removes it for **any Bishop-finite carrier** via
  transport along an explicit bijection (record `FiniteDomain`):
  `bennett-reversible-finite`, `landauer-collapse-finite`.

### Stated falsifiable obligation

- **O-THERMO-∞** (`docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic
  Bridge"): no `--safe`-total cost functional on an infinite carrier
  (`ProgramState = ℕ → ℕ`) can agree with `fiber-erasure-bound` on the
  finite restrictions. Stated with an explicit **kill condition**
  (exhibit such a `cost`, or mechanise the impossibility) — not
  softened to "future work".

## Honours retraction R-2026-05-18

Orthogonal to the retracted graded-comonad / two-models /
conservativity / universal-property / funext claims. No retracted
claim reinstated; no Agda module weakened or edited.

## Docs (same PR)

- `docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge" — proved
  generalisations, O-THERMO-∞, Theorem 4, AZ mapping row.
- `docs/STABILITY_ANALYSIS.md` §3.3 + coverage matrix — C+ 70% → B-
  85%, single residual named.
- `docs/echo-types/MAP.adoc` — Thermodynamic Directions entry + status
  tag (governance rule). Stays `[REAL*]` (real, still partial) until
  O-THERMO-∞ is discharged or refuted.

## Base

Stacked on `docs/echo-types-master-map` (PR #54) because `MAP.adoc`
does not exist on `main` yet and the governance rule requires the
status-tag update in the same PR. Re-target to `main` once #54 lands.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 18, 2026
…ive (#60)

Thermodynamic-bridge continuation. **Stacked on PR #58** (base =
`thermo/bennett-injective-finite-stack-2026-05-18`, itself on PR #54
`docs/echo-types-master-map`). Depends on #58's
`bennett-reversible-injective` / `FiberSize-fin-injective` /
`FiberSize-fin-const` and on MAP.adoc (only on the #54 branch).

**Re-target chain:** #54→main, then #58→main, then **this PR→main**.
(Automated poll armed; merges out-of-band.)

This PR closes the thermodynamic pillar: **no open obligation remains**
for the Thermodynamic Direction (`[REAL*]` → `[REAL]`, B- → B / ~95%).

## Part 1 — Bennett zero-cost on an arbitrary carrier (Steps 1–3)

The finiteness in PR #58 / `EchoThermodynamicsFinite` was an artefact of
routing cost through `FiberSize-fin` (an enumeration); Bennett's
physical content (no fan-in) needs no finiteness.

1. **`FiberSubsingleton` + `injective⇒fiber-subsingleton`** — K-free
`--without-K`-safe "no fan-in" predicate, for an **arbitrary** carrier
`A : Set a`. (Full fibre `isProp` would need `B` an h-set/UIP,
unavailable under `--without-K`; the first-projection form is what the
count needs.)
2. **`bennett-reversible-arbitrary`** — Bennett zero-cost for every
injective map on **any** carrier, no `Fin`/`FiniteDomain`, via an
occupancy-keyed `reversible-erasure-cost`. **Anti-vacuity:**
`occupancy≡FiberSize-fin` + `bennett-arbitrary-refines-finite` prove it
coincides with and strictly subsumes #58's established count.
3. **`bennett-reversible-cno-identity`** — instantiated at `cno-identity
: Program → Program` over the genuine **infinite** absolute-zero
`Program` carrier: "a CNO dissipates zero Landauer energy" is now a real
theorem, not the historically vacuous claim.

`EchoFiberCount` gains `FiberSize-fin-subsingleton`
(`FiberSize-fin-injective` is its corollary; kept as-is upstream for pin
stability).

## Part 2 — O-THERMO-∞ discharged negatively → `[CLOSED-NEG]`

Route (a): mechanise the impossibility. `EchoThermoCollapseImpossible`
proves the obligation's **own kill condition, second horn — (i)∧(ii) ⊢ ⊥
— verbatim**, for its named witness:

- `nat-into-collapse-fiber{-injective}`: `ℕ ↪ Echo (const y₀) y₀` — the
collapse fiber is infinite (the structural reason no finite count
exists).
- `collapse-cost-impossible`: any total `--safe` `cost` agreeing with
`fiber-erasure-bound` on every finite restriction of the constant map is
impossible — clause (ii) at `n = 1, 2` (`T = 1`, via
`FiberSize-fin-const`) forces its single value to be both `0` and `1`.

The quantitative-collapse functional provably does **not** extend to an
infinite carrier as a total `--safe` function: a settled negative
boundary, **not** a softened "future work" item and **not** a defect.
Orthogonal to the Bennett zero direction (closed for all carriers, Part
1).

## Verification

- All `--safe --without-K`, **zero postulates, zero escape pragmas**
(the lone `postulate` string is the comment false-positive class —
EchoKernel precedent).
- `Smoke.agda` + `All.agda` typecheck (exit 0); all new headlines pinned
in `Smoke.agda`.
- Governance docs updated same PR per the MAP rule:
`ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge" (O-THERMO-∞ →
`[CLOSED-NEG]`), `STABILITY_ANALYSIS.md` §3.3 (B / ~95%, with explicit
rationale for the freeze-lift), `docs/echo-types/MAP.adoc` (`[REAL*]` →
`[REAL]`, proofs list).

Honours retraction R-2026-05-18 — orthogonal; nothing retracted is
reinstated. The separate Information-Theory bridge (Theorem 5) remains
unbuilt by design — a different Direction.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath
Copy link
Copy Markdown
Owner Author

MAP.adoc status delta — characteristic / EI lane (from #55, which now also bundles #61)

No change to the EI-2 tag itself: it stays [CLOSED-NEG] (terminated negative — not reopened, not weakened). This note is only so the MAP owner can fold the residual-obligation progress into the Characteristic / EI section if desired; nothing here requires a MAP edit.

Residual EI-2 obligations, updated state (all --safe --without-K, zero postulates, zero escape pragmas; full characteristic lane typechecks):

Loss-only abstract obligation: discharged in #55 via the sharpened irreflexive ProperNonLossOnly (Mode-is-not-proper-non-loss-only).

Honours retraction R-2026-05-18 (no retracted vocabulary).

hyperpolymath added a commit that referenced this pull request May 18, 2026
… proper-strict criterion) (#55)

## Summary

Discharges the abstract loss-only obligation flagged open in
`proofs/agda/characteristic/RecipeNonTriviality.agda` (`--
Mode-is-loss-only : ¬ NonLossOnly ModeAxis -- ^^^ open obligation`).

The literal claim `¬ NonLossOnly ModeAxis` is **false**: the un-refined
`NonLossOnly` counts *reflexive* identity steps as "strict", so it is
vacuously satisfied by every axis with a multi-inhabitant decoration.
Rather than paper over the gap, this PR:

1. **Proves the vacuity explicitly** —
`NonLossOnly-holds-vacuously-for-Mode`.
2. **Sharpens the criterion** to the intended irreflexive reading (cf.
`ChoreoInjective.agda`: "strict (non-reflexive) steps") —
`ProperlyStrict` / `ProperNonLossOnly`.
3. **Retains the positive case** — `ChoreoAxis-proper-non-loss-only`.
4. **Discharges the obligation** — `Mode-is-not-proper-non-loss-only`.

## Verification
- `--safe --without-K`, **zero postulates, zero escape pragmas**.
- Full characteristic lane typechecks (`agda -i proofs/agda
proofs/agda/characteristic/All.agda`, exit 0) on a clean
true-`origin/main` base.

## Scope
- **EI-2 unchanged**: remains `[CLOSED-NEG]` (terminated-negative). Not
reopened.
- Retraction **R-2026-05-18** honoured — no retracted vocabulary
reinstated.
- Commit author = 6759885+hyperpolymath@users.noreply.github.com.

## Note: branch replanted
This branch was force-updated. The earlier push had drifted onto
**#54**'s base (`docs/echo-types-master-map`) and bundled `README.md` +
the whole `docs/echo-types/MAP.adoc` — not part of this change. It is
now replanted onto true `origin/main` (`2ca3122`) and contains the
**single Agda proof file only**. The MAP.adoc status tag for this work
is posted as a review comment on #54 (which owns that file), per "link,
don't duplicate".

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 18, 2026
…ing (#59)

## Summary

`docs/EI2_REPORT.adoc` contained a self-contradiction: its *concrete
next steps* listed obligation 2 (decide READING 1 vs READING 2) as
*"partial / Decision pending / obligation 2 remains open"*, while the
**same file's** authoritative Status line and supersession NOTE record
EI-2 as terminated and the reading question as settled.

This reconciles the stale text with the authoritative record:

- Both readings shared the premise that *non-loss-only is sufficient*
for substantive cross-axis interaction.
- `RoleRole.agda` refuted that premise (NLO necessary but **not**
sufficient).
- On record: **READING 2 rejected as overstrong; READING 1 adopted in
revised form**, distinctness rerouted to truncation + 2-cell arguments.
- Obligation 2 is therefore marked **RESOLVED (superseded; no live
choice)**; the candidate-patch files are reframed as historical record
only.

## Scope
- **Documentation reconciliation only.** No Agda touched.
- Does **not** reopen or weaken the terminated-negative EI-2 verdict
(`[CLOSED-NEG]`); it removes the only load-bearing contradiction
*reinforcing* that verdict.
- Single file, off true `origin/main` (`2ca3122`). Independent of
#54/#55.
- Commit author = 6759885+hyperpolymath@users.noreply.github.com.

Companion: MAP.adoc status tag for this requested as a review comment on
#54 (which owns that file).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 18, 2026
#57 reduced to its sole content not already in main: the new module
proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda (225 lines) +
Smoke pins + All.agda registration. F1/F4/F2 spikes and the doc
reframes from the original branch were superseded by #54/#55/#56/#58/#60
(present in main, byte-identical) and the Nix-flake commit dropped
(Guix-primary policy). Typechecks --safe --without-K, zero postulates;
full All.agda + Smoke + characteristic + examples suites green.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity Count
🔴 Critical 0
🟠 High 5
🟡 Medium 5
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 quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "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": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 4 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

hyperpolymath added a commit that referenced this pull request May 18, 2026
## Summary

Earns back the **K-attributed part of proof-debt ledger item B**
(Buchholz order). Item B held that the two same-binder sub-cases
(`bpsi ν α <ᵇ bpsi ν β` with `α <ᵇ β`; `bplus x y₂ <ᵇ bplus x z₂`
with `y₂ <ᵇ z₂`) were *"not constructible pending a K-free
reformulation"*.

- **Reconfirmed** the obstruction on **Agda 2.8** (the `Order.agda`
  comment cited 2.6.3): the *naive* `<ᵇ-irrefl` matching `x <ᵇ x`
  forces the shared-binder deletion `ν =?= ν`, rejected `--without-K`.
- **New module** `Ordinal.Buchholz.OrderExtendedDirect` (`_<ᵇᵈ_`)
  carries **both** same-binder constructors and proves, `--safe
  --without-K`, **zero postulates / zero escape pragmas**:
  - `<ᵇ-irrefl` via generalised `<ᵇ⇒≢` (distinct indices) discharged
    by `cong`-projection injectivity + the K-free **conflict** rule —
    `refl` is never matched, so the deletion rule is never invoked;
  - `<ᵇ-trans` (full extended transitivity);
  - `embed : Order._<ᵇ_ ⇒ _<ᵇᵈ_` — conservativity (faithful strict
    extension, not a redefinition).
- Wired into `All.agda`, pinned in `Smoke.agda`; **full + smoke build
  green** locally (Agda 2.8, stdlib v2.3).

## Scope (rigorous, not over-claimed)

- This is **not** `[CLOSED-NEG]`: the K-free reformulation **did not
  resist** — it succeeded.
- WF of the direct relation is **out of scope**: a termination-checker
  matter (Routes A/B of `buchholz-extended-wf.md`), orthogonal to K,
  still delivered via the `ExtendedOrder._<ᵇ⁺_` measure, which stays
  load-bearing. Trichotomy/totality out of scope.
- **No paper / conservativity / abstract claim moves** — item B is off
  the paper critical path. Logged as retraction follow-up
  **F-2026-05-18b**; ledger row B / recommended-order / Status updated.

## Notes

- **Base:** `earn-back/f4-f2-2026-05-18` (PR #50, unmerged) — the
  earn-back ledger + `F-2026-05-18a` live there; this work edits those
  files so it must stack on #50, not `main`.
- **MAP.adoc:** not on `main` (introduced by open PR #54). To avoid an
  add/add duplication, the item-B status line is **not copied**; the
  exact one-line replacement is recorded in `docs/retractions.adoc`
  (F-2026-05-18b) as a tracked follow-up to apply in/after #54.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant