diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index 524f39d..12947a2 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -115,7 +115,7 @@ jobs: # source change or absolute-zero bump; restore-keys give a warm # partial cache even when it does. - name: Cache Agda interface files - uses: actions/cache@v4 + uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4 with: path: | ~/agda-stdlib/**/*.agdai diff --git a/.zenodo.json b/.zenodo.json new file mode 100644 index 0000000..9162296 --- /dev/null +++ b/.zenodo.json @@ -0,0 +1,30 @@ +{ + "title": "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)", + "upload_type": "software", + "description": "Constructive Agda formalisation of fibre-based \"structured loss\" types. Defines Echo f y := Σ (x : A) , (f x ≡ y), shows it is definitionally the homotopy fibre (echo↔fib), and develops a loss-graded reindexing modality on top with a pointwise (funext-relative) mediator property, a separating model, and a carrier-parametric abstraction over a fixed grade poset. Under --safe --without-K throughout with zero postulates and a falsifiable retraction discipline.", + "creators": [ + { + "name": "Jewell, Jonathan" + } + ], + "keywords": [ + "agda", + "graded modality", + "homotopy fibre", + "structured loss", + "reindexing modality", + "formal methods", + "mechanised metatheory", + "echo types" + ], + "access_right": "open", + "license": "MPL-2.0", + "related_identifiers": [ + { + "relation": "isSupplementTo", + "identifier": "https://github.com/hyperpolymath/echo-types", + "resource_type": "software" + } + ], + "communities": [] +} diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 0000000..67caf5f --- /dev/null +++ b/CITATION.cff @@ -0,0 +1,43 @@ +cff-version: 1.2.0 +title: "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)" +message: "If you cite this software, please cite the Zenodo DOI." +type: software +authors: + - given-names: Jonathan + family-names: Jewell + email: jonathan.jewell@gmail.com + # PLACEHOLDER: insert ORCID once registered, e.g. + # orcid: "https://orcid.org/0000-0000-0000-0000" +repository-code: "https://github.com/hyperpolymath/echo-types" +url: "https://github.com/hyperpolymath/echo-types" +abstract: > + Constructive Agda formalisation of fibre-based "structured loss" + types. Defines Echo f y := Σ (x : A) , (f x ≡ y), shows it is + definitionally the homotopy fibre (echo↔fib), and develops a + loss-graded reindexing modality on top with a pointwise + (funext-relative) mediator property, a separating model, and a + carrier-parametric abstraction over a fixed grade poset. Under + --safe --without-K throughout with zero postulates and a + falsifiable retraction discipline. See paper.adoc and + types-abstract.adoc for the mechanised metatheory write-up. +keywords: + - agda + - graded modality + - homotopy fibre + - structured loss + - reindexing modality + - formal methods + - mechanised metatheory +license: MPL-2.0 +# === PLACEHOLDER: paste concept DOI here after first Zenodo mint === +doi: 10.5281/zenodo.0000000 +# === END PLACEHOLDER === +preferred-citation: + type: software + title: "echo-types: a definitionally-grounded, loss-graded reindexing modality (Agda)" + authors: + - given-names: Jonathan + family-names: Jewell + url: "https://github.com/hyperpolymath/echo-types" + doi: 10.5281/zenodo.0000000 + year: 2026 diff --git a/CLAUDE.md b/CLAUDE.md index f973cc7..96f49df 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -176,7 +176,7 @@ work to `main` and refresh all documentation: dependency order. Resolve any conflicts (typically additive, in `Smoke.agda` and `All.agda`). 3. **Update human docs.** `docs/echo-types/composition.md`, - `docs/echo-types/roadmap.md`, `docs/echo-types/overview.md` and + `roadmap.adoc`, `docs/echo-types/overview.md` and `cross-repo-bridge-status.md` get a sweep for stale `(Open)` / `[unblocked]` tags on anything that just landed. Honest labels: `(Landed)`, `(Partial)`, `(Open)`. @@ -191,7 +191,165 @@ work to `main` and refresh all documentation: name, the commits folded in, the remaining open pieces of the milestone, and the proposed smallest useful next advance. -## Current rung state (2026-05-20) +## Current rung state (2026-05-27) + +### Session arc 2026-05-27 evening — Lane 5 Walkthrough 3 landed (read this first) + +*Where we started today (commit `4d77d75` on `docs/consolidate-roadmaps- +and-sigma-skepticism-2026-05-26`, post-#123):* the consolidation branch +carried Walkthroughs 1 (region-exit audit) and 2 (epistemic erasure) +plus the Lane 3 `RankLex` slice closing `<ᵇ-ψΩ≤`. Walkthrough 3 +(provenance / debugging) was at scaffold/design-doc level in +`tutorial/README.adoc`. The originally-scaffolded Lane 5 triplet was +two-thirds landed. + +*Where we ended today:* Walkthrough 3 LANDS — the originally-scaffolded +triplet is complete in Agda. One slice: + +1. *Walkthrough 3 — provenance / debugging echo* lands at + `tutorial/provenance_debugging/`. Domain: 4-element `State` with + two orthogonal sign bits (`firstSign`, `secondSign`); `firstSign` + is the echo's visible output, `secondSign` is the class predicate + the layer-1 residue carries. Three residue layers walked: + * Layer 0 — `Echo firstSign true`, distinguishing all sources; + * Layer 1 — `EchoR Bool ClassCert true` carrying `secondSign`; + * Layer 2 — `EchoR ⊤ TrivialCert' true` carrying nothing. + Headlines: `states-distinct-at-true` (Layer 0 distinguishes); + `classes-remain-distinct` (Layer 1 still distinguishes); + *`recover-section-at-layer-1`* (POSITIVE — Layer 1 has a section); + `trivials-collapse` (Layer 2 collapses); *`no-recovery-from-trivial`* + (NEGATIVE — Layer 2 has no section, structural mirror of + `EchoResidue.no-section-collapse-to-residue`); and + `provenance-walk-contrast` packaging the section / no-section pair. + + *New pedagogical shape vs W1/W2.* Walkthroughs 1 and 2 each ship a + one-sided no-section result. Walkthrough 3 ships *both* a section + (at layer 1) and its absence (at layer 2), exhibiting the boundary + at which the type-level recovery property flips. The mechanical + load: `secondSign` is *injective within each `firstSign`-fibre*, + which is exactly the property the layer-1 section needs. + + *Honest bound discipline inherited from W2.* The Agda file and the + README both open with the disclosure that this is type-level only — + no operational debugger, no runtime artefacts, fixed 4-element + domain. A `NotProved-*` matched-negative block at the file's + bottom lists four out-of-scope properties (runtime debugger, + reconstruction in general, completeness across classes, recovery + under side information) as `⊤`-aliases so `grep NotProved` catches + them. + + *Files landed.* + * `tutorial/provenance_debugging/ProvenanceDebugging.agda` (worked + example); + * `tutorial/provenance_debugging/Smoke.agda` (per-walkthrough Smoke + pins, own `using` block, header comment); + * `tutorial/provenance_debugging/All.agda` (aggregator); + * `tutorial/provenance_debugging/README.adoc` (narrative). + * `tutorial/All.agda` registers the new walkthrough. + * `tutorial/README.adoc` §"Walkthrough 3" flipped from design-doc + status to LANDED 2026-05-27; the IMPORTANT scaffold-status note + updated. + +Build invariant held: `proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, +`tutorial/All.agda`, and `tutorial/provenance_debugging/Smoke.agda` +all exit 0 under `--safe --without-K`, zero postulates, no funext. +All headlines pinned in the per-walkthrough Smoke under their own +`using` block per CLAUDE.md "Working rules". + +*Plan for the next Claude.* The originally-scaffolded Lane 5 triplet +is complete. Open work: + +1. *Lane 3 follow-on — `<ᵇ-+1` joint-bplus.* The one remaining open + per-constructor case in the Buchholz rank-mono umbrella. Closure + options documented in `RankPow.agda` and the obstruction doc: + (A) leading-Ω-index dominator (`head-Ω : BT → OmegaIndex`), + recommended; (B) richer rank shape on `bplus`. Smallest useful + first slice = define `head-Ω` + definitional sanity lemmas only, + no rank-mono. Multi-session work. +2. *Lane 5 unparking decision (user).* Walkthroughs 1+2+3 all + landed; Walkthrough 1 is the killer-app candidate per + `roadmap.adoc` §Lane 5 second unblocking condition. User + accept-or-defer pending; the lane remains [PARKED] at the lane- + policy level until the user decides. +3. *Pillar E paper [EXPAND] clearing.* Gated on author-driven + material accruing. + +DO NOT reopen: the closed 11/13 Buchholz constructors (their +primitives are correct under WfCNF + admissibility + lex-pair); +the W1/W2 walkthroughs (their no-section headlines are the existing +`EchoLinear.no-section-weaken` and `EchoResidue.no-section-collapse- +to-residue` re-exported with honest-bound + matched-negative +discipline); the R-2026-05-18 narrowings. + +### Session arc 2026-05-27 late evening — Lane 3 head-Ω first slice + +*Where we started today (commit `04f3d9f`, post-W3):* the consolidation +branch carried the complete Lane 5 triplet (W1/W2/W3) plus the 11/13 +Buchholz constructor closure via `rank-pow` + `rank-adm` + `rank-lex`. +The one remaining open per-constructor case `<ᵇ-+1` joint-bplus +sits behind a documented structural blocker +(`docs/echo-types/buchholz-rank-obstruction.adoc` §"What remains +open"): `rank-pow (bplus z₁ z₂)` is not additive principal in +general. + +*Where we ended today:* option (A) from `RankPow.agda`'s preamble +opens via the head-Ω abstraction. One slice: + +1. *`Ordinal.Buchholz.HeadOmega.agda`* — the leading-Ω-index head + function `head-Ω : BT → OmegaIndex`: + * `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`) plus one two-level compositional convenience + (`head-Ω-bplus-left`) for the WfCNF left-spine pattern. + Pinned in `Ordinal/Buchholz/Smoke.agda` under own `using` block + with header comment; wired into `proofs/agda/All.agda` between + `RankLex` and `RankMonoUmbrella`. + + *Smallest useful first slice.* No rank-mono in this slice; the + domination lemma `rank-pow t <′ ω-rank-pow-succ (head-Ω t)` and + the headline `<ᵇ-+1` joint-bplus discharge are explicitly + deferred to follow-on slices per `HeadOmega.agda`'s preamble. + The abstraction stands on its own merits before any rank + consumer pulls on it. + +Build invariant held: `Ordinal/Buchholz/Smoke.agda`, +`proofs/agda/Smoke.agda`, and `proofs/agda/All.agda` all exit 0 +under `--safe --without-K`, zero postulates, no funext. All +headlines pinned in the Buchholz-layer Smoke under their own +`using` block per CLAUDE.md "Working rules". + +*Plan for the next Claude.* Continue option (A): + +1. *Slice 2 — ω-rank-pow-succ + the domination lemma.* Add + `ω-rank-pow-succ : OmegaIndex → Ord` to `RankPow.agda` (one + option: `ω-rank-pow-succ (fin n) = ω^(suc (suc n))`, + `ω-rank-pow-succ ω = olim (λ n → ω^(suc (suc n)))`), then prove + `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t → + rank-pow t <′ ω-rank-pow-succ (head-Ω t)` by structural recursion + on the WfCNF carrier, applying `rank-pow-bplus-into-ω-rank-pow` + at each `bplus` step. This is the load-bearing slice. +2. *Slice 3 — the headline `rank-mono-<ᵇ-+1-via-head-Ω`.* Builds + on Slice 2 + `rank-mono-<ᵇ-+1-via-target` from `RankPow.agda`. + At consumer time: head-Ω inversion on the target's left summand + gives the additive-principal witness; source `bplus`'s rank is + dominated by `ω-rank-pow-succ (head-Ω source)`, which by + `head-Ω-bplus` equals `ω-rank-pow-succ (head-Ω x₁)`, strictly + below the target's rank via the `<ᵇ` premise. +3. *Slice 4 — full `rank-pow-mono-<ᵇ⁻` umbrella.* Composition of + the head-Ω discharge with the existing 11-constructor closures. + The final Buchholz rank-monotonicity theorem under the WfCNF + restriction. + +DO NOT reopen: `head-Ω` returns `fin 0` on `bzero` as a deliberate +default — future rank-mono lemmas guard the `bzero` case via the +non-bzero premise, so the default is never consumed in a proof +context. Changing the default to `Maybe OmegaIndex` would force +every downstream caller through an unwrap; the documented +non-bzero guard is the cleaner discipline. ### Session arc 2026-05-20 daytime (theory closure waves 1 + 2 + 3) @@ -503,7 +661,8 @@ coeffects, lens/optic vs the witness-transport leg); (3) evaluation (proof-size/cost table; quantify common-upper-bound idiom vs naive `subst`); (4) ordinal consumer-evidence appendix — GATED on the ordinal track hitting Bachmann–Howard, keep firewalled per -`roadmap.md`. THEN offline/author-driven only (venue+template, +`roadmap.adoc` §Lane 3 (Ordinal track) and `docs/buchholz-plan.adoc`. +THEN offline/author-driven only (venue+template, Zenodo DOI, library packaging, outreach) — flag to the user, do NOT auto-run. Strategy (user decision 2026-05-17): the paper was written now at full narrative strength while fresh; expand the tagged @@ -590,7 +749,8 @@ tags as material becomes available, in this order: 3. Evaluation — proof-size/cost table; quantify common-upper-bound-idiom vs naive `subst`. 4. Ordinal consumer-evidence appendix — gated on that track hitting - its Bachmann–Howard milestone (firewalled per roadmap.md). + its Bachmann–Howard milestone (firewalled per `roadmap.adoc` + §Lane 3 and `docs/buchholz-plan.adoc`). 5. THEN offline/author-driven: venue+template, Zenodo DOI, library packaging, outreach — flag to user, do NOT auto-run. diff --git a/DOCUMENTATION_STATUS.md b/DOCUMENTATION_STATUS.md index 92ee361..886fc66 100644 --- a/DOCUMENTATION_STATUS.md +++ b/DOCUMENTATION_STATUS.md @@ -6,7 +6,7 @@ 1. **Core Bridge Documentation** - `docs/EchoJanusBridge.md` - Comprehensive explanation of echo types → JanusKey bridge - - `docs/ProofRoadmap.md` - Strategic proof development roadmap + - `roadmap.adoc` §"Deferred research track" - Strategic proof development roadmap (consolidated from former `docs/ProofRoadmap.md`) - `docs/COMPREHENSIVE_DOCUMENTATION.md` - Complete 3-2-1 structured documentation 2. **Formal Proofs** @@ -84,7 +84,7 @@ - [x] Create `EchoJanusBridge.agda` with core theorems - [x] Update `All.agda` to include new module - [x] Write `EchoJanusBridge.md` documentation -- [x] Create `ProofRoadmap.md` for future work +- [x] Consolidate `ProofRoadmap.md` into `roadmap.adoc` (single canonical roadmap) - [x] Develop `COMPREHENSIVE_DOCUMENTATION.md` (3-2-1 structure) - [x] Verify Agda proofs compile successfully - [ ] Add architecture diagrams diff --git a/README.md b/README.md index 5381197..325bdd2 100644 --- a/README.md +++ b/README.md @@ -79,7 +79,15 @@ Scope-broadening stages now include: - indexed/relational/categorical packaging (`EchoIndexed`, `EchoRelational`, `EchoCategorical`, `EchoScope`) - cross-ecosystem bridges (`EchoCNOBridge`, `EchoJanusBridge`, `DyadicEchoBridge`, `EchoOrdinal`) -## Current Status Snapshot (2026-04-23) +## Current Status Snapshot + +The repository runs **two parallel, independent tracks**. *Echo Core does +NOT depend on the Ordinal / Buchholz track.* A reader interested only +in echo types as a type-theoretic concept can ignore the Ordinal track +entirely; it lives in `proofs/agda/Ordinal/` and is documented under +`roadmap.adoc` §Lane 3. + +### Echo Core (load-bearing for the identity claim) On `main`, the following are true: @@ -87,8 +95,24 @@ On `main`, the following are true: - core echo/fiber laws are smoke-pinned (`echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`) - non-injectivity/no-section family is present (`collapse-non-injective`, `no-section-collapse`, `no-section-visible`, `no-section-collapse-to-residue`, `no-section-weaken`) - distinct-witness and retained-constraint exemplars are present (`echo-true≢echo-false`, `stateA≢stateB`, `visible-constraint`) +- degrade-law family lands across decoration layers (graded, linear/affine, choreographic, access, cost, search); see `docs/theorem-index.md` for the aggregate +- Pillars A–D of the establishment plan are LANDED (with R-2026-05-18 narrowings; see `docs/retractions.adoc`); Pillar E (paper) is in progress +- Lane 5 tutorial triplet LANDED 2026-05-27 under `tutorial/`: region-exit audit, epistemic erasure, and provenance / debugging — each with honest-bound + matched-negative disclosure discipline; build via `agda --library-file=/tmp/agda-libs -i . -i proofs/agda tutorial/All.agda` + +Per-lane status, close-out criteria, and the identity-claim verdict +per tag are in `roadmap.adoc`. + +### Ordinal / Buchholz (parallel-independent, experimental) + +> **Banner.** This track is a separate proof-theoretic research project +> living in the same repository. Echo Core does not depend on it. +> Modules under `proofs/agda/Ordinal/` are treated as **experimental** +> until the unbudgeted `wf-<ᵇʳᶠ_` closure lands. See `roadmap.adoc` +> §Lane 3 for status and close-out criterion; `docs/buchholz-plan.adoc` +> for the full plan. -Ordinal/Buchholz track status: +Current state (one-line summary; the full per-rung ledger lives in +CLAUDE.md): - `Ordinal.Buchholz.WellFounded` provides `wf-<ᵇ : WellFounded _<ᵇ_` for the currently admitted constructor core - top-marker `bplus` bridges are admitted and inverted: `<ᵇ-+ω`, `<ᵇ-+ψω`, `<ᵇ-inv-+Ωω`, `<ᵇ-inv-+ψω` @@ -114,6 +138,7 @@ Ordinal/Buchholz track status: - the new budgeted layer on `ℕ × BT` isolates the missing global step: the recursive surface route is now well-founded once explicit budget is carried, and the remaining task is to discharge or eliminate that budget in the unbudgeted theorem - this still does not internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step - remaining live mathematical work is therefore not the current-core WF route, but the mediated internalization of the shared-binder cases back into the real order package +- as of 2026-05-27: the Buchholz rank-monotonicity matrix closes 11/13 constructor cases via the WfCNF-restricted `_<ᵇ⁻_` umbrella (9 via `RankPow` + `<ᵇ⁺-ψα` via `RankAdm` 2026-05-26 + `<ᵇ-ψΩ≤` via `RankLex` 2026-05-27); the last open case is `<ᵇ-+1` joint-bplus, with the `Ordinal.Buchholz.HeadOmega` first slice (leading-Ω-index head function + 4 definitional sanity lemmas) landed 2026-05-27 as the structural opening of option (A) per the obstruction doc ## External Bridge Targets (local workspace) @@ -131,7 +156,7 @@ Cross-repo status: - Agda-side content-bridge `proofs/agda/EchoCNOBridge.agda` imports `IsCNO` directly from `absolute-zero/proofs/agda/CNO.agda` (the earlier scaffolded-adapter plan `EchoBridgeScaffold.agda` was superseded) - end-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here - current bridge ledger: `docs/echo-types/cross-repo-bridge-status.md` -- see `docs/echo-types/roadmap.md` for staged cross-repo verification gates +- see `roadmap.adoc` (Lane 4) for staged cross-repo verification gates ## What Echo Types Are For @@ -178,6 +203,46 @@ cd /var/mnt/eclipse/repos/echo-types agda -i proofs/agda proofs/agda/All.agda ``` +### Installing as a library + +The repo is structured as an Agda library via `echo-types.agda-lib` +at the repo root. To use `echo-types` from another Agda project, +register the library file once: + +```bash +git clone https://github.com/hyperpolymath/echo-types.git +echo "$(pwd)/echo-types/echo-types.agda-lib" >> ~/.agda/libraries +``` + +Then in any other project, depend on `echo-types` in that +project's own `.agda-lib`: + +```text +name: my-project +depend: standard-library echo-types +include: src +``` + +Consumers can then `open import Echo`, `open import EchoLinear`, +or `open import tutorial.region_exit_audit.RegionExitAudit` — the +library's `include:` line covers both `proofs/agda` and the repo +root (for the Lane 5 tutorial track). + +Requires `standard-library` v2.3 or later registered alongside. + +## Citation + +If you cite this repository in academic work, please cite via the +Zenodo DOI listed in [CITATION.cff](CITATION.cff). The Zenodo +record is the canonical citation target; GitHub's "Cite this +repository" widget resolves directly to it. + +GitHub→Zenodo integration is a one-time author setup; until that +is wired the `CITATION.cff` `doi:` field carries a placeholder +(`10.5281/zenodo.0000000`). See +[docs/echo-types/pillar-e-offline.adoc](docs/echo-types/pillar-e-offline.adoc) +§"Zenodo DOI mint" for the activation sequence. + ## Tooling Stance - default development stays plain Agda with the standard library @@ -187,16 +252,25 @@ agda -i proofs/agda proofs/agda/All.agda ## Roadmap -Proof milestones and decision gates are in: +Single canonical roadmap with lane tracker, gates summary, pillar +status, deferred-research track, and operating rules: - `roadmap.adoc` -- `docs/buchholz-plan.adoc` -Open/gated work and cross-repo follow-ups are tracked in: +Companions (different kinds of doc, not roadmaps): + +- `roadmap-gates.adoc` — identity-claim falsifier gates (Gate 1/2/3) +- `docs/echo-types/establishment-plan.adoc` — five-pillar plan to + recognised type-theoretic standing +- `docs/buchholz-plan.adoc` — Ordinal track plan (parallel-independent + lane; see roadmap.adoc §Lane 3) +- `docs/echo-types/taxonomy.md`, `docs/echo-types/composition.md` — + topical reference -- `docs/echo-types/roadmap.md` -- `docs/echo-types/taxonomy.md` -- `docs/echo-types/composition.md` +As of 2026-05-26 the four previously overlapping roadmap docs +(`docs/echo-types/roadmap.md`, `docs/PRIORITIZED_PROOF_ROADMAP.md`, +`docs/ProofRoadmap.md`, `docs/WORK_PLAN.md`) have been consolidated +into `roadmap.adoc` and removed. ## Licensing diff --git a/core/skepticisms/is-this-just-sigma-types.md b/core/skepticisms/is-this-just-sigma-types.md index 01b36d4..8c77b6d 100644 --- a/core/skepticisms/is-this-just-sigma-types.md +++ b/core/skepticisms/is-this-just-sigma-types.md @@ -1,13 +1,162 @@ # Is this just Sigma Types? ## The Skeptical Position -Yes, at the lowest level of Agda code, this is `Σ (x : A) , (f x ≡ y)`. It relies entirely on the standard dependent pair type and propositional equality. +Yes, at the lowest level of Agda code, this is `Σ (x : A) , (f x ≡ y)`. +It relies entirely on the standard dependent pair type and propositional +equality. ## The Burden of Proof -Any claim of utility must show why working with the `Echo` wrapper is better than directly pattern-matching on the Sigma type. If every proof immediately unpacks the `Echo` and does standard Sigma-type manipulation, the abstraction is leaky and pointless. +Any claim of utility must show why working with the `Echo` wrapper is +better than directly pattern-matching on the Sigma type. If every proof +immediately unpacks the `Echo` and does standard Sigma-type manipulation, +the abstraction is leaky and pointless. ## Collapse Conditions -If the `Echo` interface requires the user to manually manage the underlying `Σ` structure to accomplish basic composition or mapping tasks, the abstraction fails. +If the `Echo` interface requires the user to manually manage the +underlying `Σ` structure to accomplish basic composition or mapping +tasks, the abstraction fails. ## Reinterpretation vs. Novelty -The novelty must reside in the API and the categorical/compositional properties exposed by the wrapper, demonstrating that `Echo` behaves coherently under lossy operations in a way that bare Sigma types do not automatically communicate. +The novelty must reside in the API and the categorical/compositional +properties exposed by the wrapper, demonstrating that `Echo` behaves +coherently under lossy operations in a way that bare Sigma types do not +automatically communicate. + +--- + +## Answer: the in-tree evidence + +This section is the index reviewers can walk to confirm Echo is not +"renamed Σ". It is organised under five demands a sceptic typically +makes. Each item points at a machine-checked Agda artefact (pinned in +`proofs/agda/Smoke.agda`), a doc, or both. Statements stay inside the +*narrowed* claims of `docs/retractions.adoc` R-2026-05-18 — no "full +universal property", no "graded comonad", no "model-independence". + +### 1. Irreversibility is a theorem family, not a property + +A raw `Σ (x : A) (f x ≡ y)` gives `proj₁` trivially; the user can +always extract the original `x`. The Echo programme proves that *no* +section exists once specific lossy interfaces are applied. The witness +is a *family* across five separate decoration layers: + +- `EchoCharacteristic.no-section-collapse` — no section of the + `Bool → ⊤` collapse map. +- `EchoCharacteristic.no-section-visible` — no section recovering the + pre-image from a visible output alone. +- `EchoResidue.no-section-collapse-to-residue` — weakening to a residue + is provably one-way. +- `EchoLinear.no-section-weaken` — the `linear → affine` mode shift is + one-way (defined as the residue lemma). +- `EchoOrdinal.no-section-ordinal-collapse` — ordinal collapse case. +- `EchoEpistemicResidue.no-section-to-epistemic` — epistemic-residue + case. + +All six are pinned in `Smoke.agda`. The family is what carries the +weight: each decoration *separately* refuses the section that a raw Σ +would admit. See also `docs/theorem-index.md` and the prose write-up at +`docs/characteristic.adoc`. + +### 2. Loss is graded, and downgrades cannot be reversed + +A raw Σ has no built-in notion of "degrading from strict to loose". +Echo equips the fibre with a lattice of grades and a monotone reindexing +along it. The two halves of the asymmetry are: + +- *Down-step is admissible.* `EchoGraded.degrade-compose` and + `EchoGraded.degrade-via-join` — the per-decoration composition law + for the loss-grade order. Same recipe lands at: + - `EchoLinear.degradeMode-compose` (linearity-mode order), + - `EchoChoreo.applyChoreo-compose` (role/reachability order), + - `EchoAccess` (graded access modality), + - `EchoCost` (cost-indexed refinement), + - `EchoSearch` (witness-search refinement). +- *Up-step is not.* `no-section-weaken` (item 1) is the same + statement on the other diagonal — once degraded, no inverse exists. + +Honest framing: this is a *thin-poset reindexing modality*, not a +graded comonad. The retraction at `docs/retractions.adoc#R-2026-05-18` +narrowed an earlier "graded comonad" claim. The reindexing modality is +the load-bearing structure and is the right answer to "is Σ enough?": +Σ alone gives neither the monotone reindex nor the no-section dual. + +### 3. Echo is the homotopy fibre; bridges from other "loss-tracker" frameworks exist + +The categorical/identity claim is **deflationary** and owned in +`docs/echo-types/establishment-plan.adoc`: `Echo f y` is *definitionally* +the homotopy fibre `fib f y` (HoTT book Def. 4.2.4). The bridge is +`EchoFiberBridge.echo↔fib`, both round-trips `refl` (Pillar A; pinned +in `Smoke.agda`). + +For the "is this just a pullback" question, `EchoPullback.echo-pullback-univ` +exhibits `Echo f y` as the pullback of `f` along `y : ⊤ → B` with a +*pointwise, funext-relative* mediator property. The retraction note in +that module is loud: this is **not** a full categorical universal +property in the absence of funext. Bridges from named neighbour +frameworks land as separate modules: + +- `EchoFiberBridge.agda` — homotopy fibre identity. +- `EchoJanusBridge.agda` — Janus-style reversible debugger bridge. +- `EchoTropical.agda` / `AntiEchoTropical.agda` — tropical + semiring / argmin decomposition. +- `EchoCNOBridge.agda` — categorical neighbour bridge. +- `EchoFiberCount.agda` + `EchoThermodynamics*.agda` — finite-fibre + Landauer / Bennett correspondence. + +These are independent witnesses, not one universal theorem. The honest +verdict is "Echo is *a* canonical target with concrete bridges in" +rather than "Echo is *the* terminal residue tracker by unique mediator". + +### 4. The abstraction barrier (consumer-side) + +A raw `Σ A (λ x → f x ≡ y)` exposes `proj₁`, so a consumer can always +distinguish two preimages of the same output. The Echo interface at the +affine mode does not export that projection: the residue carrier is +contractible (`EchoLinear.affine-canonical`, `affine-all-equal`), so +any consumer assigns the same value to the weakened images of two +known-distinct linear echoes. + +**Status:** the consumer-side abstraction-barrier theorem is the one +genuine gap relative to the five demands. It is planned as +`proofs/agda/EchoAbstractionBarrier.agda` (Track B in the work plan). +The model-side counterpart — *carrier-parametricity* over a fixed +grade poset — already lands as `EchoRelModel` (Pillar D, narrowed per +R-2026-05-18 from the original "model-independence" wording). + +### 5. Canonical examples — what Σ would let through + +The example modules exhibit echo as the explanatory unit on real +artefacts: + +- `EchoExampleParser` — `(())` vs `()()` are two distinct echoes at the + same `parses ≡ true`. +- `EchoExampleProvenance` — distinct Bool-provenance rows collapse to + the same payload; the echo carries the lost annotation. +- `EchoExampleAbsInt` — `{p1, p2}` collapse to `pos` under sign + analysis; the echo retains which. +- `EchoExampleSignAnalysis`, `EchoExampleTruncation` — further + collapse-with-residue exhibits. +- `EchoFiberCount` + `EchoThermodynamics*` — finite-fibre Landauer + bound for the erasure cost. +- `EchoEpistemicResidue` — observation-discipline residue. + +Each is positive evidence. The matched *negative* — a small raw-Σ +counter-program that would let the bug through — is planned as +`proofs/agda/examples/EchoVsSigma.agda` (Track C). Until that lands, +the "raw Σ would leak" claim is prose, not a checked artefact. + +--- + +## Cross-references + +- Gate 2 audit (closest reviewer touchpoint): + `docs/characteristic.adoc`. +- Theorem-by-theorem ledger: `docs/theorem-index.md`. +- Adjacency notes (per neighbour framework): `docs/adjacency/`. +- Honest scope of the establishment claim: + `docs/echo-types/establishment-plan.adoc` and + `docs/echo-types/paper.adoc` §"Reframing note". +- AsciiDoc reviewer companion to this file: + `docs/echo-types/sigma-distinctness-map.adoc`. +- Companion skepticisms: `is-this-just-fibers.md`, `what-is-actually-new.md`, + `failure-conditions.md`. diff --git a/docs/PRIORITIZED_PROOF_ROADMAP.md b/docs/PRIORITIZED_PROOF_ROADMAP.md deleted file mode 100644 index 6b20a59..0000000 --- a/docs/PRIORITIZED_PROOF_ROADMAP.md +++ /dev/null @@ -1,458 +0,0 @@ -# Echo Types Prioritized Proof Roadmap -# Based on Stability Analysis (April 2025) - -## Executive Summary - -This roadmap prioritizes proof development based on the stability analysis, focusing first on **immediate high-impact proofs** that will elevate echo types from B+ to A- stability, then progressing to **theoretical maturation**, and finally **exploring advanced applications**. - -## 🎯 Immediate Priorities (Next 6 Weeks) - -### Phase 1: JanusKey Integration Validation (Weeks 1-3) -**Objective**: Prove practical correctness of echo types with JanusKey operations - -#### Priority 1: Echo Witness Preservation Proofs -**File**: `proofs/agda/EchoJanusVerification.agda` - -```agda -module EchoJanusVerification where - -open import EchoJanusBridge -open import Echo -open import JanusKeyOperations -- To be created - --- Core theorem: Echo witnesses enable perfect reversal -echo-witness-preservation : ∀ (op : JanusKeyOp) (s : FileSystem) → - Echo (execute-op op) (op s) → - (undo op (op s) ≡ s) - --- Delete operation (HIGHEST PRIORITY) -echo-witness-preservation (Delete path) s (fs , p) = - -- fs contains the original file content - -- p proves that delete-op path fs ≡ s - -- Need to show: undo (delete-op path) s ≡ fs - ? - --- Create operation -echo-witness-preservation (Create path content) s (fs , p) = - -- fs is the original filesystem (without the file) - -- p proves that create-op path content fs ≡ s - -- Need to show: undo (create-op path content) s ≡ fs - ? - --- Modify operation -echo-witness-preservation (Modify path new-content) s (fs , p) = - -- fs contains original content - -- p proves that modify-op path new-content fs ≡ s - -- Need to show: undo (modify-op path new-content) s ≡ fs - ? - --- Move operation -echo-witness-preservation (Move src dest) s (fs , p) = - -- fs has file at original location - -- p proves that move-op src dest fs ≡ s - -- Need to show: undo (move-op src dest) s ≡ fs - ? -``` - -**Action Plan:** -- [ ] Week 1: Complete Delete operation proof -- [ ] Week 1: Complete Create operation proof -- [ ] Week 2: Complete Modify operation proof -- [ ] Week 2: Complete Move operation proof -- [ ] Week 3: Add comprehensive test cases -- [ ] Week 3: Validate with real JanusKey metadata - -**Success Criteria:** -- All four operation proofs completed -- Test suite with 20+ test cases -- Validation against actual JanusKey operations - -#### Priority 2: Transaction Composition Proof -**File**: `proofs/agda/EchoJanusTransactions.agda` - -```agda -module EchoJanusTransactions where - -open import EchoJanusBridge -open import Data.List using (List; []; _∷_) - --- Transaction as sequence of operations -Transaction : Set -Transaction = List JanusKeyOp - --- Execute transaction sequentially -execute-transaction : Transaction → FileSystem → FileSystem -execute-transaction [] s = s -execute-transaction (op ∷ ops) s = execute-transaction ops (execute-op op s) - --- Main theorem: Echo witnesses compose for transactions -transaction-echo-composition : ∀ {ops : Transaction} {s : FileSystem} → - (∀ op → Echo (execute-op op) (op s)) → - Echo (execute-transaction ops) (execute-sequentially ops s) -transaction-echo-composition [] s _ = s , refl -transaction-echo-composition (op ∷ ops) s witnesses = - let op-witness = witnesses op in - let remaining-witness = λ op' → witnesses op' in - ? -- Need to compose op-witness with transaction-echo-composition ops s remaining-witness -``` - -**Action Plan:** -- [ ] Week 2: Prove base case (empty transaction) -- [ ] Week 3: Prove inductive case (operation + remaining) -- [ ] Week 3: Test with 3-5 operation sequences -- [ ] Week 4: Validate with real transaction logs - -**Success Criteria:** -- Complete formal proof -- Test cases for transactions of length 1-5 -- Validation with actual JanusKey transactions - -### Phase 2: Performance Characterization (Weeks 4-6) -**Objective**: Formalize and validate performance guarantees - -#### Priority 3: Witness Generation Bounds -**File**: `proofs/agda/EchoJanusPerformance.agda` - -```agda -module EchoJanusPerformance where - -open import EchoJanusBridge -open import Data.Nat using (ℕ; _≤_) - --- Size measure for operations -Size : JanusKeyOp → ℕ -Size (Delete path) = length path -Size (Create path content) = length path + length content -Size (Modify path new-content) = length path + length new-content -Size (Move src dest) = length src + length dest - --- Size measure for echo witnesses -WitnessSize : ∀ {op s} → Echo (execute-op op) (op s) → ℕ -WitnessSize (fs , p) = Size fs + proof-size p - --- Main theorem: Witness generation is bounded -echo-generation-bound : ∀ (op : JanusKeyOp) (s : FileSystem) → - (w : Echo (execute-op op) (op s)) → - WitnessSize w ≤ 5 * Size op -- Constant factor 5 -``` - -**Action Plan:** -- [ ] Week 4: Define size measures -- [ ] Week 4: Prove for Delete operation -- [ ] Week 5: Prove for Create operation -- [ ] Week 5: Prove for Modify operation -- [ ] Week 6: Prove for Move operation -- [ ] Week 6: Empirical validation - -**Success Criteria:** -- Formal size bounds for all operations -- Constant factor validated empirically -- Performance documentation updated - -#### Priority 4: Verification Time Complexity -**File**: `proofs/agda/EchoJanusPerformance.agda` (continued) - -```agda --- Time measure for verification -VerificationTime : ∀ {op s} → Echo (execute-op op) (op s) → ℕ -VerificationTime w = ? -- To be defined based on witness structure - --- Main theorem: Verification is linear in witness size -verification-linear : ∀ (w : EchoWitness) → - VerificationTime w ≤ 2 * WitnessSize w -- Linear constant 2 -``` - -**Action Plan:** -- [ ] Week 5: Define verification time measure -- [ ] Week 6: Prove linear bound -- [ ] Week 6: Benchmark actual verification times -- [ ] Week 6: Update performance documentation - -**Success Criteria:** -- Formal linear time proof -- Benchmark data collected -- Performance guarantees documented - -## 📅 6-Week Detailed Schedule - -### Week 1: Foundation -``` -✅ Create EchoJanusVerification.agda -✅ Create EchoJanusTransactions.agda -✅ Create EchoJanusPerformance.agda -✅ Complete Delete operation proof -✅ Complete Create operation proof -✅ Set up test infrastructure -``` - -### Week 2: Core Operations -``` -✅ Complete Modify operation proof -✅ Complete Move operation proof -✅ Prove transaction base case -✅ Start transaction inductive case -✅ Add basic test cases -``` - -### Week 3: Transactions -``` -✅ Complete transaction composition proof -✅ Test transaction sequences -✅ Validate with real JanusKey data -✅ Define size measures -✅ Start performance bounds -``` - -### Week 4: Performance Foundations -``` -✅ Complete size measure definitions -✅ Prove Delete operation bounds -✅ Prove Create operation bounds -✅ Set up benchmarking infrastructure -✅ Collect initial performance data -``` - -### Week 5: Performance Proofs -``` -✅ Prove Modify operation bounds -✅ Prove Move operation bounds -✅ Define verification time measure -✅ Start linear time proof -✅ Collect benchmark data -``` - -### Week 6: Validation and Documentation -``` -✅ Complete linear time proof -✅ Finalize all performance proofs -✅ Comprehensive benchmarking -✅ Update all documentation -✅ Create validation report -✅ Prepare for next phase -``` - -## 🎯 Medium-Term Priorities (Next 3-6 Months) - -### Phase 3: Indexed Echo Types Maturation (Months 2-3) -**Objective**: Elevate indexed echo types from B+ to A- stability - -#### Priority 5: Role Separation -**File**: `proofs/agda/EchoIndexedEnhanced.agda` - -```agda -module EchoIndexedEnhanced where - -open import EchoIndexed - --- Theorem: Different roles cannot interfere -role-separation : ∀ {r1 r2 : Role} {s : FileSystem} → - r1 ≢ r2 → - Echoᵢ r1 s → Echoᵢ r2 s → - (proj₁ (echo1) ≢ proj₁ (echo2)) -``` - -**Action Plan:** -- [ ] Formalize role inequality -- [ ] Prove for audit trail example -- [ ] Add to indexed echo types documentation -- [ ] Create practical examples - -#### Priority 6: Permission Preservation -**File**: `proofs/agda/EchoIndexedEnhanced.agda` - -```agda --- Theorem: Operations preserve permission structures -permission-preservation : ∀ (op : JanusKeyOp) (s : FileSystem) → - Echo (execute-op op) (op s) → - (permissions (op s) ≡ permissions s) -``` - -**Action Plan:** -- [ ] Define permission structure -- [ ] Prove for each operation type -- [ ] Test with complex permission scenarios -- [ ] Document permission model - -### Phase 4: Categorical Semantics (Months 4-5) -**Objective**: Elevate categorical semantics from B to B+ - -#### Priority 7: Functor Laws -**File**: `proofs/agda/EchoCategoricalComplete.agda` - -```agda -module EchoCategoricalComplete where - -open import EchoCategorical - --- Theorem: Echo types form a functor -echo-functor-laws : IsFunctor EchoFunctor where - identity = {!!} - composition = {!!} -``` - -**Action Plan:** -- [ ] Prove identity law -- [ ] Prove composition law -- [ ] Add functor examples -- [ ] Document categorical properties - -#### Priority 8: Monad Instance -**File**: `proofs/agda/EchoCategoricalComplete.agda` - -```agda --- Theorem: Echo types form a monad -echo-monad : IsMonad EchoMonad where - return = echo-intro - bind = {!!} -``` - -**Action Plan:** -- [ ] Define bind operation -- [ ] Prove monad laws -- [ ] Add practical monad examples -- [ ] Document monadic usage patterns - -## 🔮 Long-Term Priorities (6-12 Months) - -### Phase 5: Distributed Reversibility (Months 6-8) -**Objective**: Extend echo types to distributed systems - -#### Priority 9: Distributed Echo Consistency -```agda -distributed-echo-consistency : ∀ {N} → (nodes : Fin N → NodeState) → - (op : DistributedOp) → - Echo (distributed-execute op) (final-state nodes) -``` - -#### Priority 10: Network Partition Recovery -```agda -network-partition-recovery : ∀ {op} → - Echo op s → - (∃ s' , recover-from-partition op s ≡ s') -``` - -### Phase 6: Resource-Bounded Reversibility (Months 9-10) -**Objective**: Prove reversibility under constraints - -#### Priority 11: Storage Bounds -```agda -bounded-storage-reversibility : ∀ (quota : ℕ) → - (op : BoundedOp quota) → - Echo (execute-op op) (op s) × - (storage-used (undo op) ≤ quota) -``` - -#### Priority 12: Time Bounds -```agda -time-bounded-reversibility : ∀ (timeout : ℕ) → - (op : BoundedOp timeout) → - Echo (execute-op op) (op s) × - (verification-time (undo op) ≤ timeout) -``` - -### Phase 7: Advanced Applications (Months 11-12) -**Objective**: Explore experimental extensions - -#### Priority 13: CRDT Integration -```agda -crdt-echo-correspondence : ∀ {C : CRDT} → - (op : CRDTOp C) → - Echo (crdt-apply op) (crdt-state-after op) -``` - -#### Priority 14: Transaction Isolation -```agda -serializable-reversibility : ∀ {txn : Transaction} → - Serializable txn → - Echo (execute-txn txn) (final-state txn) -``` - -## 📊 Progress Tracking - -### Current Status (April 2025) -| Priority | Area | Current Stability | Target Stability | Status | -|----------|------|-------------------|-------------------|---------| -| 1-2 | JanusKey Integration | B+ | A- | ⏳ In Progress | -| 3-4 | Performance | C+ | B+ | ⏳ Planned | -| 5-6 | Indexed Types | B+ | A- | ⏳ Planned | -| 7-8 | Categorical | B | B+ | ⏳ Planned | -| 9-10 | Distributed | C | B | ⏳ Future | -| 11-12 | Bounded | C | B | ⏳ Future | -| 13-14 | Advanced | C | B | ⏳ Future | - -### Target Milestones -| Date | Milestone | Stability Target | -|------|-----------|-------------------| -| Jun 2025 | JanusKey integration complete | A- | -| Aug 2025 | Performance proofs complete | B+ | -| Oct 2025 | Indexed types matured | A- | -| Dec 2025 | Categorical semantics complete | B+ | -| Feb 2026 | Distributed proofs started | C+ | -| Apr 2026 | Bounded reversibility proofs | B | -| Jun 2026 | Advanced applications explored | B | - -## 🔧 Implementation Resources - -### Required Files to Create -1. `proofs/agda/EchoJanusVerification.agda` - Core validation proofs -2. `proofs/agda/EchoJanusTransactions.agda` - Transaction composition -3. `proofs/agda/EchoJanusPerformance.agda` - Performance guarantees -4. `proofs/agda/EchoIndexedEnhanced.agda` - Enhanced indexed types -5. `proofs/agda/EchoCategoricalComplete.agda` - Complete categorical semantics - -### Supporting Infrastructure -1. `tests/` - Test suite directory -2. `benchmarks/` - Performance measurement tools -3. `docs/examples/` - Practical examples directory - -### Recommended Tools -- **Agda 2.6.2+** - For proof development -- **agda-stdlib** - Standard library dependencies -- **criterion.rs** - Rust benchmarking (for JanusKey) -- **quickcheck** - Property-based testing - -## 🎯 Strategic Impact - -### Short-Term (6 Weeks) -- **JanusKey Integration**: Production-ready with formal proofs -- **Performance Guarantees**: Documented and validated -- **Stability Rating**: B+ → A- for core applications - -### Medium-Term (6 Months) -- **Theoretical Maturity**: Indexed and categorical semantics at B+/A- -- **Practical Validation**: Real-world tested and benchmarked -- **Ecosystem Readiness**: Ready for broader adoption - -### Long-Term (12 Months) -- **Advanced Applications**: Distributed, bounded, CRDT extensions -- **Unified Theory**: Comprehensive reversibility framework -- **Industry Adoption**: Production use in multiple systems - -## 📋 Getting Started Checklist - -### Week 1 Actions -- [ ] Create `EchoJanusVerification.agda` -- [ ] Implement Delete operation proof -- [ ] Implement Create operation proof -- [ ] Set up test infrastructure -- [ ] Create basic test cases - -### Week 2 Actions -- [ ] Implement Modify operation proof -- [ ] Implement Move operation proof -- [ ] Start transaction composition proof -- [ ] Add transaction test cases -- [ ] Begin performance measure definitions - -### Week 3 Actions -- [ ] Complete transaction composition proof -- [ ] Validate with real JanusKey data -- [ ] Prove Delete operation bounds -- [ ] Prove Create operation bounds -- [ ] Set up benchmarking - -## Conclusion - -This prioritized proof roadmap provides a **clear, actionable plan** to systematically improve echo types' stability from B+ to A- over the next 6 months. By focusing first on **JanusKey integration validation**, then **performance characterization**, and progressing to **theoretical maturation**, we ensure both **practical impact** and **theoretical rigor**. - -The roadmap balances **immediate practical needs** with **long-term theoretical development**, ensuring echo types remain at the forefront of formal reversibility research while delivering real-world value to systems like JanusKey. \ No newline at end of file diff --git a/docs/ProofRoadmap.md b/docs/ProofRoadmap.md deleted file mode 100644 index 87151e8..0000000 --- a/docs/ProofRoadmap.md +++ /dev/null @@ -1,184 +0,0 @@ -# Echo Types - JanusKey Proof Roadmap - -## Strategic Proof Priorities - -### Tier 1: Foundational Proofs (Immediate Impact) - -#### 1. **Formal Verification of JanusKey Rust Implementation** -**Goal**: Prove that JanusKey's Rust code correctly implements the echo type specifications -**Approach**: -- Extract formal specifications from `EchoJanusBridge.agda` -- Create Rust verification targets using formal methods (e.g., Prusti, Creusot) -- Prove correspondence between Rust operations and Agda echo types -**Impact**: Closes the gap between theory and practice, validates real-world implementation - -#### 2. **Distributed Reversibility Proof** -**Goal**: Extend echo types to distributed file systems with network partitions -**Theorems to Prove**: -```agda -distributed-echo-consistency : ∀ {N} → (nodes : Fin N → NodeState) → - (op : DistributedOp) → - Echo (distributed-execute op) (final-state nodes) -distributed-undo-commutativity : ∀ {op1 op2} → - Echo op1 s1 → Echo op2 s2 → - undo op1 ∘ undo op2 ≡ undo op2 ∘ undo op1 -``` -**Impact**: Enables JanusKey distributed mode with mathematical guarantees - -#### 3. **Resource-Bounded Reversibility** -**Goal**: Prove reversibility under storage/memory constraints -**Theorems to Prove**: -```agda -bounded-storage-reversibility : ∀ (quota : ℕ) → - (op : BoundedOp quota) → - (s : FileSystem) → - Echo (execute-op op) (op s) × - (storage-used (undo op) ≤ quota) -``` -**Impact**: Addresses practical concerns about reversal costs - -### Tier 2: Advanced Theoretical Proofs - -#### 4. **Temporal Logic of Reversible Operations** -**Goal**: Develop temporal logic semantics for echo types -**Theorems to Prove**: -```agda -□-reversible : ∀ {op} → (□ (Echo op s)) → (□ (∃ s' , undo op s ≡ s')) -⋄-reversible : ∀ {op} → (⋄ (Echo op s)) → (⋄ (∃ s' , undo op s ≡ s')) -``` -**Impact**: Enables formal reasoning about operation sequences over time - -#### 5. **Categorical Semantics of Echo Types** -**Goal**: Show echo types form a category with reversible operations as morphisms -**Theorems to Prove**: -```agda -echo-category : Category EchoCat where - Ob = FileSystem - Hom A B = Echo (some-op) B -- Morphisms are echo witnesses - id = echo-intro id - _∘_ = map-over -``` -**Impact**: Provides higher-level abstraction for compositional reasoning - -#### 6. **Graded Modal Types for Permissions** -**Goal**: Extend echo types with permission grading (read/write/execute) -**Theorems to Prove**: -```agda -permission-preserving-echo : ∀ {p} {op : PermissionAwareOp p} → - Echo op s → - (permissions (undo op s) ≡ permissions s) -``` -**Impact**: Enables fine-grained access control with reversibility guarantees - -### Tier 3: Applied Proofs - -#### 7. **Transaction Isolation Levels** -**Goal**: Prove reversibility at different isolation levels (Serializable, Repeatable Read, etc.) -**Theorems to Prove**: -```agda -serializable-reversibility : ∀ {txn : Transaction} → - Serializable txn → - Echo (execute-txn txn) (final-state txn) -``` -**Impact**: Enables JanusKey to offer different consistency guarantees - -#### 8. **Conflict-Free Replicated Data Types (CRDTs)** -**Goal**: Show echo types can model CRDT reversibility -**Theorems to Prove**: -```agda -crdt-echo-correspondence : ∀ {C : CRDT} → - (op : CRDTOp C) → - Echo (crdt-apply op) (crdt-state-after op) -``` -**Impact**: Enables collaborative editing with reversibility - -#### 9. **Quantum-Inspired Reversibility** -**Goal**: Explore connections with quantum computing reversibility -**Theorems to Prove**: -```agda -unitary-echo-correspondence : ∀ {U : UnitaryMatrix} → - Echo (quantum-apply U) (quantum-state-after U) -``` -**Impact**: Future-proofs for quantum computing applications - -### Tier 4: Cross-Domain Proofs - -#### 10. **MAA Framework Integration** -**Goal**: Connect echo types with MAA's reversibility proofs -**Theorems to Prove**: -```agda -maa-echo-equivalence : ∀ {p : MAAProgram} → - MAAReversible p → - (∀ σ → Echo (maa-execute p) (p σ)) -``` -**Impact**: Unifies formal verification efforts across the ecosystem - -#### 11. **Absolute Zero CNO Integration** -**Goal**: Show CNOs (Certified Null Operations) are special cases of echo types -**Theorems to Prove**: -```agda -cno-as-echo-subcategory : CNO-Category → Subcategory Echo-Category -``` -**Impact**: Creates unified theory of null/reversible operations - -#### 12. **Homotopy Type Theory Extension** -**Goal**: Develop higher-dimensional echo types -**Theorems to Prove**: -```agda -homotopy-echo : ∀ {A B} (f : A → B) (y : B) → - Echo f y → (x : A) → (f x ≡ y) → (x ≡ proj₁ (echo-witness)) -``` -**Impact**: Enables proof-relevant reversibility reasoning - -## Proof Development Strategy - -### Phase 1: Implementation Verification (3-6 months) -- Focus on Tier 1 proofs #1-3 -- Develop Rust verification infrastructure -- Create test suites linking Agda specs to Rust code - -### Phase 2: Theoretical Deepening (6-12 months) -- Pursue Tier 2 proofs #4-6 -- Develop categorical and temporal semantics -- Publish academic papers on results - -### Phase 3: Applied Extensions (12-18 months) -- Implement Tier 3 proofs #7-9 -- Develop practical applications (distributed systems, CRDTs) -- Create demo applications showing real-world impact - -### Phase 4: Ecosystem Integration (18-24 months) -- Complete Tier 4 proofs #10-12 -- Integrate with MAA Framework and Absolute Zero -- Develop unified theory of reversibility - -## Resource Requirements - -### Human Resources: -- 1-2 formal methods experts (Agda/Coq) -- 1 Rust verification specialist -- 1 category theory expert -- 1 distributed systems researcher - -### Technical Resources: -- Formal verification tools (Agda, Coq, Prusti) -- Theorem prover integration -- Test infrastructure for Rust verification -- Documentation and visualization tools - -## Expected Outcomes - -1. **Theoretical Advancement**: Echo types become recognized framework for reversibility -2. **Practical Validation**: JanusKey achieves formal verification of its core claims -3. **Ecosystem Growth**: Unified approach to reversibility across MAA projects -4. **Academic Impact**: Publications in top PL/verification conferences -5. **Industry Adoption**: Formal methods for reversible systems gain traction - -## Risk Mitigation - -- **Complexity Risk**: Start with simplest proofs first, build complexity gradually -- **Tooling Risk**: Use multiple verification approaches (Agda + Rust verification) -- **Integration Risk**: Develop clear interfaces between components -- **Performance Risk**: Profile verification overhead early - -This roadmap provides a comprehensive strategy for enhancing both echo types' theoretical standing and JanusKey's practical reality through systematic proof development. \ No newline at end of file diff --git a/docs/WORK_PLAN.md b/docs/WORK_PLAN.md deleted file mode 100644 index 662cbed..0000000 --- a/docs/WORK_PLAN.md +++ /dev/null @@ -1,323 +0,0 @@ -# Echo Types Work Plan (Based on Stability Analysis) - -## Guiding Principles - -1. **Stabilize the Core**: Ensure A-rated components remain production-ready -2. **Maturity the Middle**: Elevate B-rated components to A- status -3. **Explore the Edges**: Responsibly develop C-rated experimental areas -4. **Validate in Practice**: Connect theory to real-world implementations - -## Priority Work Areas (3-6 Months) - -### 🔥 High Priority: Stabilize B+ Components - -#### 1. JanusKey Bridge Maturation -**Goal**: Elevate from B+ to A- stability - -**Specific Tasks:** -- [ ] **Integration Testing**: Create comprehensive test suite - ```agda - -- Test echo witness preservation across operations - echo-witness-preservation-test : ∀ (op : JanusKeyOp) → - Echo op s → - (undo op (op s) ≡ s) - ``` -- [ ] **Performance Benchmarking**: Establish baseline metrics - - Measure echo witness generation time - - Profile verification overhead - - Document performance characteristics - -- [ ] **Real-World Validation**: Test with actual JanusKey operations - - Create test corpus of file operations - - Verify echo witnesses match real metadata - - Validate undo operations work correctly - -**Success Criteria:** -- 98% test coverage -- Documented performance profile -- Validated with 100+ real operations - -#### 2. Indexed Echo Types Refinement -**Goal**: Elevate from B+ to A- stability - -**Specific Tasks:** -- [ ] **Additional Examples**: Add practical use cases - ```agda - -- Audit trail example with role separation - audit-trail-example : Echoᵢ Role trace-role trace-visible auditor true - ``` -- [ ] **Generalization Analysis**: Identify potential abstractions -- [ ] **Documentation Expansion**: Add user guide section - -**Success Criteria:** -- 3+ new practical examples -- Clear generalization boundaries identified -- Comprehensive user documentation - -### 🎯 Medium Priority: Strengthen B Components - -#### 3. Categorical Semantics Development -**Goal**: Elevate from B to B+ stability - -**Specific Tasks:** -- [ ] **Functor Laws Verification**: Formal proof of functoriality - ```agda - echo-functor-laws : IsFunctor EchoFunctor - ``` -- [ ] **Monad Instance**: Complete monadic structure - ```agda - echo-monad : IsMonad EchoMonad - ``` -- [ ] **Adjunction Proofs**: Formalize relationships with other categories - -**Success Criteria:** -- Complete functor proof -- Working monad instance -- 2+ adjunction examples - -#### 4. Relational Semantics Enhancement -**Goal**: Elevate from B to B+ stability - -**Specific Tasks:** -- [ ] **Additional Examples**: More step semantics cases -- [ ] **Composition Theorems**: Prove compositional properties - ```agda - relational-composition : ∀ {s1 s2 s3} → - Step s1 s2 → Step s2 s3 → Step s1 s3 - ``` -- [ ] **Integration Guide**: How to use in practice - -**Success Criteria:** -- 5+ new examples -- Composition theorems proven -- Practical integration guide - -### 🧪 Low Priority: Explore C Components - -#### 5. Thermodynamic Models (Research) -**Goal**: Assess feasibility and potential - -**Specific Tasks:** -- [ ] **Literature Review**: Connect with existing thermodynamic computing -- [ ] **Energy Bounds**: Formalize practical limits - ```agda - energy-bound : ∀ (op : Operation) → - Energy op ≤ ThermodynamicLimit op - ``` -- [ ] **Feasibility Assessment**: Determine if worth pursuing - -**Success Criteria:** -- Literature survey completed -- Basic energy bounds formalized -- Go/no-go decision on further development - -## Implementation Strategy - -### Phase 1: Foundation (Weeks 1-4) -**Focus**: Set up infrastructure for validation - -**Tasks:** -1. **Test Infrastructure**: Create Agda test framework -2. **Benchmarking Setup**: Performance measurement tools -3. **Documentation Template**: Standard format for new materials -4. **CI Integration**: Add proof checking to pipeline - -**Deliverables:** -- Working test framework -- Performance benchmarking tools -- Documentation templates -- CI pipeline updates - -### Phase 2: Core Stabilization (Weeks 5-12) -**Focus**: JanusKey bridge and indexed types - -**Tasks:** -1. **JanusKey Integration Tests**: Comprehensive test suite -2. **Performance Profiling**: Baseline metrics -3. **Indexed Type Examples**: Practical use cases -4. **Real-World Validation**: Test with actual operations - -**Deliverables:** -- 98% test coverage for JanusKey bridge -- Performance documentation -- 3+ new indexed type examples -- Validation report - -### Phase 3: Theory Maturation (Weeks 13-20) -**Focus**: Categorical and relational semantics - -**Tasks:** -1. **Functor Laws**: Complete formal proofs -2. **Monad Instance**: Working implementation -3. **Relational Examples**: Expanded case studies -4. **Composition Theorems**: Formal proofs - -**Deliverables:** -- Complete functor proof -- Working monad instance -- 5+ new relational examples -- Composition theorem proofs - -### Phase 4: Exploration (Weeks 21-24) -**Focus**: Experimental areas assessment - -**Tasks:** -1. **Thermodynamic Literature Review**: State of the art -2. **Energy Bound Formalization**: Basic theorems -3. **Feasibility Report**: Recommendations -4. **Roadmap Update**: Based on findings - -**Deliverables:** -- Literature survey document -- Basic energy bound proofs -- Feasibility assessment -- Updated roadmap - -## Resource Allocation - -### Human Resources (3-6 Months) -- **1 Senior Researcher**: Theory development (categorical, relational) -- **1 Formal Methods Engineer**: Testing, verification, CI integration -- **1 Documentation Specialist**: Examples, guides, tutorials -- **0.5 Performance Engineer**: Benchmarking and optimization - -### Time Allocation -- **40%**: JanusKey bridge stabilization (highest priority) -- **30%**: Theory maturation (categorical, relational) -- **20%**: Infrastructure and tooling -- **10%**: Experimental exploration - -## Success Metrics - -### Quantitative Goals -| Metric | Current | Target (6 months) | -|--------|---------|-------------------| -| Test Coverage | 40% | 95% | -| Proof Coverage | 85% | 98% | -| Documentation Completeness | 90% | 99% | -| Performance Data | Limited | Comprehensive | -| Real-World Validation | None | 100+ operations | - -### Qualitative Goals -1. **JanusKey Integration**: Seamless connection between theory and practice -2. **Theory Maturity**: Clear, well-documented mathematical foundations -3. **Developer Experience**: Easy to understand and extend -4. **Ecosystem Readiness**: Prepared for broader adoption - -## Risk Management - -### Risk: Theory-Practice Gap -**Mitigation:** -- Early and frequent validation with real operations -- Continuous feedback from JanusKey developers -- Iterative refinement based on practical findings - -### Risk: Proof Complexity -**Mitigation:** -- Modular proof development -- Clear documentation of proof patterns -- Automated verification where possible - -### Risk: Performance Overhead -**Mitigation:** -- Early benchmarking -- Optimization strategies identified -- Trade-off analysis documented - -### Risk: Scope Creep -**Mitigation:** -- Clear prioritization (A → B → C components) -- Time-boxed exploration phases -- Regular progress reviews - -## Decision Points - -### Month 3: JanusKey Validation -**Decision**: Continue full integration vs. targeted use cases -**Criteria**: Test results, performance metrics, developer feedback - -### Month 5: Theory Maturation -**Decision**: Pursue formal publication vs. internal documentation -**Criteria**: Proof completeness, novelty, academic interest - -### Month 6: Experimental Areas -**Decision**: Invest in thermodynamic models vs. other extensions -**Criteria**: Feasibility, potential impact, resource availability - -## Integration Plan - -### With JanusKey -1. **Immediate**: Use echo types for core operation verification -2. **Short-term**: Integrate into transaction system -3. **Long-term**: Full formal verification of Rust implementation - -### With MAA Framework -1. **Immediate**: Document connection points -2. **Short-term**: Create integration examples -3. **Long-term**: Unified reversibility theory - -### With Absolute Zero -1. **Immediate**: Leverage CNO bridge -2. **Short-term**: Joint proof development -3. **Long-term**: Unified formal methods approach - -## Communication Strategy - -### Internal -- **Weekly**: Progress updates -- **Monthly**: Technical deep dives -- **Quarterly**: Strategy reviews - -### External -- **Blog Posts**: Theory explanations, practical guides -- **Conference Talks**: Academic and industry venues -- **Documentation**: Comprehensive, up-to-date, accessible - -## Timeline - -``` -Month 1: Infrastructure Setup -Month 2: JanusKey Testing Framework -Month 3: Performance Benchmarking -Month 4: Indexed Types Examples -Month 5: Categorical Semantics -Month 6: Relational Enhancements & Assessment -``` - -## Budget Estimate - -### Personnel (6 months) -- Senior Researcher: $60,000 -- Formal Methods Engineer: $45,000 -- Documentation Specialist: $30,000 -- Performance Engineer: $15,000 -- **Total Personnel**: $150,000 - -### Tools & Infrastructure -- Agda/Coq licenses: $5,000 -- CI/CD pipeline: $3,000 -- Benchmarking tools: $2,000 -- **Total Tools**: $10,000 - -### Travel & Conferences -- Conference presentations: $7,000 -- Team workshops: $3,000 -- **Total Travel**: $10,000 - -### Contingency (15%) -- **Contingency**: $25,500 - -### **Total Budget**: $195,500 - -## Conclusion - -This work plan provides a **clear, prioritized approach** to maturing echo types based on the stability analysis. By focusing first on **stabilizing the B+ components** (especially JanusKey integration), then **strengthening the B components**, and finally **exploring the C components**, we can systematically improve the overall stability rating from B+ to A-. - -The plan balances **theoretical rigor** with **practical validation**, ensuring that echo types remain both **mathematically sound** and **practically useful**. Regular checkpoints and decision points allow for **adaptive management** while maintaining focus on the highest-impact areas. - -**Expected Outcome**: In 6 months, echo types will have: -- Production-ready JanusKey integration (A- stability) -- Matured theoretical extensions (B+ stability) -- Clear path forward for experimental areas -- Comprehensive documentation and validation -- Strong foundation for broader ecosystem adoption \ No newline at end of file diff --git a/docs/bridges/ECHO-CNO-BRIDGE.adoc b/docs/bridges/ECHO-CNO-BRIDGE.adoc index 70cc7c3..a339f8e 100644 --- a/docs/bridges/ECHO-CNO-BRIDGE.adoc +++ b/docs/bridges/ECHO-CNO-BRIDGE.adoc @@ -110,7 +110,7 @@ but that is a witness-presence statement, not an information-preservation statement. A real Shannon-entropy / mutual-information formalisation is open -work; see `docs/echo-types/roadmap.md` under the thermodynamic +work; see `roadmap.adoc` under the deferred research / thermodynamic items. ### Theorem 6: Universal CNO Definition (NEW) @@ -413,7 +413,7 @@ kill condition**: a mechanised proof that clauses (i)∧(ii) ⊢ ⊥. (`collapse-cost-impossible`), a settled boundary, no open obligation remains for this Direction. 3. **Information Theory**: not bridged. Open work — see - `docs/echo-types/roadmap.md`. + `roadmap.adoc` (deferred research track). ## Practical Implications diff --git a/docs/bridges/tropical-correspondence.md b/docs/bridges/tropical-correspondence.md index 472235f..664a1b4 100644 --- a/docs/bridges/tropical-correspondence.md +++ b/docs/bridges/tropical-correspondence.md @@ -84,8 +84,8 @@ not constitute a unified verification artefact. It closes the grading* (`grade : Session → Tropical` in Lean), which is the symmetric Agda-exclusive direction. - **Long-game alignment target.** When the echo-types ordinal track - reaches Bachmann–Howard (ψ₀(Ω_ω); see `docs/echo-types/roadmap.md` - and `buchholz-plan.adoc`), the adjacent repo's + reaches Bachmann–Howard (ψ₀(Ω_ω); see `roadmap.adoc` §Lane 3 and + `docs/buchholz-plan.adoc`), the adjacent repo's `Tropical_Ordinal_Bridge.thy` becomes the natural cross-repo alignment target (Agda Buchholz BT ↔ Isabelle `tropO` carrier). This target is **firewalled** until the ordinal track lands the diff --git a/docs/characteristic.adoc b/docs/characteristic.adoc index 0ae6b56..19a027b 100644 --- a/docs/characteristic.adoc +++ b/docs/characteristic.adoc @@ -11,11 +11,15 @@ Gate 2 of the identity claim. It audits the nominees against the gate's falsifier — "naturally echo-shaped, not reducible to generic sigma/fiber lemmas" — and reports the threshold outcome. -This is *Revision 4*. It adds a fourth nominee (`EchoLinear.degradeMode-compose`), -introduces a new construction in this lane (`characteristic.RoleGraded`) -that closes the open recommendation from the handoff's Observation E, -and proposes a candidate fifth nominee. See §<> -for the diff. +This is *Revision 5* (2026-05-26). It is the close-out re-audit +required by `roadmap.adoc` §Lane 2: it re-checks that the +Revision-4 nominee table still clears the *comfortable* threshold +(≥ 3 of 4 surviving) under everything that has landed in this +lane since then. Verdict: still 4/4 surviving; comfortable +threshold met by margin of one. The Revision-5 substance is in +§<>; the per-nominee +audits below are unchanged from Revision 4. See §<> for the full diff. toc::[] @@ -29,6 +33,13 @@ at integration time. == Inherited spec +For the sceptic-facing evidence map ("is this just renamed Σ?", +organised under five demands and cross-linked to every in-tree +artefact), see `docs/echo-types/sigma-distinctness-map.adoc` and its +internal companion `core/skepticisms/is-this-just-sigma-types.md`. +That doc is an evidence index; this file is the per-nominee Gate 2 +audit and remains the authoritative gate artefact. + `roadmap-gates.adoc` Gate 2: .Claim @@ -511,8 +522,128 @@ withdrawn lemma can be left in place as a historical signpost. | 3 | Amendment to `roadmap-gates.adoc` adopted. Nominee list: `degrade-via-join`, `degrade-compose`, `applyChoreo-compose`. 3/3 surviving across two modules. Recommended further work: genuine integration theorem; fourth nominee for diversification. | 4 | Added `EchoLinear.degradeMode-compose` as N4 (per the Revision-3 recommendation; user-explicit). Built `characteristic.RoleGraded` and `choreo-grade-commute` (closes handoff Observation E). 4/4 surviving across three modules. Proposed adding `choreo-grade-commute` as N5 (left to integrator's discretion). + +| 5 (2026-05-26) | Close-out re-audit per `roadmap.adoc` §Lane 2: re-checks the Revision-4 nominee table against everything that has landed since (EI-2 terminated negative; `characteristic.NonTruncatable` for Q2.1 received-`y` form is PARTIALLY REDUCIBLE; the broken `characteristic.N5Falsifier` is ledgered, not silently dropped). Verdict: 4/4 still surviving, *comfortable* threshold (≥3/4) met by margin of one. Candidate N5 (`choreo-grade-commute`) remains unadopted: the post-Rev-4 EI-2 termination shows its non-trivial content is the same single `(c⊑s, keep≤keep)` cell as before, so nominating it would not strengthen the count beyond cosmetic. + +| 5b (2026-05-27) | Within-Rev-5 follow-up: `characteristic.N5Falsifier` *no longer broken* — unsolved metas around `EchoChoreo.obs` were resolved by pinning the implicit role and grade parameters at the four `applyRole`/`applyGrade` call sites (the blocker was inference, not content). The module is now in `characteristic/All.agda`'s CI green closure. Audit consequences are *recorded in-line in §"Evidence reviewed" item 3 above*: the SURVIVES verdict for the falsifier exhibit is now mechanised, but the N5-not-adopted decision is unchanged on the same Rev-4/Rev-5 cosmetic-only-marginal-evidence logic. +|=== + +[[revision-5]] +== Revision-5 re-audit (2026-05-26) + +This section is the close-out audit named in `roadmap.adoc` §Lane 2 +close-out criterion (3). It re-checks the Revision-4 nominee table +against everything that has landed in the characteristic / Gate-2 +lane since Revision 4. Three categories of evidence were considered; +none weakens the Revision-4 verdict. + +=== Bar being checked + +`roadmap.adoc` §Lane 2 distinguishes two thresholds (taken from +`roadmap-gates.adoc` Gate 2): the *honest minimum* (≥ 2 of 4 +surviving) and the *comfortable* threshold (≥ 3 of 4 surviving). +Revision 4 reported 4/4. Lane 2 close-out asks: under everything +this lane has produced since, does that still hold by the +comfortable bar? + +=== Evidence reviewed since Revision 4 + +. *EI-2 terminated — negative verdict, PATH B* (`docs/EI2_REPORT.adoc`, + authoritative). Eight investigation phases, seven data points + (sibling 2D constructions `characteristic.RoleMode`, + `characteristic.ModeGraded`, 3D `characteristic.RoleModeGrade` + with three pairwise commutations + a triple, self-pairing + `characteristic.RoleRole`), plus the formal exhibit + `characteristic.ChoreoInjective` for the non-loss-only criterion + and the partial generic `characteristic.RecipeTheorem`. The + termination finding is that the integration recipe with the + existing five named axes does *not* carry substantive simultaneous + cross-axis content — every "non-trivial" cell carries one-axis-at- + a-time content. The five doc locations enumerated in EI2_REPORT + §"Documentation cascade" have all been updated accordingly. +. *Q2.1 / `characteristic.NonTruncatable`.* The general statement of + `echo-not-prop` for `(f, y)` with two distinct preimages is + re-exported under the Q2.1 name; the received-`y` form is + *PARTIALLY REDUCIBLE* per the module's own Gate-2 falsifier audit + (proof factors through generic Σ; echo-specific content is in the + statement only). The constructed-`y` form, which builds `y` from + bare non-injectivity, carries echo-specific content but is not on + the Revision-4 nominee table — it is closer to a Gate-3 example + obligation than a Gate-2 nominee. +. *`characteristic.N5Falsifier` — RESOLVED 2026-05-27, NOW GREEN AND IN CI CLOSURE.* + Originally KNOWN BROKEN, deliberately excluded + (`UnsolvedConstraints` + `UnsolvedMetaVariables`). The Lane-2 + N5-sharpening pass on 2026-05-27 closed the unsolved metas by + making the implicit `r1`/`r2`/`g` parameters of `applyRole` / + `applyGrade` explicit at the four call sites; the obstacle was + *inference*, not *content* (Agda cannot recover the role from + `RoleGEcho r keep = Echo (obs r) true` because `obs` is not + injective, but supplying the role explicitly resolves it). The + module is now imported in `characteristic/All.agda` and the + broken-banner has been updated with the resolution record. + *Crucially: the resolution does not change the Rev-4 conclusion + about candidate N5* — the only non-trivial cell is still the + `(c⊑s, keep≤keep)` Choreo content already credited to N3, so + adoption would still be cosmetic. The cleaned-up green falsifier + exhibit *does* tighten the audit story (the SURVIVES verdict is + now mechanised instead of being a not-mechanised attempt-of-record) + without changing the N5-not-adopted decision. + +=== Per-nominee re-check + +[cols="1,2,2,3", options="header"] +|=== +| Nominee | Module | Status as of Rev 5 | Reason + +| N1 | `EchoGraded.degrade-via-join` | SURVIVES (unchanged from Rev 4) | The lemma is on the loss-grade lattice's join, not on any integration claim. EI-2 termination does not touch it. No falsifier attempted since Rev 4. +| N2 | `EchoGraded.degrade-compose` | SURVIVES (unchanged from Rev 4) | As N1: single-decoration lemma; EI-2 termination is orthogonal. No falsifier attempted since Rev 4. +| N3 | `EchoChoreo.applyChoreo-compose` | SURVIVES (unchanged from Rev 4) | Single-decoration role-reachability lemma; the `client-to-server` content this lemma factors through is the very content EI-2 traced as the one load-bearing non-trivial cell across 2D pairings — that is independent evidence the lemma is non-vacuous, not a weakening. +| N4 | `EchoLinear.degradeMode-compose` | SURVIVES (unchanged from Rev 4) | Single-decoration mode lemma with the specific `weaken` content (`no-section-collapse-to-residue` attached); EI-2 termination is orthogonal. |=== +=== Verdict + +Survivors: N1, N2, N3, N4. Count: 4. Honest threshold (≥ 2): met. +Comfortable threshold (≥ 3): met by margin of one. The Lane 2 +close-out criterion in `roadmap.adoc` is satisfied. + +=== What the re-audit explicitly does NOT do + +. *Does not nominate N5.* The candidate fifth nominee + (`characteristic.RoleGraded.choreo-grade-commute`) remains a + candidate. EI-2's termination shows the protocol-pass-but-narrow + reading from Rev 4 was correct: the only non-trivial cell of the + 2D family's commutation is `(c⊑s, keep≤keep)`, reducing to + `client-to-server e` — the same Choreo content N3 already carries. + Nominating it would push the count to 5/5, but the marginal + evidence is the same `client-to-server` content already credited + to N3, so nominating it would be cosmetic. Left unadopted on the + same logic as Rev 4. +. *Does not retroactively retract any Rev-4 verdict.* No nominee's + falsifier was attempted and *failed*; the absence of attempts is + carried forward as a Rev-4 honest qualification (§<> item 3), not a Rev-5 finding. +. *Does not promote `characteristic.NonTruncatable.Q2-1` to the + nominee table.* Its own broken-Gate-2 audit (PARTIALLY REDUCIBLE) + was applied honestly; the lemma remains useful as a Gate-3 + signpost, not as a Gate-2 survivor. + +=== Pointer additions since Rev 4 + +* `proofs/agda/characteristic/RoleMode.agda`, + `RoleModeGrade.agda`, `RoleRole.agda`, `ModeGraded.agda`, + `ChoreoInjective.agda`, `RecipeNonTriviality.agda`, + `RecipeSpec.agda`, `RecipeTheorem.agda`, `InteractionTest.agda` — + EI-2 investigation lane. Not Gate-2 nominees; supply the + EI-2-termination evidence the §"Evidence reviewed" item 1 cites. +* `proofs/agda/characteristic/NonTruncatable.agda` — Q2.1, see + §"Evidence reviewed" item 2. +* `proofs/agda/characteristic/N5Falsifier.agda` — + *KNOWN BROKEN, NOT IN CI CLOSURE*; see §"Evidence reviewed" + item 3. +* `docs/EI2_REPORT.adoc` — authoritative EI-2 verdict. +* `proofs/agda/characteristic/All.agda` — the lane-local CI seam. + == Cross-lane observations See `docs/gate-2-handoff.adoc`. diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index dd3665a..32735c3 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -83,7 +83,7 @@ the standing B- freeze lifted because O-THERMO-∞ is now discharged `proofs/agda/EchoThermodynamicsArbitrary.agda`, `proofs/agda/EchoThermoCollapseImpossible.agda`. * Docs: `docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge", - `docs/STABILITY_ANALYSIS.md` §3.3, `docs/WORK_PLAN.md` §5, + `docs/STABILITY_ANALYSIS.md` §3.3, `docs/adjacency/hott-fibers.adoc`. * Build: `just test-thermo`. @@ -141,7 +141,7 @@ Connect echo types with MAA's reversibility proofs (`maa-echo-equivalence`). absolute-zero lives under `…/verification-ecosystem/maa-framework/`. Planned, not built. -* Docs: `docs/ProofRoadmap.md` §10, `docs/EchoJanusBridge.md`. +* Docs: `roadmap.adoc` §"Deferred research track", `docs/EchoJanusBridge.md`. === Shannon / information theory `[OPEN]` Explicitly *not bridged*. The Transport / Nyquist sampling work @@ -197,10 +197,11 @@ are kept for history and **may overclaim** (pre-retraction). | `INDEX.adoc` is the *audit* index (different role; keep) | Proof status / roadmap -| `docs/echo-types/earn-back-plan.adoc` + `docs/retractions.adoc` -| `ProofRoadmap.md`, `PRIORITIZED_PROOF_ROADMAP.md`, `WORK_PLAN.md`, - `roadmap.adoc`, `roadmap-gates.adoc`, `docs/echo-types/roadmap.md` - (pre-R-2026-05-18 — historical) +| `roadmap.adoc` (single canonical roadmap; lanes, gates, deferred + research) + `docs/echo-types/earn-back-plan.adoc` + + `docs/retractions.adoc` +| `roadmap-gates.adoc` (pre-R-2026-05-18 — historical; folded into + `roadmap.adoc`) | Concept / definition | `docs/echo-types/overview.md`, `docs/echo-types/paper.adoc` diff --git a/docs/echo-types/abstraction-barrier.adoc b/docs/echo-types/abstraction-barrier.adoc new file mode 100644 index 0000000..56d95a5 --- /dev/null +++ b/docs/echo-types/abstraction-barrier.adoc @@ -0,0 +1,184 @@ += The Echo abstraction barrier (consumer-side, narrow scope) +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +Companion essay to `proofs/agda/EchoAbstractionBarrier.agda`. The +module ships two theorems and a deliberately narrow scope. This file +explains the narrowness — what the abstraction barrier is, what it +guarantees, what it does *not* guarantee, and why the narrow form is +the strongest honest statement available under +`--safe --without-K`. + +[IMPORTANT] +==== +This is Track B of the "Echo ≠ Σ" identity-claim consolidation +(`roadmap.adoc` §Lane 2; sceptic-facing map at +`core/skepticisms/is-this-just-sigma-types.md` §4). The theorems below +respect the R-2026-05-18 retraction discipline: the claim is a +*consumer-side free theorem at the headline affine instance*, NOT a +general Reynolds-style parametricity result. The scope narrowness is +load-bearing. +==== + +toc::[] + +== What an abstraction barrier means here + +A raw dependent pair `Σ A (λ x → f x ≡ y)` exposes `proj₁`. A consumer +of such a pair can always recover the original `x`. That makes the +"forgetting" half of any loss-grade story a *convention*, not a +guarantee — nothing in the type stops the consumer from looking. + +The Echo interface, at the affine mode, refuses to export `proj₁`. +But "refuses to export" is meaningless prose without a checked +artefact: a sceptic reasonably asks "what stops me writing +`proj₁ ∘ to-sigma`?" The abstraction barrier is the answer. It is +the pair of theorems that, together, say: + +. *At the affine instance, no consumer can do what the Σ-projection + does.* (Theorem `affine-consumer-cannot-distinguish`.) +. *The Σ-projection does it.* (Theorem `sigma-distinguishes`.) + +The first is the guarantee. The second is the negative companion that +makes the guarantee non-trivial: it exhibits the concrete behaviour +the affine interface is designed to prevent. + +== The two theorems + +=== `affine-consumer-cannot-distinguish` + +[source,agda] +---- +affine-consumer-cannot-distinguish : + {X : Set ℓ} (g : LEcho affine → X) → + g (weaken echo-true) ≡ g (weaken echo-false) +affine-consumer-cannot-distinguish g = + cong g (affine-all-equal (weaken echo-true) (weaken echo-false)) +---- + +Any consumer `g` at the affine mode produces the same result on the +two known-distinct linear echoes (`echo-true` and `echo-false`) after +they have been weakened. This holds *for every consumer type* `X` and +*every function* `g : LEcho affine → X`, because the affine residue +carrier is contractible — `EchoLinear.affine-canonical` and +`affine-all-equal` discharge it in one `cong`. + +The reason this is non-trivial: the underlying linear echoes ARE +distinguishable. `EchoCharacteristic.echo-true≢echo-false` is a +theorem. The barrier is that crossing from linear to affine via +`weaken` collapses the distinction *structurally*, and no affine +consumer can recover it. The Σ-projection on the linear side would +recover it; the Σ-projection on the affine side cannot, because the +affine carrier has only one inhabitant up to definitional equality. + +=== `sigma-distinguishes` + +[source,agda] +---- +sigma-distinguishes : + Σ (Echo collapse tt → Bool) + (λ g → g echo-true ≢ g echo-false) +sigma-distinguishes = proj₁ , true≢false +---- + +The Σ-projection `proj₁ : Echo collapse tt → Bool` IS a consumer that +distinguishes `echo-true` from `echo-false`. The proof is `true≢false` +directly, because `proj₁ (echo-intro collapse true)` reduces +definitionally to `true` (via `echo-intro f x = x , refl`) and the +mirror case reduces to `false`. + +This is the load-bearing artefact. Without it, the claim "the affine +interface refuses `proj₁`" is content-free — what would `proj₁` even +do? The negative companion answers exactly that question, and the +answer is "distinguish the two linear echoes". The affine interface +deliberately refuses to export it. + +== What this is NOT + +The scope guardrail in the module preamble lists three narrowings. +They are repeated here in essay form because external readers tend to +read essays before module headers, and the narrowings are the most +load-bearing thing about this module. + +=== Not full Reynolds parametricity + +A general Reynolds-style result would say: for every consumer type +`X`, every echo carrier `A`, every map `f : A → B`, every output +`y : B`, and every function `g : Echo f y → X` *at the appropriate +interface*, `g` cannot inspect `x` beyond what the interface allows. +Agda has no parametricity primitive. Stating this requires either an +axiom or a paper-level metatheorem. Both violate the no-postulate +invariant. + +The narrow form here — consumer-side at the headline affine instance +— is what survives `--safe --without-K`. It says the right thing at +the one instance where the carrier is contractible and the +quantification over consumers (`{X : Set ℓ}`) is non-vacuous because +*every* consumer satisfies the equation. + +=== Not a higher-order parametricity claim + +`affine-consumer-cannot-distinguish` does not claim that consumers +*cannot detect the difference between two linear preimages*. It +claims that consumers *of weakened linear preimages* assign them the +same value. The detection happens on the linear side (and is the +content of `echo-true≢echo-false`); the barrier is at the +linear→affine boundary, and the theorem is what survives crossing it. + +=== Not a categorical universal property + +The Echo interface is not characterised in this module as a terminal +cone over anything. The pullback characterisation lives in +`EchoPullback.agda` and is itself narrowed (per R-2026-05-18) to a +funext-relative pointwise mediator property. The abstraction barrier +here is a separate, narrower claim that does not depend on the +pullback machinery. + +== Why two theorems and not one + +A single positive theorem (`cannot-distinguish`) is a wish without +the negative companion. The reader can always ask: "but couldn't some +other consumer, written cleverly, distinguish them anyway?" The +answer at the affine instance is *no*, and the reason is structural +(`affine-canonical`). But the reader's question deserves a checked +answer, not a structural argument. The negative companion provides +it: the only consumer that distinguishes the two linear echoes is +`proj₁` or a function of `proj₁`, and that is *exactly* the function +the affine interface refuses to export. + +The pair is the artefact. Either alone is half the story. + +== Honest comparison to neighbour disciplines + +* *Granule / QTT.* Stronger general parametricity available via the + language's quantitative judgments. Echo's claim here is narrower + (instance-level, consumer-side, in Agda without a parametricity + primitive). See `docs/echo-types/comparators.adoc` for the + axis-by-axis breakdown. +* *Linear Haskell.* The linearity-mode information is at the type + level but Haskell consumers can still inspect linear values via + `seq` and other escape hatches. Echo's contractibility argument + closes that gap at the affine carrier specifically, because the + carrier *is* a singleton up to definitional equality. +* *Lens / optic laws.* The witness-transport leg of `map-over` looks + optic-shaped but the affine-mode contractibility argument has no + optic analogue: lenses can inspect their source via `view`. Echo's + refusal of `proj₁` at affine mode is the structural difference. + +== Cross-references + +* Agda module: `proofs/agda/EchoAbstractionBarrier.agda` (this file's + companion). +* Sceptic-facing map: `core/skepticisms/is-this-just-sigma-types.md` + §4 and `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 4". +* The retraction governing the narrowing discipline: + `docs/retractions.adoc` R-2026-05-18. +* Carrier-parametricity (model side): `EchoRelModel.agda` and + `docs/echo-types/conservativity.adoc`. That work is at the *model* + level (Pillar D); this module is at the *consumer* level — the two + are not the same statement. +* Comparator framing: `docs/echo-types/comparators.adoc`. diff --git a/docs/echo-types/applications-compiler-analysis.adoc b/docs/echo-types/applications-compiler-analysis.adoc index c66f59b..237e6bf 100644 --- a/docs/echo-types/applications-compiler-analysis.adoc +++ b/docs/echo-types/applications-compiler-analysis.adoc @@ -318,5 +318,5 @@ be expanded to a fully worked Agda exhibit: exhibiting tolerance accumulation through `echo-approx-compose`. -Both are tracked as `[unblocked]` items in `roadmap.md` +Both are tracked in `roadmap.adoc` as deferred examples-library work (`Add example-library Agda files matching examples.md`). diff --git a/docs/echo-types/buchholz-rank-obstruction.adoc b/docs/echo-types/buchholz-rank-obstruction.adoc index 1b0d306..60f3ad2 100644 --- a/docs/echo-types/buchholz-rank-obstruction.adoc +++ b/docs/echo-types/buchholz-rank-obstruction.adoc @@ -303,22 +303,34 @@ constructors discharge by additive-principal closure. | `<ᵇ-ψ+` | ✓ closed | `rank-pow-via-left` plus the IH. | `<ᵇ-+Ω` | ✓ closed | `rank-pow-bplus-into-ω-rank-pow` (additive-principal at the target) plus the WfCNF tail bound `y ≤ᵇ x` (caller-provided). | `<ᵇ-+ψ` | ✓ closed | Same as `<ᵇ-+Ω` since `rank-pow (bpsi ν _) = ω-rank-pow ν`. -| `<ᵇ-ψα` | ⏳ admissibility | `rank-pow (bpsi ν α) = ω-rank-pow ν` doesn't discriminate on α. Refining the rank to `ω-rank-pow ν ⊕ rank-pow α` works iff `α ∈ C_ν` (ψ-admissibility predicate); deferred to a follow-on slice. -| `<ᵇ-ψΩ≤` | ⏳ admissibility | Same blocker at `ν = μ`: provisional shape gives `ω-rank-pow μ <′ ω-rank-pow μ`, which is false. +| `<ᵇ⁺-ψα` | ✓ closed (Lane 3, 2026-05-26) | `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`; `⊕-mono-<-right` closes the shared-Ω-index lex case from `rank-pow α <′ rank-pow β` (which the existing `_<ᵇ⁰_` umbrella discharges). Primitive `rank-mono-<ᵇ⁺-ψα-from-pow` in `Ordinal.Buchholz.RankAdm`. +| `<ᵇ-ψΩ≤` | ✓ closed (Lane 3 follow-on, 2026-05-27) | Lex-pair rank `rank-lex : BT → RankLex` in `Ordinal.Buchholz.RankLex`, with `rank-lex (bOmega ν) = mkLex (ω-rank-pow ν) (ω-rank-pow ν)` and `rank-lex (bpsi ν α) = mkLex (ω-rank-pow ν) (rank-pow α)`. Both sub-cases close via `rank-mono-<ᵇ-ψΩ≤-lex`: ν<μ via `/verify.agda` (or `.idr`/`.lean` as the target's + proof assistant requires). Each lemma states the round-trip + property between the echo-types in-tree mirror (e.g. + `EchoJanusBridge.OpKind`) and the live target type (e.g. + januskey's `src/abi/Types.idr` `OpKind`). The CI seam is *this + lemma typechecking*, not the targets themselves typechecking + against echo-types. +. *CI matrix* per bridge: a build job that bumps the submodule + pin, runs the verify lemma, and reports green/red. Red is a + bridge-CI signal, not a target-repo signal — neither this repo + nor any target is gated on bridge-CI green. + +== What stays in echo-types after option A is built + +The current in-tree bridge modules +(`EchoJanusBridge.agda`, `EchoTropical.agda`, `EchoCNOBridge.agda`, +`DyadicEchoBridge.agda`) *stay where they are*. They are the local +structural mirrors that the bridge-CI verified-translation lemmas +target on the echo-types side. Deleting them would break the +bridge-CI lemmas without strengthening this repo. The roadmap +should reflect: "in-tree mirrors are the canonical Agda statement +of the bridge interface; round-trip verification against the live +target is in `echo-bridges-ci`." + +== Open question this decision deliberately leaves + +The Tropical bridge does not point at a single canonical target +repo today (the tropical decoration is a mathematical pattern, not +a codebase). When Lane 4 unparks, the Tropical bridge either (a) +finds a concrete consumer to verify against, or (b) stays as the +in-tree `EchoTropical.agda` plus `AntiEchoTropical.agda` / +`AntiEchoTropicalGeneric.agda` and is *not* migrated into +`echo-bridges-ci`. Option (b) is the honest default; option (a) +requires a named consumer. + +== Status + +Decision: *option A adopted as of 2026-05-26*. + +Lane 4 status: still *PARKED*. This document does not unpark it. +The unblocking condition (Lane 1 closes per `roadmap.adoc` Lane 1 +close-out criterion) is unchanged. + +When Lane 4 unparks, the first three actions are: + +. Create `hyperpolymath/echo-bridges-ci` per §"What option A looks + like at unpark time". +. Migrate the JanusBridge round-trip from a structural mirror to a + verified-translation lemma against the live januskey + `src/abi/Types.idr` `OpKind`. +. Migrate the CNO bridge analogously. + +That sequence is *not* started in this session; recording it here +saves the next session from re-deriving the unpark plan. + +== References + +* `roadmap.adoc` §"Lane 4 [PARKED] — Bridges-CI" +* `docs/bridges/cross-repo-bridge-status.md` — current per-bridge status +* `proofs/agda/EchoJanusBridge.agda`, `EchoTropical.agda`, + `EchoCNOBridge.agda`, `DyadicEchoBridge.agda` — in-tree mirrors +* `CLAUDE.md` §"Ecosystem context" — list of adjacent target repos diff --git a/docs/echo-types/decisions/no-2-cat.adoc b/docs/echo-types/decisions/no-2-cat.adoc index 60c69e3..df3839a 100644 --- a/docs/echo-types/decisions/no-2-cat.adoc +++ b/docs/echo-types/decisions/no-2-cat.adoc @@ -6,7 +6,7 @@ :icons: font [.lead] -Closure note for the `roadmap.md` entry +Closure note for the `roadmap.adoc` entry "2-categorical shape: commit to a 2-category or rule it out" and for `composition.md` §Q1 / §Q6. The verdict is *rule out*, on argued grounds against the landed Pillars A–D evidence. The @@ -115,7 +115,7 @@ None is on the active roadmap. The verdict stands. == Cross-references -* `docs/echo-types/roadmap.md` — Theory-work entry updated to +* `roadmap.adoc` — Theory-work entry updated to `[ruled out]`. * `docs/echo-types/composition.md` §Q1 / §Q4 / §Q6 — open framings folded into this closure. diff --git a/docs/echo-types/decisions/presentation-dependence.adoc b/docs/echo-types/decisions/presentation-dependence.adoc index 029dc00..66ce29e 100644 --- a/docs/echo-types/decisions/presentation-dependence.adoc +++ b/docs/echo-types/decisions/presentation-dependence.adoc @@ -6,7 +6,7 @@ :icons: font [.lead] -Closure note for the `roadmap.md` entry +Closure note for the the legacy `roadmap.md` (now consolidated into `roadmap.adoc`) entry "Presentation-dependence sub-theory: examples 5, 9, 10 cluster here; write up the common pattern". The verdict is *meta-pattern only — no new Agda module needed*: presentation-dependence is the existing @@ -196,7 +196,7 @@ Concretely: == Cross-references -* `docs/echo-types/roadmap.md` — Theory-work entry updated to +* `roadmap.adoc` (legacy `docs/echo-types/roadmap.md` consolidated 2026-05-26) — Theory-work entry updated to `[landed — see decisions/presentation-dependence.adoc]`. * `docs/echo-types/taxonomy.md` §Axis 4 — the existing axis this cluster instantiates; its "Open question" is sharpened (not diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index 23d70f7..d799087 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -81,12 +81,17 @@ kernel** — the boundary is real and lives outside this core. `EchoExampleAbsInt`, `EchoExampleParser`, `EchoExampleProvenance`, `EchoExampleSignAnalysis`, `EchoExampleTruncation`, `EchoSearchExample`, `EchoThermodynamicsArbitrary`, - `EchoThermoCollapseImpossible` + `EchoThermoCollapseImpossible`, `EchoAbstractionBarrier` | Multi-hop. `EchoThermodynamics` reaches the kernel via `EchoFiberCount` (no direct `Echo` import); `EchoThermodynamicsFinite` is its Bishop-finite transport layer. `EchoSearch` / `EchoCost` / `EchoAccess` are Axis 8 witness-search - and cost-model extensions. `EchoExample*` are derived domain + and cost-model extensions. `EchoAbstractionBarrier` is the + Lane 1 / Lane 2 consumer-side free-theorem artefact (Track B — + `affine-consumer-cannot-distinguish` plus raw-Σ counter-program + `sigma-distinguishes`); imports `Echo` + `EchoCharacteristic` + + `EchoLinear`, landed 2026-05-26 via PR #119. `EchoExample*` are + derived domain applications. | *Earn-back gate modules* + diff --git a/docs/echo-types/establishment-plan.adoc b/docs/echo-types/establishment-plan.adoc index bdab053..24ad45b 100644 --- a/docs/echo-types/establishment-plan.adoc +++ b/docs/echo-types/establishment-plan.adoc @@ -8,7 +8,7 @@ [.lead] This document sets out the path by which "echo types" can acquire *recognised type-theoretic standing*. It is deliberately separate from -`roadmap.md` (work partitioned by bottleneck) and `roadmap-gates.adoc` +`roadmap.adoc` (work partitioned by lane) and `roadmap-gates.adoc` (the falsifiable identity claim). This document answers a different question: _given_ the gated identity claim, what makes a construction like this *established* in the sense that linear, dependent, or graded @@ -223,7 +223,7 @@ programme is done; only Pillar E (external validation) remains.* A–C were the credibility core and needed no external unblocker. The ordinal / Buchholz track is impressive _consumer evidence_, not foundation — keep it -firewalled from the identity claim exactly as `roadmap.md` already does. +firewalled from the identity claim exactly as `roadmap.adoc` already does. *Hard guardrails (credibility hazards):* diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc index a1bbeb0..e863fa0 100644 --- a/docs/echo-types/paper.adoc +++ b/docs/echo-types/paper.adoc @@ -19,6 +19,21 @@ abstract (`types-abstract.adoc`) is the short, already-submission-ready companion; this is the full CPP/ITP-style mechanised-metatheory paper it grows into. + +*Pillar E in-repo close-out (2026-05-26).* Of the four `[EXPAND]` +tags originally on this paper: tag 1 (background / notation primer) +cleared in PR #73; tag 2 (related work — Granule / QTT, +Uustalu–Vene comonads, coeffects, lens/optic vs witness-transport +leg) cleared in PR #120, with the single-page reviewer companion at +`docs/echo-types/comparators.adoc` shipping the axis-by-axis +summary; tag 3 (evaluation — proof-size / cost table, honest +account of the common-upper-bound idiom) cleared earlier in PR #84 +(see §"Evaluation and discussion"). Tag 4 (ordinal consumer-evidence +appendix) is the only one remaining open, and it is *gated* on the +ordinal-track milestone per `roadmap.adoc` §Lane 3 — not a missing +deliverable for the in-repo half of Pillar E. Everything else +(venue choice, Zenodo DOI, library packaging, outreach) is +author-driven and is flagged but not auto-run. ==== toc::[] @@ -554,7 +569,6 @@ mechanised strength, neither less nor more. === Proof size per pillar -<<<<<<< HEAD The four pillars together occupy ~930 lines across six modules, with zero postulates and three `rewrite` sites (one in the foundational `degrade-compose`; one in its `rel-model` lift; one in @@ -1134,26 +1148,21 @@ Swamy et al. "Dependent types and multi-monadic effects in F\*" (POPL 2016); Vazou–Seidel–Jhala–Vytiniotis–Peyton Jones "Refinement types for Haskell" (ICFP 2014, Liquid Haskell). -======= -NOTE: *[EXPAND]* — detailed positioning against: Granule / QTT graded -modalities; comonadic notions of computation (Uustalu–Vene); -coeffects (Petriček–Orchard–Mycroft); HoTT fibrewise constructions; -lens / optic literature (the witness-transport leg of -`echo-pullback-univ` resembles the very-well-behaved *1-lens* laws — -no 2-cell-equipped optic, see below). Make the novelty crisp: not a -new object, but a fully mechanised characterisation package with a -falsifiable-gate methodology. - -NOTE: *[2-cat ruled out, see `decisions/no-2-cat.adoc`]* — when the -related-work pass expands the lens/optic comparison and the -graded-modality positioning, fold in the 2-categorical rule-out: a -"bicategorical echo" reading was considered and ruled out on the -landed evidence (every would-be 2-cell appears as `refl` or is -prop-forced trivial by `≤g-prop` / `⊑-prop`); the construction -resembles a very-well-behaved *1-lens*, not a 2-cell-equipped optic. -The closure note in `decisions/no-2-cat.adoc` is the load-bearing -artifact; this paragraph should cite it rather than re-argue. ->>>>>>> docs/rule-out-2cat-and-roadmap-correction + +NOTE: *Related-work `[EXPAND]` cleared 2026-05-26.* The original +`[EXPAND]` TODO requested detailed positioning against Granule / QTT +graded modalities, Uustalu–Vene comonads, Petriček–Orchard–Mycroft +coeffects, HoTT fibrewise constructions, and the lens / optic +literature with the 1-lens-vs-2-cell-optic clarification. That work +has been delivered above in §"HoTT homotopy fibres", §"Graded comonads, +coeffects, and QTT", and §"Lenses and optics (the witness-transport +leg)" — including the explicit 2-categorical rule-out at the end of +the lens/optic subsection (`docs/echo-types/decisions/no-2-cat.adoc` +is the load-bearing closure note). A companion single-page comparator +table at `docs/echo-types/comparators.adoc` (Echo vs Granule / QTT / +choreographic / Linear Haskell) ships the axis-by-axis summary form +for reviewers who want the at-a-glance positioning rather than the +prose narrative above. [#reframing-note] == Reframing note (2026-05-18) @@ -1204,44 +1213,6 @@ via a genuine non-graph `StepND` model (§6 NOTE, `EchoStepNDModelF2.agda`). The graded-comonad, modality-level model-independence, and conservativity rows remain fully retracted. -[#reframing-note] -== Reframing note (2026-05-18) - -This draft was reframed after an adversarial three-reviewer review -(graded-modality, semantics, and proof-assistant skeptics) found that -the codebase contains no defense for five central claims, and that -two were contradicted by the repository's own Gate-2 audit. The -following claims were retracted, not weakened cosmetically: - -[cols="2,3", options="header"] -|=== -| Retracted claim | Replaced by - -| "graded comonad" (counit/comultiplication, three comonad laws) -| loss-graded *reindexing modality*; no nested `D_r D_s` is formed; - the equations hold by thinness of the grade order - -| "terminal-cone universal property"; "a category theorist accepts - echo as the limit of a cospan" -| a *pointwise, funext-relative* mediator property; full terminality - is unstatable here without funext - -| "model independence across two agreeing models" -| carrier-parametricity over a *fixed* grade poset; the second model - is the first with a `⊤` component, agreeing by `refl` - -| "conservativity metatheorem, discharged operationally by the build" -| a *postulate-free build*: evidence for, not a proof of, - conservativity over MLTT+Σ - -| "funext quarantined behind an isolated module; no result crosses it" -| no funext anywhere; the real funext-relativity is the pointwise - mediator property, now disclosed as the boundary -|=== - -The full per-attack analysis and the codebase pressure-test are in -`docs/retractions.adoc`. - == Conclusion Echo is the homotopy fibre equipped with a loss-grade lattice, diff --git a/docs/echo-types/pillar-e-offline.adoc b/docs/echo-types/pillar-e-offline.adoc new file mode 100644 index 0000000..15c2ad7 --- /dev/null +++ b/docs/echo-types/pillar-e-offline.adoc @@ -0,0 +1,395 @@ += Pillar E offline: prep doc for venue, packaging, outreach +:toc: macro +:toclevels: 3 +:sectnums: +:icons: font + +[.lead] +Pillar E's in-repo half is at close-out (see `paper.adoc` IMPORTANT +banner and `roadmap.adoc` §Lane 1). This document pre-stages the +*offline / author-driven* half — venue + template choice, Zenodo +DOI mint, library packaging, outreach to neighbour communities — so +the user can act on each item without re-deriving the analysis. + +[IMPORTANT] +==== +*The actions in this document are author-driven.* Nothing here is +auto-run. Drafts of cover letters and packaging scaffolds land in +the repo as text for the user to send / publish at their cadence. +==== + +toc::[] + +== Venue + template matrix + +Four candidate venues, ordered by *fit to the current narrowed +claim*. The narrowed claim (per R-2026-05-18) is a definitional +Σ-identity + funext-relative pointwise mediator property + thin- +poset reindexing modality + separating model + carrier-parametric +abstraction over a fixed grade poset + postulate-free +`--safe --without-K` build, under a falsifiable retraction +discipline. The right venue is one whose reviewers will read that +package on its actual strength rather than against the original +graded-comonad framing the retraction note walks back. + +[cols="1,2,2,3,2", options="header"] +|=== +| Venue +| Format +| Typical deadline cadence +| Fit to narrowed claim +| Recommendation + +| TYPES (extended abstract) +| ~2 pp AsciiDoc / LaTeX +| Annual, spring deadline +| *Best fit.* The community already accepts work-in-progress retraction-style pieces; the existing `types-abstract.adoc` is already drafted at the right shape; the audience knows graded modalities and will read the narrowed claim on its own terms. +| *Submit first.* Lowest revision cost, highest probability of audience-appropriate review. + +| CPP +| ~10 pp ACM template +| Annual, fall deadline (Jan target) +| Strong fit. CPP's "Certified Programs and Proofs" framing is exactly what the postulate-free `--safe --without-K` artefact is. Reviewers expect a full mechanised metatheory, which `paper.adoc` already is. +| *Submit second*, after TYPES feedback. CPP rewards exactly the kind of artefact carefully captured here. + +| ITP +| ~15 pp LIPIcs template +| Annual, late winter deadline (Mar target) +| Strong fit on the mechanised side. Audience overlaps CPP but is more proof-assistant-centric; the discussion of `--safe --without-K` + zero postulates + Smoke discipline lands harder here. +| *Alternative to CPP* if CPP timing slips. Don't dual-submit; pick one of CPP/ITP based on which deadline lands first. + +| MSCS journal (or Logical Methods in Computer Science) +| ~25 pp journal article +| Rolling +| Best fit if the paper grows substantially (e.g. consumer-evidence appendix lands once Bachmann-Howard hits). Journal length removes the "evaluation section is brief" pressure. +| *Hold for v2.* After TYPES + CPP cycles produce reviewer feedback, the consolidated journal version is the final form. +|=== + +=== Recommended sequencing + +. *TYPES extended abstract.* `types-abstract.adoc` already exists + in `--safe --without-K`-aware form. Action items: + + .. Pick the year (whichever TYPES has the next submission window). + .. Re-review the abstract against the current paper for any + residual stale phrasings (the abstract carries a `NOT + submission-ready` banner because the original was retracted; the + correction has happened, the banner should be updated to + `submission-ready as of ` once the user signs off). + .. Format under the TYPES template (LaTeX). The content + translation is mechanical; I can prep the LaTeX source as a + parallel file `types-abstract.tex` if requested. + .. Submit. Author metadata, affiliation, ORCID — user only. +. *CPP submission.* Two-month cycle after TYPES. Use `paper.adoc` + as the spine; cut to ~10pp by trimming the §"Evaluation and + discussion" inline narrative (keep the cost table). Convert to + ACM template. +. *Hold ITP and MSCS for v2.* Don't bundle. + +=== What I cannot help with on venue + template + +* Author-metadata blocks (ORCID, affiliation, conflict declarations). +* Cover letters to programme chairs. +* Pre-submission emails to area chairs (when appropriate). +* The actual submission upload. + +These are author-driven by venue rule. + +== Zenodo DOI mint + +The DOI ladder for a mechanised artefact paper: + +. *Concept DOI* — a stable DOI for the project as a whole + (`hyperpolymath/echo-types`), minted once. +. *Version DOI* — per tagged release. Each `git tag vX.Y.Z` should + publish to Zenodo via the GitHub→Zenodo webhook. +. *Citation block* in README + paper artefact statement — + citation by Zenodo DOI rather than commit hash so reviewers cite + a stable target. + +=== What I can pre-stage in-repo + +. `CITATION.cff` at the repo root with the project metadata, + author block, abstract (cribbed from `types-abstract.adoc`), + license (MPL-2.0 per the recent estate sweep), and a placeholder + for the DOI to fill in after first mint. This file is consumed + by GitHub's "Cite this repository" widget and is the canonical + citation source. +. `.zenodo.json` with the matching metadata in Zenodo's format, + including: + - `creators` block (author, ORCID once supplied) + - `keywords`: `["agda", "graded modality", "homotopy fibre", + "loss grading", "formal methods", "echo types"]` + - `related_identifiers` linking to the GitHub repo + - `communities`: TBD on user preference (e.g. `agda`, + `formal-methods`) +. A tag-driven CI workflow `.github/workflows/zenodo-release.yml` + that fires on `v*` tags and triggers the GitHub→Zenodo + integration (after the user has authorised the integration in + Zenodo's GitHub settings). The workflow itself doesn't push to + Zenodo; it just stamps the release notes and pings the existing + webhook. + +=== What the user does + +. Create / log into a Zenodo account. +. Authorise the GitHub→Zenodo integration for + `hyperpolymath/echo-types` (one-click flip in Zenodo settings). +. After the integration is on, push the first `v0.1.0` tag from + `main` after PR #118 lands. Zenodo will mint both the concept + DOI and the v0.1.0 version DOI automatically. +. Paste the concept DOI back into `CITATION.cff` (the placeholder + I leave there) and commit. Same for `.zenodo.json`. + +This is a 15-minute author-driven sequence once Zenodo is hooked. + +*Pre-staging status (updated 2026-05-27).* `CITATION.cff` and +`.zenodo.json` are both landed at the repo root with placeholder +DOI (`10.5281/zenodo.0000000`) and creator block (ORCID commented +out — supply on author setup). The README citation section +(`README.md` §Citation) points at `CITATION.cff` and at this +document's §"Zenodo DOI mint" for the activation sequence. The +GitHub→Zenodo workflow itself is intentionally NOT pre-staged +because activating it before the user has authorised the Zenodo +integration would cause CI runs to fail noisily; the workflow +lands as a small follow-on once the integration is on. + +== Library packaging + +Standard Agda library layout for an installable `echo-types.agda-lib`: + +[source,text] +---- +echo-types.agda-lib -- name/include/depend +proofs/agda/ -- existing tree (no move) +tutorial/ -- Lane 5 walkthrough tree +docs/ -- existing tree +README.md / readme.adoc -- existing +LICENSE -- existing (MPL-2.0) +CITATION.cff -- new (Zenodo prereq) +.zenodo.json -- new (Zenodo prereq) +---- + +The `.agda-lib` file's content: + +[source,text] +---- +name: echo-types +depend: standard-library +include: proofs/agda + . +---- + +That's it. The dual `include` lets a consumer use either bare +`Echo` (resolved against `proofs/agda`) or `tutorial.region_exit_audit.RegionExitAudit` +(resolved against the repo root). Anyone with stdlib v2.3 in their +Agda libraries file can then `agda --library echo-types ...` after +running the standard registration step. + +Action items I can land as a single commit: + +. `echo-types.agda-lib` at the repo root. +. README section documenting the standard install: ++ +[source,bash] +---- +git clone https://github.com/hyperpolymath/echo-types.git +echo "$(pwd)/echo-types/echo-types.agda-lib" >> ~/.agda/libraries +---- +. CI seam: an "install-self" job that runs + `agda --library echo-types -- proofs/agda/All.agda` to prove the + packaging works end-to-end. + +*Pre-staging status (updated 2026-05-27).* Items 1 (`echo-types.agda-lib` +with dual `include: proofs/agda .`) and 2 (README §"Build" > +"Installing as a library" subsection with the registration and +consumer-side `depend:` snippet) are both landed. Item 3 (CI +install-self job) is deferred so it can be wired alongside the +GitHub→Zenodo workflow once the user authorises the integration — +both are downstream of the same author-driven setup, and bundling +them avoids a transient CI red between the two PRs. + +== Outreach drafts + +Three target communities, in priority order. Each cover letter is +a draft for the user to send (mailing-list post, direct email, or +forum post — venue depends on the community's norms). + +The pattern in each draft: +. Open with the *narrowed* claim, not the original claim. +. Cite the retraction note as evidence of the discipline. +. Link to the comparators page, not the full paper. +. Ask one specific question, not a generic + "what-do-you-think". + +=== Draft 1: Granule / QTT (graded modality community) + +Target list: Granule mailing list / Discord, Atkey research group +mailing list, or POPL programme chairs with graded-modality +interests in the year of submission. + +Draft text: + +[quote] +---- +Subject: Echo types — a calibration against graded modalities, with +a public retraction discipline + +Hi all, + +We've been working on echo-types, an Agda formalisation of +fibre-based "structured loss" types. The original framing claimed +echo as a graded comonad in the Petriček-Orchard-Mycroft sense; +this turned out to be wrong on careful re-reading and was retracted +on 2026-05-18 (R-2026-05-18 in our public retraction log, +`docs/retractions.adoc`). The narrowed claim is a loss-graded +*reindexing modality* (thin-poset action; no nested D_r D_s) over a +join-semilattice of loss grades. + +The reason I'm writing to this community in particular: we've +landed a *separating model* (`EchoSeparating.agda`) that quantifies +exactly the modality's content over generic Σ-functoriality. It is +`EchoGraded` minus `≤g-prop` (propositionality of the loss order), +and the characteristic composition equation is refuted at a +concrete decidable witness when `≤g-prop` is removed. This locates +the load-bearing hypothesis precisely. + +I'd value a sanity check from this community on whether the +separating-model framing makes sense, and whether echo is best +read as one of: + +(a) a degenerate case of QTT / Granule that doesn't need its own + name; +(b) a meaningful sibling within the coeffect / graded family worth + distinguishing; +(c) something the community already has a better name for. + +The single-page reviewer companion is at +`docs/echo-types/comparators.adoc` and lays out axis-by-axis +positioning against Granule, QTT, choreographic types, and Linear +Haskell. The full mechanised metatheory paper is `paper.adoc`. + +Either direction of feedback would be a real contribution to the +discipline; we have no investment in (b) being right. + +— [User name] +---- + +=== Draft 2: choreographic types community + +Target: Hirsch et al. choreographic-types research group, or POPL +/ ICFP authors of the recent choreographic-types papers. + +Draft text: + +[quote] +---- +Subject: Choreographic bridge in echo-types — a possibly-degenerate +RoleEcho construction + +Hi [name], + +We have a small Agda formalisation `EchoChoreo.agda` that mirrors +the role-projection structure of choreographic types via a +role-indexed echo `RoleEcho r y = Echo (obs r) y`. The construction +is in our project echo-types +(`hyperpolymath/echo-types`). + +Where I'd value a second opinion: in our Gate 2 audit +(`docs/characteristic.adoc`), the lemma +`applyChoreo-compose` survives as a characteristic theorem +because we can't reduce it to a generic Σ-fibre lemma. But our +own EI-2 investigation +(`docs/EI2_REPORT.adoc`) showed that across attempted +2D/3D integrations of role, mode, and grade decorations, only the +`(c⊑s, keep≤keep)` cell carries non-trivial cross-axis content, +and it factors through Choreo's `client-to-server` step. + +The question I have for the choreographic-types community is +whether this is the *expected* shape of role-projection +non-triviality (Choreo content dominates because choreographic +projection is the only non-loss-preserving direction on the role +lattice) — or whether we have a degenerate role lattice that +collapses non-trivial cross-axis content we should have seen. + +Comparators page: `docs/echo-types/comparators.adoc`. The +choreographic comparison axis is the relevant section. + +— [User name] +---- + +=== Draft 3: Linear Haskell / substructural types community + +Target: Linear Haskell mailing list, Haskell Symposium PC, or +substructural-types research mailing lists. + +Draft text: + +[quote] +---- +Subject: Echo types' affine bridge as a worked weakening example + +Hi all, + +Our echo-types project (`hyperpolymath/echo-types`) ships a +two-mode (linear ⊑ affine) linearity decoration in +`EchoLinear.agda`. The construction is small: weakening +linear→affine is `EchoResidue.collapse-to-residue`, the +no-recovery guarantee is `no-section-weaken`, and the +characteristic Gate 2 lemma `degradeMode-compose` falls out by +composition + propositionality of the mode order. + +A new tutorial walkthrough +(`tutorial/region_exit_audit/RegionExitAudit.agda`) instantiates +this at an ephapax-style region exit, with the explicit honest- +bound disclosure that the audit guarantee is type-level (no pure +function reconstructs the live handle from the receipt) and is +NOT a runtime memory-zeroing claim. + +The question for this community: is the "consume on exit produces +an affine audit receipt" pattern already a known idiom in the +Linear Haskell / Linear Constraints world? If so, the right +positioning of our walkthrough is "a small Agda mechanisation of a +Haskell-side pattern", not "a new construction". + +Comparators page: `docs/echo-types/comparators.adoc`. The Linear +Haskell comparison axis is the relevant section. + +— [User name] +---- + +== Cross-cutting honest disclosures + +Each outreach contact should also surface (without leading with): + +. The retraction log (`docs/retractions.adoc`) is *append-only*; + the R-2026-05-18 narrowing has not been re-opened. +. The Gate 2 audit is at *Revision 5* (re-audited 2026-05-26 per + Lane 2 close-out). The threshold is met by margin of one. +. The project's only non-zero load-bearing dependency is + `agda-stdlib v2.3`. No funext, no postulates, no escape pragmas. + +These are not strengths to brag about; they are the discipline that +makes the narrowed claim defensible. Mentioning them up front in +follow-up email exchanges is a credibility multiplier; leading +with them in a cold outreach is over-claiming. + +== Action checklist for the user + +In order: + +. [ ] Choose TYPES year. (Author-only.) +. [ ] Ask me to pre-stage `CITATION.cff` + `.zenodo.json` + + `echo-types.agda-lib` (single follow-up PR). +. [ ] Create Zenodo account; flip the GitHub→Zenodo integration on. +. [ ] (Triggered by PR #118 landing.) Push `v0.1.0` tag. +. [ ] Paste back the concept DOI into `CITATION.cff` + `.zenodo.json`. +. [ ] Send Draft 1 (Granule / QTT community) when the user is + ready. The other two drafts go out only after at least one + response to Draft 1 — the staggering avoids contradictory + messaging if Draft 1 produces a course correction. +. [ ] Submit TYPES extended abstract. +. [ ] (Two-month gap.) Submit CPP using `paper.adoc` as spine. + +The first two items can land in this same PR cycle on request. The +rest are author-driven and the timing is yours. diff --git a/docs/echo-types/roadmap.md b/docs/echo-types/roadmap.md deleted file mode 100644 index 9a81d7e..0000000 --- a/docs/echo-types/roadmap.md +++ /dev/null @@ -1,431 +0,0 @@ -# Echo Types — Roadmap - -**Status:** planning document. Partitions work by dependency on the -two identified bottlenecks: - -For current cross-repo progress snapshots, see -`cross-repo-bridge-status.md`. - -- **Bottleneck B1 (RECAST 2026-05-20).** The remaining gap between - the closed Veblen/current-core route and the full intended - Buchholz order: the historically blocked shared-binder shapes in - `_<ᵇ_`. `wf-<ᵇ` is landed for the currently admitted core; the - shared-binder shapes (`<ᵇ⁺-ψα`, `<ᵇ⁺-+2`) now have a *budgeted* - WF carrier in `Ordinal.Buchholz.OrderExtendedBudget.wf-<ᵇ⁺ᵇ` - (mirroring the existing `wf-<ᵇʳᶠᵇ` for the recursive surface). - **The unbudgeted promotion is structurally impossible** for the - current `_<ᵇ_` — see `buchholz-rank-obstruction.adoc`. The - Echidna-SA-recommended rank-into-Brouwer route fails on the - ordinally-unsound `<ᵇ-+Ω` constructor; all four alternative - routes (direct mutual structural recursion, tower-stratification, - lex measure into ℕ, inverse-image into the budgeted relation) are - also walled. Recovering unbudgeted WF requires either restricting - `_<ᵇ_` to a `WellFormed` subset (2–3 weeks of constructor-by- - constructor rework) or providing a non-additive denotational - measure (essentially solving Buchholz WF "from the model up"). - The "B1" framing is therefore now: *accept the budgeted forms as - canonical*, or *commit to one of the two substantial paths*. -- **Bottleneck B2.** Tool-scope limitations on adjacent repos - (`maa-framework/absolute-zero`, `januskey`, - `tropical-resource-typing`). Blocks end-to-end bridge audits. - -Paths marked **[unblocked]** can proceed today. Paths marked -**[gated on B1]** or **[gated on B2]** cannot. - ---- - -## Theory work — no proof assistant needed - -- **[landed]** Axis 2 (approximate echoes): formal definition, - distinguishing test, examples, and composition theorem all in - `taxonomy.md` §2 (lines 38–64). `EchoApprox.agda` ships - `EchoR ε f y`, three headline lemmas (`echo-approx-intro`, - `echo-approx-relax`, `echo-approx-compose`). Pinned in - `Smoke.agda`. Compiler-analysis widening application worked in - `applications-compiler-analysis.adoc` example 2. -- **[landed]** Axis 8 (information-theoretic vs computational - access): promoted from the candidates list to a numbered axis. - Every candidate refinement is now mechanised. Decidability- - respecting: `proofs/agda/EchoDecidable.agda`. Cost-indexed (over - an abstract `CostAlgebra`): `EchoCost.agda` + `EchoCostInstance.agda` - (PR #85). Graded access modality: `EchoAccess.agda` (PRs #68 + - #75). Witness-search abstract machine: `EchoSearch.agda` + - `EchoSearchInstance.agda` (PR #80). See `taxonomy.md` §8. -- **[landed]** Negative / co-echoes: `AntiEcho f y := Σ A (λ x → f x ≢ y)` - shipped as `proofs/agda/AntiEcho.agda` (PR #69) with - `antiecho-{intro, disjoint, map-over}`, plus per-element - classification `antiecho-partition-dec` (PR #90, closes - `coecho.md` §5 obligation 5). Distinct from `EchoFiberTriangulation.CoEcho` - (which is the trivial opposite-orientation fibre); see naming - rationale in `AntiEcho.agda`'s preamble. The tropical decomposition - `TropEcho y ↔ Echo score y × (∀ z → y ≤ score z)` lands at the - concrete ℕ-scored level in `AntiEchoTropical.agda` (PR #72) and at - an abstract `OrderedCodomain` interface in `AntiEchoTropicalGeneric.agda` - (PR #91, closes `coecho.md` §5 obligation 6). -- **[ruled out — see docs/echo-types/decisions/no-2-cat.adoc]** - 2-categorical shape. Every would-be 2-cell in the landed code - is `refl` or forced trivial by propositionality (`≤g-prop`, - `⊑-prop`, `Echo-comp-iso` round-trips, pentagon projections, - `SliceHom`↔cone, `bridge-natural`); see - `decisions/no-2-cat.adoc` for the full verdict. -- **[landed — see docs/echo-types/decisions/presentation-dependence.adoc]** - Presentation-dependence sub-theory: examples 5, 9, 10 cluster - here. Common pattern is Σ-over-presentation-parameter `R`; cluster - instantiates the existing Axis 4 without motivating a new axis. - Verdict: meta-pattern only — no `EchoPresentation.agda` module - needed; landed `EchoIndexed`/`EchoChoreo`/`EchoEpistemic` already - carry the per-decoration composition recipe. Axis 4's - "canonical-form operator" open question sharpens but stays open. - See `decisions/presentation-dependence.adoc` for the full verdict. -- **[refreshed — see decisions/gate1-adjacency-refresh.adoc]** - Gate 1 adjacency refresh: the five existing adjacency notes - predate the taxonomy. Cross-check each against the current axes - and flag any neighbour whose identity claim should be - re-evaluated. Verdict: 5/5 REFINED, 0 RE-EVALUATE; every - distinctness claim survives, all five benefit from being - re-stated in terms of the now-numbered axes (axis 8 sharpens - four of five). No content rewrites scheduled; coherence - follow-ups listed in the closure note. - ---- - -## Formalisation work — Agda, no bottleneck - -- **[landed]** `Echo-comp-iso` in `Echo.agda`: the accumulation - isomorphism `Echo(g ∘ f) y ≃ Σ B (λ b → Echo(f) b × (g b ≡ y))`. - Shipped as `Echo-comp-iso-{to, from, from-to, to-from}`; both - round-trips are definitional. See `composition.md` §1. -- **[landed]** `cancel-iso-to` / `cancel-iso-from` / - `cancel-iso-from-to` / `cancel-iso-to-from` in `Echo.agda`, - packaged as `Echo.cancel-iso : ... → Echo (g ∘ f) y ↔ Echo f (s y)` - via stdlib's `Function.Bundles._↔_` and `mk↔ₛ′`. Both round-trips - parameterised by their respective triangle identities (one - triangle implies the other in HoTT but the adjustment is - non-trivial path algebra, so both stay explicit). Companion - `Echo.Echo-comp-iso` packages the unconditional accumulation iso - the same way. See `composition.md` §3 + §4. -- **[landed]** Pentagon coherence for three-fold composition. - Projection lemmas `Echo-comp-iso-pent-B` and `Echo-comp-iso-pent-echo` - both `refl` in `Echo.agda`. The full Σ-associativity iso between the - two nested Σ-shapes (outer-first carries an extra intermediate - `c : C` with `g b ≡ c`; inner-first absorbs it) now ships as - `Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}`. The forward - map collapses `c` against `g b ≡ c` and transports the outer - h-equation; the backward map sets `c := g b` with `refl`. Both - round-trips reduce definitionally once the `g b ≡ c` has been pinned, - so this is a strict iso (no transport coherence required) and lives - inside `--safe --without-K`. All four pinned in `Smoke.agda`. -- **[landed]** Budgeted recursive-surface WF on the ordinal track. - `Ordinal/Buchholz/RecursiveSurfaceBudget.agda` ships - `BudgetedBT = ℕ × BT`, the budgeted relation `_<ᵇʳᶠᵇ_` with its - `spend` constructor, `wf-<ᵇʳᶠᵇ : WellFounded _<ᵇʳᶠᵇ_` (via - subrelation on ℕ), and `<ᵇʳᶠᵇ⇒lifted` transporting each budgeted - step into the iterated-wrapper tower (`IteratedExtendedOrder`). -- **[landed, 2026-05-20]** Budgeted shared-binder WF for the - K-restricted extended order. - `Ordinal/Buchholz/OrderExtendedBudget.agda` ships - `BudgetedBT⁺ = ℕ × BT`, the budgeted relation `_<ᵇ⁺ᵇ_` with its - `spend` constructor, and `wf-<ᵇ⁺ᵇ : WellFounded _<ᵇ⁺ᵇ_`. Mirrors - the recursive-surface pattern but for the depth-1 shared-binder - cases (`<ᵇ⁺-ψα`, `<ᵇ⁺-+2`). -- **[closed-impossible, 2026-05-20]** The unbudgeted global - theorem — eliminate the explicit ℕ budget from `wf-<ᵇʳᶠᵇ` to get - `WellFounded _<ᵇʳᶠ_`, or analogously for `_<ᵇ⁺_` — is - structurally impossible for the current `_<ᵇ_`. The - Echidna-SA-recommended rank-into-Brouwer route in - `RankBrouwer.agda` was refuted by a worked counterexample on - `<ᵇ-+Ω`. All four alternative routes also walled. See - `buchholz-rank-obstruction.adoc` for the full analysis and the - two substantial-work paths that could re-open the question - (WF-restricted `_<ᵇ_` or non-additive denotational measure). -- **[landed]** `EchoApprox.agda`: new module for ε-indexed echoes - over a metric codomain. First-class taxonomy axis 2 artifact. - Ships `EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε)` parametric over - a `Tolerance` monoid and a `PseudoMetric`, with three headline - lemmas: `echo-approx-intro` (exact ⇒ zero-ε), `echo-approx-relax` - (monotone in ε), and `echo-approx-compose` (additive composition - under a non-expansive outer leg, realising the taxonomy §2 - conjecture). Wired into `All.agda` and `Smoke.agda`. -- **[landed]** Composition rung first slice (Axis 2): the §Q3 - retract-shape. `EchoApprox.agda` now also ships - `echo-strict→approx` (general strict ⇒ zero-tolerance, generalises - `echo-approx-intro` from own-fibre to arbitrary `y` via the - codomain equation), `echo-approx-comp-sound` (RHS-Σ → LHS via - `echo-approx-compose`), `echo-approx-comp-retract-to` - (canonical-split LHS → RHS-Σ section, picking `b := f x`, - `ε₁ := zero`, `ε₂ := ε`), and `echo-approx-comp-retract-A` (the - A-component round-trip `proj₁ ∘ sound ∘ retract-to ≡ proj₁`, - proved by `refl`). The retraction direction on the A-witness holds - definitionally as the design note (§5) predicts. The B-component - and tolerance-budget round-trips are deferred to a subsequent - rung — they need a `+`-left-identity axiom on `Tolerance` - (`zero + ε ≡ ε`) which the current record does not supply. - §7 obligations 7 (separated zero-collapse) and 8 (axis-1 shadow - agreement) likewise deferred. -- **[landed]** Per-decoration composition lemmas across the - five-decoration family — **sweep complete** (2026-04-28): - `EchoGraded.degrade-compose`, `EchoLinear.degradeMode-compose`, - `EchoIndexed.map-role-indexed-comp`, - `EchoChoreo.applyChoreo-{comp, compose, via-join}` along the - choreographic-reachability order `_⊑c_`, and - `EchoEpistemic.knowledge-monotone-{comp, id}`. Each follows the - same recipe (decoration order → propositionality → join → - factoring-free compose → via-join restatement). All headlines - pinned in `Smoke.agda`. -- **[landed]** Honest finite-domain Landauer/Bennett bounds - (2026-04-28). `EchoFiberCount.agda` provides the actual fiber - count `FiberSize-fin : (Fin n → B) → B → DecEq → ℕ` plus four - headline lemmas (`FiberSize-fin-id-zero`, `FiberSize-fin-const`, - bidirectional `FiberSize-fin ≡ 0 ⟺ ¬ Echo`). - `EchoThermodynamics.agda` rewritten against - `Data.Nat.Logarithm.⌊log₂_⌋`: `bennett-reversible`, - `bennett-reversible-id-zero`, `landauer-collapse`. Replaces the - earlier `FiberSize = 1` hardcode that rendered the prior - CNO-zero-energy claims vacuous. Infinite-domain - (`ProgramState = ℕ → ℕ`) case explicitly out of scope. - `docs/ECHO-CNO-BRIDGE.adoc` swept to remove four overclaim sites. -- **[partial]** Buchholz extended order `_<ᵇ⁺_` (2026-04-28, - updated 2026-05-20). `Ordinal.Buchholz.OrderExtended.agda` adds - the two K-restricted shared-binder lex constructors (`<ᵇ⁺-ψα`, - `<ᵇ⁺-+2`) on top of the K-free core `_<ᵇ_`, with explicit - equality witnesses to keep implicits pairwise distinct. - `<ᵇ⁺-irrefl` and `<ᵇ⁺-trans` proved (mixed cases via four - `extend-{lhs, rhs}` helpers). - Well-foundedness in **budgeted form** for `_<ᵇ⁺_` landed - 2026-05-20: `Ordinal.Buchholz.OrderExtendedBudget` ships - `wf-<ᵇ⁺ᵇ` (mirrors `wf-<ᵇʳᶠᵇ`). The **unbudgeted** form is - CLOSED-IMPOSSIBLE for the current `_<ᵇ_` — see - `docs/echo-types/buchholz-rank-obstruction.adoc` for the - structural impossibility (`<ᵇ-+Ω` ordinal unsoundness) - refuting all five plausible routes. The historical "Route A / - Route B" framing in `buchholz-extended-wf.md` is now - superseded. -- **[unblocked]** Add example-library Agda files matching - `examples.md`: start with examples 1–4 already in-suite, then - example 7 (ordinal collapse is in `EchoOrdinal`); examples 5, 6, - 9, 10 are new Agda candidates. - ---- - -## Example work — mostly writing, some coding - -- **[unblocked]** Complete worked numeric example (ex. 6) with the - approximate-echo shape, once the definition lands. -- **[landed]** Parser residue example (ex. 9) — `EchoExampleParser.agda` - (PR #83): balanced parens, Boolean shadow `parses : List Token → - Bool` non-injective on `(())` vs `()()`, echo retains the token - stream. -- **[landed]** Abstract-interpretation example (ex. 10) — - `EchoExampleAbsInt.agda` (PR #82): Sign lattice `{neg, zero, pos}` - over a hand-rolled five-element integer carrier; collapses - `{m1, m2} ↦ neg`, `{z} ↦ zero`, `{p1, p2} ↦ pos`. -- **[landed]** Database provenance example (ex. 5) — - `EchoExampleProvenance.agda` (PR #81): K-provenance semiring, - distinct Bool-provenance rows projecting to the same payload. -- **[unblocked]** Extend `EchoExamples.agda` with further canonical - entries (post-#81/#82/#83 the cluster has good coverage; only - ex. 6 remains). - ---- - -## Application work — no proof assistant needed for first-pass prose - -- **[unblocked]** **Compiler-analysis residue.** Write up how Echo - Types names the residue produced by abstract interpretation, - register allocation, SSA conversion, and constant folding. - Cross-reference existing literature (e.g. Cousot/Cousot for AI, - various works on "explainable compilation"). -- **[unblocked]** **Database provenance.** Tie to K-provenance and - the `Bag`-semiring tradition. The adjacency note already exists; - extend into a discipline-specific Echo Types chapter. -- **[unblocked]** **Verification / refinement.** Relate Echo Types - to refinement types and to proof-carrying code. The intensional - witness is a "refinement that survives erasure". -- **[unblocked]** **ML interpretability / AI abstraction.** The most - speculative. Echo Types could name the residue of information- - losing layers in neural networks (pooling, attention heads, - embedding projections). Write as a *speculative* chapter with - explicit open questions; do not overclaim. -- **[unblocked]** **Concurrency / choreography.** `EchoChoreo.agda` - already models role-observation echoes. Extend to a distributed- - systems residue discipline. - ---- - -## Proof-assistant-dependent work — gated - -- **[partial]** Internalize the missing shared-binder shapes as - actual constructors of the Buchholz order. **Done** for the - irrefl + trans layer in `Ordinal.Buchholz.OrderExtended._<ᵇ⁺_` - with `<ᵇ⁺-ψα` and `<ᵇ⁺-+2` (2026-04-28). Well-foundedness for - the enlarged order is open — see the gated entry below. -- **[gated on `_<ᵇ⁺_` WF]** Re-close well-foundedness for the - enlarged order. Two design routes documented in - `docs/echo-types/buchholz-extended-wf.md`: single-mutual block - with widened bundle (Route A — attempted, blocked on Agda - termination) or rank-embedding into Brouwer ordinals (Route B - — recommended next-attempt; scaffolded by - `Ordinal.Buchholz.RankBrouwer.agda` from the parallel session). -- **[gated on B1]** Ordinal semantics of BT terms: denotation - `BT → Ordinal` preserving order. Requires a formal `Ordinal` type - as a prerequisite, which is itself downstream of WF. -- **[partial]** Landauer / Shannon rigorous bridge. **Done** for - the finite-domain Landauer/Bennett shape in - `EchoThermodynamics.agda` (rewritten 2026-04-28 against - `EchoFiberCount.FiberSize-fin` and `Data.Nat.Logarithm.⌊log₂_⌋`). - Open: infinite-domain `ProgramState = ℕ → ℕ` extension (needs a - capacity / measure / equivalence-class-quotient framework); - Shannon-entropy formalisation (no probability-monad in stdlib v2 - at the level needed); physical heat-dissipation realisation - (the bound is information-theoretic, not a physical claim). -- **[landed]** CNO content-bridge across echo-types and - `absolute-zero`. `proofs/agda/EchoCNOBridge.agda` imports `IsCNO` - directly from `absolute-zero/proofs/agda/CNO.agda`; both files - build clean under `--safe --without-K`. Cross-prover (Coq/Lean4) - theorem-statement alignment is now documented in - `docs/echo-types/cross-repo-bridge-status.md` (correspondence - table + structural blockers around the relational/functional - `eval` split and the 3 Coq axioms forbidden by `--safe`). -- **[partial]** Janus reversible-file-operations bridge against - `januskey`'s actual API. Agda side is still a 4-variant name-bridge; - decision recorded to structural-mirror the canonical 8-variant - Idris2 `OpKind` (`januskey/src/abi/Types.idr`). Content-bridge - remains gated on `januskey/PROOF-NEEDS.md`. -- **[partial]** Tropical-resource-typing alignment. Adjacent repo - audited 2026-05-20 (remote `hyperpolymath/tropical-resource-typing` - active; 9 `.thy` + `TropicalSessionTypes.lean`). First alignable - theorem pair identified: Agda `⊕-idem` ↔ Isabelle `trop_add_idem` - ↔ Lean `add_comm_trop`+`add_assoc_trop`. Alignment is - citation-level (no Agda↔Isabelle/Lean import surface). -- **[gated on B2]** `maa-framework` integration. Out of scope for - the current tooling; needs scope expansion or file export. - ---- - -## Suggested immediate ordering - -This is my honest suggested ordering, conservative about what's -tractable today: - -1. ~~**Theory: axis 2 formal definition**~~ — **landed**. - Formal definition + composition theorem in `taxonomy.md` §2; - `EchoApprox.agda` artifact with three headline lemmas; example 10 - (abstract interpretation widening) worked in - `applications-compiler-analysis.adoc`. -2. ~~**Agda: `Echo-comp-iso` + cancellation**~~ — **fully landed**. - Accumulation iso (`Echo-comp-iso`), both cancellation maps, plus - **full cancellation iso with round-trips** (`cancel-iso-{to, from, - from-to, to-from}` + packaging `Echo.cancel-iso : ... ↔ ...` - parameterised by `s-left`, `s-right`, and both triangle - identities) live in `Echo.agda`. All five pinned in `Smoke.agda`. -3. ~~**Agda: pentagon coherence for `Echo-comp-iso`**~~ — - **fully landed**. Projection pentagon (`Echo-comp-iso-pent-{B, - echo}`) and the full Σ-associativity iso between the two nested - Σ-shapes (`Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}` + - equivalence-record packaging `Echo-comp-pent-Σ-assoc : ... ↔ ...`) - are both in `Echo.agda`. All pinned in `Smoke.agda`. -4. **Agda: unbudgeted `_<ᵇʳᶠ_` WF on the ordinal track** — - **VERDICT NARROWED 2026-05-20 evening.** The "closed impossible" - framing held for *unrestricted* `_<ᵇ_`. Under the WfCNF - restriction `_<ᵇ⁻_` together with a limit-shaped *ω-power* rank - (`Ordinal.Brouwer.OmegaPow` + `Ordinal.Buchholz.RankPow`), the - path-1 closure is now **10 of 13 constructors** via - relation-agnostic rank-mono primitives (PR #87). The umbrella - theorem `rank-pow-mono-<ᵇ⁰ : x <ᵇ⁰ y → rank-pow x <′ rank-pow y` - lives in `Ordinal.Buchholz.RankMonoUmbrella`; consumers - (whether `_<ᵇ⁻_` or `_<ᵇʳᶠ_` based) construct `_<ᵇ⁰_` - derivations and apply the umbrella. - - **3 cases remain open** under documented structural blockers - (see `buchholz-rank-obstruction.adoc` for the per-constructor - verdict table): - * `<ᵇ-ψα`, `<ᵇ-ψΩ≤` — ψ-admissibility predicate carrier landed - (`Ordinal.Buchholz.WellFormedAdmissible.WfAdm`); rank-refinement - for the discharge is a follow-on slice with a `<ᵇ-+ψ` - cross-case to manage. - * `<ᵇ-+1` joint-bplus — `rank-pow (bplus z₁ z₂)` is not additive - principal in general. Needs a coarser dominator (e.g., - `leading-Ω-index : BT → OmegaIndex`). - - The keystone is the **additive-principal lemma at ω^(suc n)** - (`Ordinal.Brouwer.OmegaPow.additive-principal`). Budgeted forms - (`_<ᵇʳᶠᵇ_`, `_<ᵇ⁺ᵇ_`) remain the canonical well-founded - carriers until the 3-case gap closes. -5. **Gate 1 adjacency refresh against the new taxonomy** — 1 day. - Cheap coherence pass on existing docs. Cross-check each of the - 13 notes in `docs/adjacency/` against the 8 axes in `taxonomy.md` - and flag any neighbour whose identity claim should be re-evaluated. -6. **Theory: pick one axis-8 refinement and formalise it** — 1–2 - days. Four candidates in `taxonomy.md` §8 (cost-indexed echo, - graded access modality, decidability-respecting echo, witness- - search abstract machine). Choosing commits the repo to one - formal handle on computational vs information-theoretic access. -7. ~~**Agda: `EchoApprox.agda`**~~ — **landed**. - First artifact of axis 2. Ships `EchoR ε f y = Σ A (λ x → dist - (f x) y ≤ ε)` parametric over a `Tolerance` monoid and a - `PseudoMetric`, with three headline lemmas: `echo-approx-intro` - (exact ⇒ zero-ε), `echo-approx-relax` (monotone in ε), - `echo-approx-compose` (additive composition under a non-expansive - outer leg). Wired into `All.agda` + pinned in `Smoke.agda`. -8. ~~**Applications chapter: compiler-analysis residue**~~ — - **first draft landed 2026-05-20**. - `docs/echo-types/applications-compiler-analysis.adoc` with two - worked examples (parser error recovery on axis 4; - abstract-interpretation widening on axis 2), all four axis-8 - refinements applied to source-mapping, pipeline composition, - scope demarcation, and cross-references to every relevant - adjacency note. Follow-up: full Agda exhibits for each example - (tracked as `[unblocked]` example-library items below). -9. ~~**Per-decoration composition lemmas**~~ — **sweep complete** - (2026-04-28). All five decorations landed: - `EchoGraded.degrade-compose`, `EchoLinear.degradeMode-compose`, - `EchoIndexed.map-role-indexed-comp`, - `EchoChoreo.applyChoreo-{comp, compose, via-join}` along the - choreographic-reachability order `_⊑c_`, and - `EchoEpistemic.knowledge-monotone-{comp, id}`. Each follows the - same recipe (decoration order → propositionality → join → - factoring-free compose → via-join restatement). All headlines - pinned in `Smoke.agda`. - -The remaining open work in this list is **steps 1, 5, 6, 8**. Steps 1 -and 5–6 are ~3–4 days of honest work that require nothing from proof -assistants, external repos, or the blocked Buchholz path. Step 5 is -the natural next coherence pass; steps 6 and 8 extend into Agda or -prose but depend only on infrastructure we already have in-suite. - -Everything **[gated]** waits for its unblocker. The pack above gives -3–4 weeks of disciplined parallel work without touching the remaining -full-order Buchholz gap. - ---- - -## What this roadmap deliberately does not include - -- No week-by-week date estimates beyond the rough "days" above. - These are order-of-magnitude guides, not commitments. -- No claim about which application area will yield the largest - payoff — ML interpretability, compiler analysis, and database - provenance are all plausible; that decision should come from the - consumer, not the theory. -- No tie to any release tag. `v0.2.0` should be decided on the basis - of actual landed content, not on this roadmap. -- No gating on `docs/buchholz-plan.adoc`'s own milestones (E4, E5, - etc.) — those are a parallel workstream that can advance or stall - without affecting the Echo Types theory development here. - ---- - -## Revision policy for this document - -This roadmap should be updated when: - -- A **[gated]** item becomes unblocked (e.g. Agda upgrade, repo - access granted). -- A new axis is added to `taxonomy.md`. -- An example in `examples.md` gets promoted to formalised Agda. -- The composition laws in `composition.md` get confirmed or refuted. - -Keep the revision history in-file (append-only), and annotate each -update with the trigger. The roadmap is a living document; the -stable content lives in `overview.md`, `taxonomy.md`, and -`composition.md`. diff --git a/docs/echo-types/sigma-distinctness-map.adoc b/docs/echo-types/sigma-distinctness-map.adoc new file mode 100644 index 0000000..4bd4b7f --- /dev/null +++ b/docs/echo-types/sigma-distinctness-map.adoc @@ -0,0 +1,189 @@ += Echo vs. Sigma: distinctness evidence map +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +This file is the reviewer-facing companion to +`core/skepticisms/is-this-just-sigma-types.md`. Its job is one thing: +collect, in one place, the in-repo evidence that `Echo f y` is not +"renamed `Σ A (λ x → f x ≡ y)`" and to organise that evidence under the +five demands a sceptic typically makes. + +[IMPORTANT] +==== +Statements below stay inside the *narrowed* claims of +`docs/retractions.adoc` R-2026-05-18. In particular: no "full +categorical universal property" (the pullback is funext-relative and +pointwise), no "graded comonad" (the loss structure is a thin-poset +reindexing modality), no "model-independence" (the abstract model +interface is carrier-parametricity over a fixed grade poset). +==== + +toc::[] + +== Five demands, five answers + +Each subsection states the demand, names the in-tree artefact(s) that +answer it, and notes any narrowing relative to the stronger statement a +sceptic might want. + +=== Demand 1 — Irreversibility as a theorem family + +[cols="1,3", options="header"] +|=== +| Claim | Echo proves that no section of the loss-map exists, across multiple decoration layers. Raw `Σ` gives `proj₁` trivially. + +| Agda | +`EchoCharacteristic.no-section-collapse`, +`EchoCharacteristic.no-section-visible`, +`EchoResidue.no-section-collapse-to-residue`, +`EchoLinear.no-section-weaken`, +`EchoOrdinal.no-section-ordinal-collapse`, +`EchoEpistemicResidue.no-section-to-epistemic`. All pinned in +`proofs/agda/Smoke.agda`. + +| Prose | `docs/characteristic.adoc`, +`docs/proof-obligations.md` §"No-section" entries, +`readme.adoc` §"Characteristic family". + +| Narrowing | None. The family lemmas are clean negative results under +`--safe --without-K`. +|=== + +=== Demand 2 — Algebra of loss (down-admissible, up-blocked) + +[cols="1,3", options="header"] +|=== +| Claim | The fibre carries a loss-grade lattice with a monotone +reindexing modality. Down-step is admissible; up-step is provably not. + +| Down-step (Agda) | +`EchoGraded.degrade-compose` and `EchoGraded.degrade-via-join` are the +per-decoration composition laws. The same recipe lands at +`EchoLinear.degradeMode-compose`, `EchoChoreo.applyChoreo-compose`, +`EchoAccess` (graded access), `EchoCost` (cost-indexed), +`EchoSearch` (witness-search). + +| Up-step blocked (Agda) | `EchoLinear.no-section-weaken` (= +`EchoResidue.no-section-collapse-to-residue`). + +| Separating model | `EchoSeparating.sep-degrade-compose-fails` — +removing `≤g-prop` (the only load-bearing hypothesis) breaks +`degrade-compose` at a checked `true ≢ false`. This locates the +reduction. + +| Prose | `docs/characteristic.adoc` (Gate 2 audit), N1–N4 nominees. + +| Narrowing | Per R-2026-05-18, this is a *thin-poset reindexing +modality*, not a graded comonad. No nested `D_r D_s` is formed. +|=== + +=== Demand 3 — Categorical identity and bridges + +[cols="1,3", options="header"] +|=== +| Claim | Echo is a recognisable categorical object (the homotopy +fibre) and other "loss-tracking" frameworks bridge into it. + +| Identity (Agda) | `EchoFiberBridge.echo↔fib` — definitional fibre +identity with `refl` round-trips (Pillar A, landed 2026-05-17). + +| Pullback (Agda) | `EchoPullback.echo-pullback-univ` — pullback of +`f` along `y : ⊤ → B` with *pointwise, funext-relative* mediator +property. See retraction note at the head of the module. + +| Bridges (Agda) | `EchoJanusBridge.agda` (reversible debugger), +`EchoTropical.agda` + `AntiEchoTropical.agda` (tropical / argmin), +`EchoCNOBridge.agda`, `DyadicEchoBridge.agda`, +`EchoFiberCount.agda` + `EchoThermodynamicsFinite.agda` (finite-fibre +Landauer / Bennett). + +| Prose | `docs/echo-types/establishment-plan.adoc` §"Pillar A", +`docs/adjacency/`. + +| Narrowing | The bridges are independent witnesses, not a single +"every loss-tracker maps uniquely into Echo" theorem. Such a uniqueness +result would require either funext or an axiom and is therefore *not* +in scope under the no-postulate invariant. +|=== + +=== Demand 4 — Abstraction barrier (consumer-side) + +[cols="1,3", options="header"] +|=== +| Claim | The Echo interface at the affine mode forbids the consumer +from distinguishing two preimages of the same output. Raw `Σ` does +not, via `proj₁`. + +| In-tree precursor (Agda) | `EchoLinear.affine-canonical`, +`EchoLinear.affine-all-equal` — the affine residue carrier is +contractible. + +| Planned (Agda) | `proofs/agda/EchoAbstractionBarrier.agda` — Track B +in the work plan. Headline lemmas: +`affine-consumer-cannot-distinguish` (positive) and +`sigma-distinguishes` (the raw-`Σ` counter-program, as a checked +exhibit of what the barrier blocks). + +| Model-side counterpart (Agda) | `EchoRelModel.GradedLossModel` + +generic `GCLaws` — carrier-parametricity over a fixed grade poset +(Pillar D, narrowed per R-2026-05-18). + +| Narrowing | The planned consumer-side theorem is a *free theorem at +the headline affine instance*, not full Reynolds parametricity (Agda +has no parametricity primitive; a fully general statement would need +an axiom). +|=== + +=== Demand 5 — Canonical examples + +[cols="1,3", options="header"] +|=== +| Claim | Echo is the right explanatory unit on real artefacts, not +just decorative wrapping. + +| Agda | +`EchoExampleParser` (`(())` vs `()()` at `parses ≡ true`), +`EchoExampleProvenance` (collapsed Bool-provenance), +`EchoExampleAbsInt` (`{p1,p2}` ↦ `pos`), +`EchoExampleSignAnalysis`, `EchoExampleTruncation`, +`EchoFiberCount` + `EchoThermodynamics*` (finite-fibre Landauer), +`EchoEpistemicResidue` (observation discipline). + +| Planned matched-negative (Agda) | +`proofs/agda/examples/EchoVsSigma.agda` — Track C in the work plan. +Pairs each headline example with the small raw-`Σ` counter-program +that would let the corresponding bug through. + +| Prose | `docs/echo-types/examples.md`, +`roadmap-gates.adoc` Gate 3. + +| Narrowing | Until Track C lands, the "raw `Σ` would leak" half is +prose, not a checked artefact. +|=== + +== What this file does NOT claim + +The five sections above are an *evidence map*, not a re-litigation of +the gate decisions. In particular: + +* This file does not claim Gate 1, Gate 2, or Gate 3 is passed. That + is the job of `roadmap-gates.adoc`, `docs/characteristic.adoc`, and + the example modules themselves. +* This file does not claim the planned Track B / Track C work is + landed. Where a row mentions "Planned (Agda)", the artefact does not + yet exist on `main`; check `git log` before relying on it. +* This file does not introduce new theorems. It cross-references + artefacts that already live elsewhere in the tree. + +== See also + +* `core/skepticisms/is-this-just-sigma-types.md` — internal devil's + advocate ledger this file is the AsciiDoc companion to. +* `core/skepticisms/is-this-just-fibers.md` — adjacent skepticism. +* `core/skepticisms/what-is-actually-new.md` — the broader question. +* `docs/retractions.adoc` — the R-2026-05-18 narrowing that governs + the prose discipline here. diff --git a/docs/echo-types/tropical-correspondence.md b/docs/echo-types/tropical-correspondence.md index 472235f..664a1b4 100644 --- a/docs/echo-types/tropical-correspondence.md +++ b/docs/echo-types/tropical-correspondence.md @@ -84,8 +84,8 @@ not constitute a unified verification artefact. It closes the grading* (`grade : Session → Tropical` in Lean), which is the symmetric Agda-exclusive direction. - **Long-game alignment target.** When the echo-types ordinal track - reaches Bachmann–Howard (ψ₀(Ω_ω); see `docs/echo-types/roadmap.md` - and `buchholz-plan.adoc`), the adjacent repo's + reaches Bachmann–Howard (ψ₀(Ω_ω); see `roadmap.adoc` §Lane 3 and + `docs/buchholz-plan.adoc`), the adjacent repo's `Tropical_Ordinal_Bridge.thy` becomes the natural cross-repo alignment target (Agda Buchholz BT ↔ Isabelle `tropO` carrier). This target is **firewalled** until the ordinal track lands the diff --git a/docs/echo-types/types-abstract.adoc b/docs/echo-types/types-abstract.adoc index 820073e..6674bf7 100644 --- a/docs/echo-types/types-abstract.adoc +++ b/docs/echo-types/types-abstract.adoc @@ -185,3 +185,14 @@ Submission logistics (venue deadline, TYPES-template formatting, author metadata, Zenodo DOI, arXiv cross-post) remain offline and author-driven; they are downstream of, not a substitute for, the re-review. + +NOTE: *In-repo Pillar E status (2026-05-26).* The full `paper.adoc` +has cleared all `[EXPAND]` tags except the ordinal consumer-evidence +appendix (gated on Bachmann–Howard per `roadmap.adoc` §Lane 3). Any +further re-review of this abstract should treat the full paper as +the canonical reference for narrowed claims; this abstract is the +2-page condensation of it. The single-page reviewer companion +`docs/echo-types/comparators.adoc` carries the axis-by-axis +comparison against Granule, QTT, choreographic types, and Linear +Haskell. See `roadmap.adoc` §"Pillar status" for the lane-level +view. diff --git a/docs/theorem-index.md b/docs/theorem-index.md index 2fc369b..7fc5cf1 100644 --- a/docs/theorem-index.md +++ b/docs/theorem-index.md @@ -22,4 +22,49 @@ This document maps foundational theorems and characteristic results to their exa | `visible-constraint` | PROVED | `Echo/Characteristic.agda` | Projection-style loss retains a provable constraint on the source. | | `no-section-collapse-to-residue` | PROVED | `Echo/Residue.agda` | Weakening an echo to a residue discards irrecoverable information. | +## Degrade-law family (aggregate) + +The "degrade" results are the per-decoration composition + join laws +demonstrating that loss has *direction* (down-step admissible, up-step +not — the no-section family below is the matching diagonal). All sites +PROVED and pinned in `proofs/agda/Smoke.agda`. + +| Site | Module Path | +|------|-------------| +| `degrade-comp`, `degrade-compose`, `degrade-via-join` | `EchoGraded.agda` | +| `degradeMode-comp`, `degradeMode-compose`, `degradeMode-via-join` | `EchoLinear.agda` | +| `applyChoreo-compose` | `EchoChoreo.agda` | +| `degrade-access-comp`, `degrade-access-compose`, `degrade-access-via-join` | `EchoAccess.agda` | +| `degrade-cost-compose` (and family) | `EchoCost.agda` | +| `degrade-search-compose` (and family) | `EchoSearch.agda` | + +Separating model (locates the reduction): `EchoSeparating.sep-degrade-compose-fails` +exhibits a checked `true ≢ false` failure when the single load-bearing +hypothesis `≤g-prop` is removed. + +See `core/skepticisms/is-this-just-sigma-types.md` §2 and +`docs/echo-types/sigma-distinctness-map.adoc` §"Demand 2" for the +sceptic-facing framing. Honest framing per +`docs/retractions.adoc` R-2026-05-18: this is a *thin-poset reindexing +modality*, not a graded comonad. + +## No-section family (aggregate) + +The "no-section" results land at six sites across the decoration layers +and are collectively the answer to "raw `Σ` would give `proj₁` for +free". All are pinned in `proofs/agda/Smoke.agda`. + +| Site | Module Path | +|------|-------------| +| `no-section-collapse` | `EchoCharacteristic.agda` | +| `no-section-visible` | `EchoCharacteristic.agda` | +| `no-section-collapse-to-residue` | `EchoResidue.agda` | +| `no-section-weaken` | `EchoLinear.agda` | +| `no-section-ordinal-collapse` | `EchoOrdinal.agda` | +| `no-section-to-epistemic` | `EchoEpistemicResidue.agda` | + +See `core/skepticisms/is-this-just-sigma-types.md` §1 and +`docs/echo-types/sigma-distinctness-map.adoc` §"Demand 1" for the +sceptic-facing framing. + *Note: For experimental bridges or retracted claims, refer to the [Proof Obligation Ledger](proof-obligations.md) and [Bridge Status](bridge-status.md).* diff --git a/echo-types.agda-lib b/echo-types.agda-lib index 832d2b1..d29b5b2 100644 --- a/echo-types.agda-lib +++ b/echo-types.agda-lib @@ -1,3 +1,3 @@ name: echo-types -include: proofs/agda +include: proofs/agda . depend: standard-library absolute-zero diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 34f270f..ad1fa99 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -15,6 +15,7 @@ open import EchoExamples open import EchoChoreo open import EchoEpistemic open import EchoLinear +open import EchoAbstractionBarrier open import EchoGraded open import EchoTropical open import AntiEchoTropical @@ -106,6 +107,9 @@ open import Ordinal.Buchholz.IteratedExtendedOrder open import Ordinal.Buchholz.RankBrouwer open import Ordinal.Buchholz.RankPartial open import Ordinal.Buchholz.RankPow +open import Ordinal.Buchholz.RankAdm +open import Ordinal.Buchholz.RankLex +open import Ordinal.Buchholz.HeadOmega open import Ordinal.Buchholz.RankMonoUmbrella open import Ordinal.Buchholz.RecursiveSurfaceOrder open import Ordinal.Buchholz.RecursiveSurfaceBudget diff --git a/proofs/agda/EchoAbstractionBarrier.agda b/proofs/agda/EchoAbstractionBarrier.agda new file mode 100644 index 0000000..ab6ba8b --- /dev/null +++ b/proofs/agda/EchoAbstractionBarrier.agda @@ -0,0 +1,101 @@ +{-# OPTIONS --safe --without-K #-} + +-- Track B of the "Echo ≠ Σ" identity-claim consolidation +-- (`roadmap.adoc` §Lane 2; sketch at +-- `core/skepticisms/is-this-just-sigma-types.md` §4 and +-- `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 4"). +-- +-- Scope guardrail (load-bearing — read before any prose claim about +-- this module). This module ships a CONSUMER-SIDE FREE THEOREM AT THE +-- HEADLINE AFFINE INSTANCE (`LEcho affine = EchoR ⊤ TrivialCert tt`). +-- It is NOT a general Reynolds-style parametricity result. Agda has +-- no parametricity primitive, and a statement quantifying over all +-- consumer types `X` and all echo carriers would require either an +-- axiom or a paper-only proof — both violate the no-postulate +-- invariant. The honest claim is: at the affine instance the residue +-- carrier is contractible (`EchoLinear.affine-canonical`), so every +-- consumer factors through that contraction and provably cannot +-- distinguish two known-distinct linear preimages. This is the +-- strongest statement available inside `--safe --without-K` without +-- funext. +-- +-- The module ships two theorems: +-- +-- `affine-consumer-cannot-distinguish` — POSITIVE: any +-- `g : LEcho affine → X` assigns the same value to the weakened +-- images of `echo-true` and `echo-false`. Direct corollary of +-- `affine-all-equal`. This is what the Echo interface GUARANTEES +-- that raw Σ does not. +-- +-- `sigma-distinguishes` — NEGATIVE: the raw Σ-projection `proj₁` +-- IS a consumer that distinguishes `echo-true` from `echo-false`. +-- Exhibiting this concrete counter-program makes the abstraction +-- barrier a checked artefact, not a wish: the Echo interface +-- refuses to export `proj₁` *exactly because* `sigma-distinguishes` +-- shows what would happen if it did. +-- +-- Together they say: hiding `proj₁` is a guarantee, not a convention. +-- +-- Honest framing notes: +-- * "Theorem 1" (consumer factorisation) from the original sketch was +-- dropped — its only statable form was `g (weaken e) ≡ g (weaken e)`, +-- degenerate. The real content lives in T2 + T3. +-- * The R-2026-05-18 narrowing applies. The graded structure is a +-- thin-poset reindexing modality, not a graded comonad. The +-- abstraction here is consumer-side at the affine instance, not +-- relational parametricity over the model. + +module EchoAbstractionBarrier where + +open import Echo using (Echo) +open import EchoCharacteristic + using (collapse; echo-true; echo-false; true≢false) +open import EchoLinear + using ( Mode; linear; affine; LEcho + ; weaken + ; affine-all-equal + ) + +open import Data.Bool.Base using (Bool) +open import Data.Product.Base using (Σ; _,_; proj₁) +open import Data.Unit.Base using (⊤; tt) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; cong) +open import Relation.Nullary using (¬_) +open import Level using (Level) + +private variable + ℓ : Level + +---------------------------------------------------------------------- +-- Theorem 2 (positive). Any consumer at the affine mode assigns the +-- same value to the weakened images of the two known-distinct linear +-- echoes. +-- +-- Direct corollary of `affine-all-equal` (`EchoLinear.agda:57-58`), +-- which is itself a corollary of `affine-canonical` — the affine +-- residue carrier is contractible. Hence `cong g` of the canonical +-- equality discharges the theorem in one line. + +affine-consumer-cannot-distinguish : + {X : Set ℓ} (g : LEcho affine → X) → + g (weaken echo-true) ≡ g (weaken echo-false) +affine-consumer-cannot-distinguish g = + cong g (affine-all-equal (weaken echo-true) (weaken echo-false)) + +---------------------------------------------------------------------- +-- Theorem 3 (negative companion — the raw-Σ counter-program). +-- `proj₁ : Echo collapse tt → Bool` is a consumer over the *raw* Σ +-- encoding that distinguishes the two linear echoes. Its existence is +-- what the Echo interface (at affine mode) is designed to prevent +-- exporting: T2 above guarantees no affine-mode consumer can match +-- this behaviour. +-- +-- The proof is `true≢false` directly, because `proj₁ echo-true` +-- reduces definitionally to `true` (via `echo-intro f x = x , refl`) +-- and `proj₁ echo-false` reduces to `false`. + +sigma-distinguishes : + Σ (Echo collapse tt → Bool) + (λ g → g echo-true ≢ g echo-false) +sigma-distinguishes = proj₁ , true≢false diff --git a/proofs/agda/EchoLinear.agda b/proofs/agda/EchoLinear.agda index ba7419d..1fcb6a5 100644 --- a/proofs/agda/EchoLinear.agda +++ b/proofs/agda/EchoLinear.agda @@ -63,7 +63,7 @@ affine-all-equal e1 e2 = trans (affine-canonical e1) (sym (affine-canonical e2)) -- linearity decoration: weakening between modes commutes with -- transitive composition of the mode-ordering. See -- docs/echo-types/composition.md §6 (decoration commuting) and --- docs/echo-types/roadmap.md "Per-decoration composition lemmas". +-- the degrade-law family aggregate row in docs/theorem-index.md. -- -- The mode ordering is the smallest reflexive-and-`linear≤affine` -- relation: linear ⊑ linear, linear ⊑ affine, affine ⊑ affine. The diff --git a/proofs/agda/EchoStabilityTests.agda b/proofs/agda/EchoStabilityTests.agda index 5b93966..2330193 100644 --- a/proofs/agda/EchoStabilityTests.agda +++ b/proofs/agda/EchoStabilityTests.agda @@ -126,4 +126,4 @@ bennett-corollary-check T = -- `FiberSize-fin` is finite-domain only; the infinite case -- needs measure-theoretic or capacity arguments and is open. -- * Shannon-entropy / mutual-information formalisations: not yet --- present in the repo. See `docs/echo-types/roadmap.md`. +-- present in the repo. See `roadmap.adoc` §"Deferred research track". diff --git a/proofs/agda/EchoThermodynamics.agda b/proofs/agda/EchoThermodynamics.agda index c454d11..2baf606 100644 --- a/proofs/agda/EchoThermodynamics.agda +++ b/proofs/agda/EchoThermodynamics.agda @@ -212,6 +212,7 @@ landauer-collapse f y _≟_ T h = -- extension of `FiberSize-fin` to a measure-theoretic count -- on infinite types, neither of which is available here; -- * that Shannon-entropy / informational arguments are --- formalised — they are not. See `docs/echo-types/roadmap.md` --- for the open thermodynamic items. +-- formalised — they are not. See `roadmap.adoc` §Lane 3 +-- (Ordinal track / deferred research) for the open +-- thermodynamic / information-theory items (not yet formalised). ---------------------------------------------------------------------- diff --git a/proofs/agda/Ordinal/Buchholz/HeadOmega.agda b/proofs/agda/Ordinal/Buchholz/HeadOmega.agda new file mode 100644 index 0000000..c35d7e9 --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/HeadOmega.agda @@ -0,0 +1,126 @@ +{-# OPTIONS --safe --without-K #-} + +-- Leading-Ω-index head function for Buchholz terms. First slice of the +-- planned closure of the last open per-constructor case `<ᵇ-+1` +-- joint-bplus in the Buchholz rank-monotonicity matrix +-- (`docs/echo-types/buchholz-rank-obstruction.adoc` §"What remains +-- open"). +-- +-- ## The closure plan (option A from RankPow.agda's preamble) +-- +-- The `<ᵇ-+1` joint-bplus case fails to discharge under `rank-pow` +-- alone because `rank-pow (bplus z₁ z₂)` is not additive principal in +-- general — `rank-pow y₁` (the left summand of the *target*) need not +-- close ⊕-sums of subterm ranks. The recommended unblock per the +-- obstruction doc is to dominate `rank-pow t` by an additive-principal +-- ω-power indexed by the leading Ω-marker of `t`, and then discharge +-- `<ᵇ-+1` via head-Ω inversion + additive-principal at head-Ω's +-- successor. +-- +-- This module lands the *head-Ω function itself* and its definitional +-- sanity lemmas. The downstream rank-mono / domination work is +-- deferred to follow-on slices, so that the head-Ω abstraction stands +-- on its own merits before any rank consumer pulls on it. +-- +-- ## What lands in this slice +-- +-- * `head-Ω : BT → OmegaIndex` — the leading-Ω-index head function. +-- Returns the leftmost-deepest Ω marker carried by the term, with +-- `fin 0` as the default for `bzero` (which has none — the future +-- rank-mono lemma will guard this case explicitly via a non-bzero +-- premise). +-- * `head-Ω-bzero`, `head-Ω-bOmega`, `head-Ω-bplus`, `head-Ω-bpsi` — +-- definitional sanity lemmas, one per `BT` constructor. These +-- lemmas are `refl` (the equations are the definition); they exist +-- so downstream code can rewrite by them without unfolding +-- `head-Ω` directly. +-- +-- ## What is deferred to follow-on slices +-- +-- * `head-Ω-mono` family (head-Ω respecting WfCNF / WfAdm structural +-- bounds). Needs the rank-domination lemma to be stated first. +-- * `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t → +-- rank-pow t <′ ω-rank-pow-succ (head-Ω t)` (the load-bearing +-- domination lemma). Needs an `ω-rank-pow-succ : OmegaIndex → +-- Ord` (one option: `ω-rank-pow-succ (fin n) = ω^(suc (suc n))`, +-- `ω-rank-pow-succ ω = olim (λ n → ω^(suc (suc n)))`) plus a +-- structural recursion on `WfCNF t` using +-- `rank-pow-bplus-into-ω-rank-pow` at each `bplus` step. +-- * `rank-mono-<ᵇ-+1-via-head-Ω` (the headline discharge). Builds +-- on the domination lemma + `rank-mono-<ᵇ-+1-via-target` from +-- `RankPow.agda`. + +module Ordinal.Buchholz.HeadOmega where + +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Ordinal.OmegaMarkers using (OmegaIndex; fin; ω) +open import Ordinal.Buchholz.Syntax using + ( BT + ; bzero + ; bOmega + ; bplus + ; bpsi + ) + +---------------------------------------------------------------------- +-- `head-Ω : BT → OmegaIndex` — leading-Ω-index head function +---------------------------------------------------------------------- + +-- The leftmost-deepest Ω marker carried by the term. +-- +-- * `bzero` ↦ `fin 0` (default; bzero has no Ω marker — the +-- future rank-mono lemma will require a +-- non-bzero premise so this default is never +-- consumed in proofs). +-- * `bOmega ν` ↦ `ν` (the Ω marker IS ν). +-- * `bplus x y` ↦ `head-Ω x` (leftmost — the WfCNF tail bound +-- `y ≤ᵇ x` means y's leading Ω is dominated by +-- x's, so the leftmost is also the deepest). +-- * `bpsi ν α` ↦ `ν` (the ψ-binder's Ω-index dominates the +-- argument α, mirroring the provisional +-- `rank-pow (bpsi ν α) = ω-rank-pow ν` shape in +-- `RankPow.agda`). +-- +-- Termination is structural (size-decreasing on the first argument +-- of `bplus`), no decreasing measure needed. + +head-Ω : BT → OmegaIndex +head-Ω bzero = fin 0 +head-Ω (bOmega ν) = ν +head-Ω (bplus x _) = head-Ω x +head-Ω (bpsi ν _) = ν + +---------------------------------------------------------------------- +-- Definitional sanity, one lemma per `BT` constructor +---------------------------------------------------------------------- + +-- These are all `refl` — they record the defining equations so that +-- downstream slices can rewrite by them at consumer sites without +-- unfolding `head-Ω` (or, equivalently, naming the equations +-- explicitly when the unfolding is inconvenient in tactic position). + +head-Ω-bzero : head-Ω bzero ≡ fin 0 +head-Ω-bzero = refl + +head-Ω-bOmega : ∀ ν → head-Ω (bOmega ν) ≡ ν +head-Ω-bOmega _ = refl + +head-Ω-bplus : ∀ x y → head-Ω (bplus x y) ≡ head-Ω x +head-Ω-bplus _ _ = refl + +head-Ω-bpsi : ∀ ν α → head-Ω (bpsi ν α) ≡ ν +head-Ω-bpsi _ _ = refl + +---------------------------------------------------------------------- +-- Compositional convenience +---------------------------------------------------------------------- + +-- `head-Ω` of a left-leaning `bplus` chain bottoms out at the +-- leftmost atom's leading Ω. Direct consequence of `head-Ω-bplus` +-- applied twice; provided as a named lemma because the two-level +-- pattern recurs in any rank-mono discharge that walks the WfCNF +-- left spine of a `bplus`. + +head-Ω-bplus-left : ∀ x y z → head-Ω (bplus (bplus x y) z) ≡ head-Ω x +head-Ω-bplus-left _ _ _ = refl diff --git a/proofs/agda/Ordinal/Buchholz/RankAdm.agda b/proofs/agda/Ordinal/Buchholz/RankAdm.agda new file mode 100644 index 0000000..bdd4898 --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/RankAdm.agda @@ -0,0 +1,280 @@ +{-# OPTIONS --safe --without-K #-} + +-- Admissibility-aware rank for Buchholz terms (Lane 3 active-push +-- slice, 2026-05-26). +-- +-- ## Where this sits +-- +-- `Ordinal.Buchholz.RankPow.rank-pow` uses the provisional shape +-- `rank-pow (bpsi ν _) = ω-rank-pow ν`, which is α-blind and so +-- cannot discriminate the shared-Ω-index lex constructor +-- `<ᵇ⁺-ψα : ν₁ ≡ ν₂ → α <ᵇ β → bpsi ν₁ α <ᵇ⁺ bpsi ν₂ β` of +-- `Ordinal.Buchholz.OrderExtended._<ᵇ⁺_`. Two of the three open +-- constructor cases in `docs/echo-types/buchholz-rank-obstruction.adoc` +-- (`<ᵇ⁺-ψα`, `<ᵇ-ψΩ≤`) are flagged there as needing a ψ-admissibility +-- rank refinement; `WellFormedAdmissible.agda` landed the carrier +-- (`WfAdm` + the rank-bound on the `bpsi` constructor); this module +-- lands the refined rank itself and discharges the `<ᵇ⁺-ψα` half of +-- the two-case unblock. +-- +-- ## What this slice closes +-- +-- 1. `rank-adm : BT → Ord`, an α-discriminating rank that diverges +-- from `rank-pow` only on the `bpsi` case: +-- `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`. +-- 2. `rank-pow≤rank-adm : ∀ t → rank-pow t ≤′ rank-adm t` — the new +-- rank dominates the provisional one, so the existing 10-case +-- `_<ᵇ⁰_` umbrella's rank-mono lifts to `rank-adm` consumers via +-- monotonicity (caller composes). +-- 3. `rank-mono-<ᵇ⁺-ψα-from-pow` — the headline primitive: from a +-- `rank-pow α <′ rank-pow β` hypothesis (which the existing +-- umbrella `rank-pow-mono-<ᵇ⁰` discharges for any +-- `<ᵇ⁰`-derivable `α <ᵇ⁰ β`), produces +-- `rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β)`. +-- 4. `rank-adm-bpsi-bounded-under-adm` — the admissibility-source- +-- bound lemma referenced in CLAUDE.md. Under `WfAdm (bpsi ν α)`, +-- `rank-adm (bpsi ν α) <′ ω-rank-pow (suc-Ω ν)` where +-- `suc-Ω ν` is the syntactic next-Ω-marker, via the +-- additive-principal closure of `ω-rank-pow ν`. Documented; +-- full statement TBD pending a `suc-Ω` operation on the open +-- `OmegaIndex` set. +-- +-- ## What this slice deliberately does NOT close +-- +-- * `<ᵇ-ψΩ≤` at ν = μ. The classical Buchholz semantics has +-- ψ_μ(α) < Ω_μ under admissibility (this is what admissibility +-- *means*). Under the present syntactic-rank encoding +-- `ω-rank-pow ν` ↔ Ω_ν and `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`, +-- we would need `ω-rank-pow ν ⊕ rank-pow α <′ ω-rank-pow ν`, +-- which is impossible because `ω-rank-pow ν ≤′ ω-rank-pow ν ⊕ rank-pow α` +-- by `⊕-left-≤-sum`. This is a classical-vs-syntactic encoding +-- mismatch surfaced by the slice: the next-Ω-marker gap that +-- classical admissibility lives inside is *not modelled* by the +-- present rank. Closure requires either a two-component lex +-- rank (`(ω-rank-pow ν, rank-pow α)` with lex order) or a richer +-- target encoding `ω-rank-pow ν · ω + rank-pow α`. Recorded as +-- a design follow-up in `docs/echo-types/buchholz-rank-obstruction.adoc` +-- and pinned in this module's `<ᵇ-ψΩ≤-still-open` comment block +-- below so the next session sees the constraint without re-deriving +-- it. +-- * `<ᵇ-+1` joint-bplus. Unchanged from `RankPow.agda`'s deferral +-- — this slice is ψ-side only. +-- +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) +-- +-- * `rank-adm` -- the admissibility-aware rank +-- * `rank-adm-bzero`, `rank-adm-bOmega`, +-- `rank-adm-bplus`, `rank-adm-bpsi` -- definitional sanity +-- * `rank-pow≤rank-adm` -- new dominates provisional +-- * `rank-mono-<ᵇ⁺-ψα-from-pow` -- the slice's headline primitive +-- * `rank-adm-pos-bpsi` -- positivity at the bpsi case + +module Ordinal.Buchholz.RankAdm where + +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Ordinal.OmegaMarkers using (OmegaIndex) +open import Ordinal.Brouwer using (Ord; oz; osuc) +open import Ordinal.Brouwer.Arithmetic using (_⊕_) +open import Ordinal.Brouwer.Phase13 using + ( _≤′_ + ; _<′_ + ; ≤′-refl + ; ≤′-trans + ; ⊕-mono-<-right + ; ⊕-mono-≤-left + ; ⊕-mono-≤-right + ; ⊕-left-≤-sum + ) +open import Ordinal.Buchholz.Syntax using + ( BT + ; bzero + ; bOmega + ; bplus + ; bpsi + ) +open import Ordinal.Buchholz.RankPow using + ( rank-pow + ; ω-rank-pow + ; ω-rank-pow-pos + ) + +---------------------------------------------------------------------- +-- The admissibility-aware rank +---------------------------------------------------------------------- + +-- Diverges from `rank-pow` only on `bpsi`: the α-tail contributes +-- to the rank, so the shared-Ω-index lex case `<ᵇ⁺-ψα` is no longer +-- collapsed to a same-rank pair. + +rank-adm : BT → Ord +rank-adm bzero = oz +rank-adm (bOmega ν) = ω-rank-pow ν +rank-adm (bplus x y) = rank-adm x ⊕ rank-adm y +rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α + -- The α-tail uses `rank-pow`, not `rank-adm`, deliberately: + -- the existing umbrella `rank-pow-mono-<ᵇ⁰` discharges rank-pow + -- comparisons on the inner α; lifting the tail to `rank-adm` + -- would require a recursive primitive we have not yet proved. + -- See `<ᵇ-ψΩ≤-still-open` for the design constraint that fixes + -- this choice. + +---------------------------------------------------------------------- +-- Definitional sanity +---------------------------------------------------------------------- + +rank-adm-bzero : rank-adm bzero ≡ oz +rank-adm-bzero = refl + +rank-adm-bOmega : ∀ ν → rank-adm (bOmega ν) ≡ ω-rank-pow ν +rank-adm-bOmega _ = refl + +rank-adm-bplus : ∀ x y → rank-adm (bplus x y) ≡ rank-adm x ⊕ rank-adm y +rank-adm-bplus _ _ = refl + +rank-adm-bpsi : ∀ ν α → rank-adm (bpsi ν α) ≡ ω-rank-pow ν ⊕ rank-pow α +rank-adm-bpsi _ _ = refl + +---------------------------------------------------------------------- +-- Positivity at the bpsi case +---------------------------------------------------------------------- + +-- `oz <′ rank-adm (bpsi ν α)`. Useful for the `<ᵇ-0-ψ` +-- rank-mono case under `rank-adm` consumers (which the existing +-- `rank-mono-<ᵇ-0-ψ : oz <′ rank-pow (bpsi ν α) = ω-rank-pow ν` +-- discharges only for the rank-pow consumer). + +rank-adm-pos-bpsi : ∀ {ν α} → oz <′ rank-adm (bpsi ν α) +rank-adm-pos-bpsi {ν} {α} = + -- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α; first summand + -- is strictly positive by ω-rank-pow-pos, and ⊕-left-≤-sum makes + -- the whole sum dominate. + let + pos-left : oz <′ ω-rank-pow ν + pos-left = ω-rank-pow-pos ν + left≤sum : ω-rank-pow ν ≤′ ω-rank-pow ν ⊕ rank-pow α + left≤sum = ⊕-left-≤-sum {ω-rank-pow ν} (rank-pow α) + in + ≤′-trans + {osuc oz} {ω-rank-pow ν} {ω-rank-pow ν ⊕ rank-pow α} + pos-left + left≤sum + +---------------------------------------------------------------------- +-- `rank-pow ≤′ rank-adm` (dominance) +---------------------------------------------------------------------- + +-- The admissibility-aware rank dominates the provisional one +-- pointwise. Used by callers that have a `rank-pow` strict-mono +-- conclusion in hand and want to lift it to `rank-adm`. + +rank-pow≤rank-adm : ∀ t → rank-pow t ≤′ rank-adm t +rank-pow≤rank-adm bzero = ≤′-refl {oz} +rank-pow≤rank-adm (bOmega ν) = ≤′-refl {ω-rank-pow ν} +rank-pow≤rank-adm (bpsi ν α) = + -- rank-pow (bpsi ν α) = ω-rank-pow ν; + -- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α. + -- The left summand is ≤ the sum. + ⊕-left-≤-sum {ω-rank-pow ν} (rank-pow α) +rank-pow≤rank-adm (bplus x y) = + -- rank-pow (bplus x y) = rank-pow x ⊕ rank-pow y; + -- rank-adm (bplus x y) = rank-adm x ⊕ rank-adm y. + -- Compose left-mono with right-mono via transitivity through the + -- intermediate `rank-adm x ⊕ rank-pow y`: + -- rank-pow x ⊕ rank-pow y + -- ≤′ rank-adm x ⊕ rank-pow y (⊕-mono-≤-left on rank-pow≤rank-adm x) + -- ≤′ rank-adm x ⊕ rank-adm y (⊕-mono-≤-right on rank-pow≤rank-adm y) + ≤′-trans + {rank-pow x ⊕ rank-pow y} + {rank-adm x ⊕ rank-pow y} + {rank-adm x ⊕ rank-adm y} + (⊕-mono-≤-left {rank-pow x} {rank-adm x} {rank-pow y} + (rank-pow≤rank-adm x)) + (⊕-mono-≤-right {rank-adm x} {rank-pow y} {rank-adm y} + (rank-pow≤rank-adm y)) + +---------------------------------------------------------------------- +-- Headline primitive: `<ᵇ⁺-ψα` rank-mono under `rank-adm` +---------------------------------------------------------------------- + +-- Given a `rank-pow α <′ rank-pow β` hypothesis (produced by the +-- existing umbrella for any `α <ᵇ⁰ β` per +-- `Ordinal.Buchholz.RankMonoUmbrella.rank-pow-mono-<ᵇ⁰`), conclude +-- `rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β)`. +-- +-- This is the slice's load-bearing addition: it discharges the +-- *first* of the two ψ-admissibility-blocked constructor cases +-- (`<ᵇ⁺-ψα`). See `<ᵇ-ψΩ≤-still-open` comment block below for the +-- structural reason the *second* case (`<ᵇ-ψΩ≤`) does not close +-- under this rank shape. + +rank-mono-<ᵇ⁺-ψα-from-pow : ∀ {ν α β} + → rank-pow α <′ rank-pow β + → rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β) +rank-mono-<ᵇ⁺-ψα-from-pow {ν} {α} {β} p = + -- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α; + -- rank-adm (bpsi ν β) = ω-rank-pow ν ⊕ rank-pow β. + -- Pure right-strict-mono of `_⊕_` against the hypothesis. + ⊕-mono-<-right {ω-rank-pow ν} {rank-pow α} {rank-pow β} p + +---------------------------------------------------------------------- +-- `<ᵇ-ψΩ≤-still-open` — the design constraint this slice surfaces +---------------------------------------------------------------------- + +-- `<ᵇ-ψΩ≤ : ν ≤Ω μ → bpsi ν α <ᵇ bOmega μ` ranges over ν ≤Ω μ, +-- INCLUDING the boundary case ν = μ. Under admissibility, +-- `rank-pow α <′ ω-rank-pow ν` holds (`WfAdm` predicate's +-- `bpsi`-constructor rank bound). +-- +-- Under `rank-adm`: +-- rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α +-- rank-adm (bOmega μ) = ω-rank-pow μ +-- +-- Case `ν <Ω μ` (strict). Both summands are strictly below +-- `ω-rank-pow μ` (rank-pow α via admissibility + transit through +-- `ω-rank-pow ν <′ ω-rank-pow μ`; `ω-rank-pow ν` directly via +-- `ω-rank-pow-mono`). `additive-principal-ω-rank-pow {μ}` closes. +-- This case is straightforward and the follow-on slice will land it. +-- +-- Case `ν = μ` (boundary). Need +-- `ω-rank-pow μ ⊕ rank-pow α <′ ω-rank-pow μ`, +-- but `ω-rank-pow μ ≤′ ω-rank-pow μ ⊕ rank-pow α` always (left-≤-sum), +-- so a strict `<′ ω-rank-pow μ` conclusion forces the absurd +-- `ω-rank-pow μ <′ ω-rank-pow μ`. Impossible under this rank shape. +-- +-- The classical reading: ψ_μ(α) for admissible α lives in the gap +-- [ω-rank-pow μ, ω-rank-pow (μ+1)) +-- (it is a countable ordinal below the next cardinal threshold). +-- The present rank `ω-rank-pow ν ⊕ rank-pow α` collapses that gap; +-- the constraint `α <′ ω-rank-pow ν` does not buy `<′ ω-rank-pow ν` +-- for the sum, only for the right summand. +-- +-- Design follow-ups (not landed in this slice): +-- +-- (A) Two-component lex rank. `rank-lex : BT → Ord × Ord` +-- comparing first lex-by-`<′`-then-`≤′` on the second. The +-- ψ-case is `(ω-rank-pow ν, rank-pow α)`, the Ω-case is +-- `(ω-rank-pow μ, oz)`. Closes `<ᵇ-ψΩ≤` cleanly (when +-- `ν = μ`, first components are equal and admissibility's +-- `rank-pow α <′ ω-rank-pow ν` on the second component +-- carries the strict-less-than). Cost: every existing +-- rank-mono primitive in `RankPow` needs a lex re-statement. +-- +-- (B) Successor-multiplied rank. Define a `_·ω_` operation on +-- `Ord` and set `rank-adm (bpsi ν α) = ω-rank-pow ν ·ω + rank-pow α` +-- so the ψ-rank lives strictly between two consecutive +-- Ω-ranks. Cost: a multiplicative ordinal-arithmetic layer +-- beyond what `Ordinal.Brouwer.Arithmetic` currently ships; +-- `(·ω)`'s monotonicity lemmas would be a separate +-- sub-slice's worth of work. +-- +-- (C) Stratify `_<ᵇ_` into a ν-respecting equivalence and use +-- a per-ν rank. Heaviest re-architecture; mentioned for +-- completeness only. +-- +-- Recommendation for the follow-on slice: option (A). It reuses +-- the existing `RankPow` primitives verbatim on the first +-- component and the existing scalar `<′` / `≤′` infrastructure on +-- the second; the lex order propagates cleanly to a new umbrella. +-- Option (B) is ordinally cleaner but ships a new arithmetic +-- layer. diff --git a/proofs/agda/Ordinal/Buchholz/RankLex.agda b/proofs/agda/Ordinal/Buchholz/RankLex.agda new file mode 100644 index 0000000..b24a02c --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/RankLex.agda @@ -0,0 +1,186 @@ +{-# OPTIONS --safe --without-K #-} + +-- Lex-pair rank for Buchholz terms (Lane 3 follow-on slice, 2026-05-27). +-- +-- ## Where this sits +-- +-- `Ordinal.Buchholz.RankAdm.rank-adm` discharged the `<ᵇ⁺-ψα` +-- (shared-Ω-index lex) constructor by shifting the ψ-rank from +-- `ω-rank-pow ν` (α-blind) to `ω-rank-pow ν ⊕ rank-pow α` +-- (α-discriminating). That fixed `<ᵇ⁺-ψα` cleanly, but it surfaced +-- a new gap: the `<ᵇ-ψΩ≤` constructor at the ν = μ boundary case is +-- *structurally impossible* under any scalar `Ord`-valued rank with +-- `ω-rank-pow ν ≤ rank-adm (bpsi ν α)` — that monotonicity forces +-- the goal `rank-adm (bpsi ν α) <′ ω-rank-pow ν` to imply the absurd +-- `ω-rank-pow ν <′ ω-rank-pow ν` (see `RankAdm.agda` +-- §"<ᵇ-ψΩ≤-still-open" for the full diagnostic). +-- +-- The recommended follow-up there was option (A): a two-component +-- lex rank. This module lands it as a *thin* slice: the lex pair +-- exists alongside `rank-pow` and `rank-adm`, only for the headline +-- `<ᵇ-ψΩ≤` close-out. The existing 10 + 1 = 11 closed cases +-- continue to consume the scalar `rank-pow` / `rank-adm` infrastructure +-- unchanged. +-- +-- ## What this slice closes +-- +-- 1. `RankLex` record with two `Ord` fields (`first`, `second`). +-- 2. `_