diff --git a/CHANGELOG.md b/CHANGELOG.md index 50863ee..c0ef84d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,84 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). ## [Unreleased] +### Added (2026-05-28) + +- *Lane 3 ordinal track — Slice 3 prerequisites.* PR #137 added + `proofs/agda/Ordinal/Buchholz/RankPowSlice3.agda` (220 lines) — + three primitives toward the Slice 3 headline: + - `NonBzero` — left-spine non-bzero predicate excluding the + degenerate `bplus bzero bzero` chains that WfCNF technically + allows but CNF normalisation excludes. + - `ω-rank-pow-succ-≤-via-<Ω` — strict-jump bridge from `μ <Ω ν` + to `ω-rank-pow-succ μ ≤′ ω-rank-pow ν`. Closes the gap between + Slice 2-bplus's upper bound on the source's rank and the lower + bound on the target's rank. + - `head-Ω-lower-bound` — head-Ω LOWER bound under WfCNF + + NonBzero. Dual of `rank-pow-dominated-by-head-Ω`. + +- *Lane 3 ordinal track — Slice 3 headline closed under a strict-head + premise.* PR #141 added + `proofs/agda/Ordinal/Buchholz/RankPowSlice3Headline.agda` (155 + lines). The headline `rank-mono-<ᵇ-+1-via-head-Ω` closes the + joint-bplus rank-mono case for `_<ᵇ-+1_` via Route A from the + Slice 3 design note. The proof composes the four Slice 3 + prerequisites in a clean chain (no structural recursion): + Slice 2-bplus + head-Ω-bplus → strict-jump bridge → head-Ω lower + bound → `⊕-left-≤-sum`, all via `≤′-trans`. The headline takes + the strict-head premise `head-Ω x₁ <Ω head-Ω y₁` as an EXTERNAL + HYPOTHESIS; the umbrella's case-split is the remaining wiring + (the `bpsi=bpsi` at equal markers sub-case still needs `α`'s + rank via rank-adm or rank-lex). Compiles standalone under + `--safe --without-K`, zero postulates. Smoke green. + +- *Canonical identity layer — (epi, mono) earn-back form.* PR #138: + `proofs/agda/EchoImageFactorizationProp.agda` lands the + (epi, mono) factorisation module-parameterised in a truncation + interface — the long-pending earn-back gate previously referenced + as "next" in `docs/echo-types/MAP.adoc`. Companion to + `EchoImageFactorization`. Classification: Tier 2 in + `docs/echo-types/echo-kernel-note.adoc`. + +- *Classification grid — Search + Epistemic ResidueForm instances.* + PR #139: `EchoResidueTaxonomy.agda` gains two further `ResidueForm + f R` instances (`Search` and `Epistemic`) alongside the existing + four (trivial, identity, generic Σ-cert, linear-affine). Brings + the total to six instances, with the other four decoration + modules documented as structurally compatible. + +- *Visual identity — banner kit ("Diagrammatic Hush").* PR #140: + `docs/assets/banner.{png,svg}`, `docs/assets/banner-philosophy.md`, + `tools/banner/build-banner.mjs`. The `README.md` and `readme.adoc` + both gained the banner image at the top. No content impact; purely + visual identity for the project's public surface. + +### Fixed (2026-05-28) + +- *CI hygiene: kernel-guard classification-drift unblocked.* PR #136: + 18 previously-unclassified `Echo*.agda` modules (the canonical- + identity / OFS cohort plus the application/extension modules: + `EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`, + `EchoImageFactorization`, `EchoNoSectionGeneric`, + `EchoLossTaxonomy`, `EchoResidueTaxonomy`, + `EchoDecorationStructure`, `EchoObservationalEquivalence`, + `EchoOFSUnivF5`/`Diag`/`Iso`, `EchoCanonicalIdentitySuite`, + `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`, + `EchoProbabilisticSupport`, `EchoDifferential`) are now classified + in `docs/echo-types/echo-kernel-note.adoc`, unblocking + `scripts/kernel-guard.sh` Check B (classification-drift lint). + +- *CI hygiene: N5Falsifier xfail gate removed.* PR #136 also dropped + the `Expected-failure gate (N5Falsifier is known-broken)` step + from `.github/workflows/agda.yml`. `proofs/agda/characteristic/ + N5Falsifier.agda` was resolved on 2026-05-27 by pinning the + implicit `r` / `grade` at four `applyRole` / `applyGrade` call + sites — the unsolved-metas were an inference blocker, not a + content blocker. The module is now imported by + `proofs/agda/characteristic/All.agda` (line 33). The xfail gate's + own self-disclosed instructions (`"register it in + characteristic/All.agda and remove this xfail gate"`) fired on + the previous CI run; this PR completed those instructions. + ### Added (2026-05-27) - *Lane 3 ordinal track — 11/13 Buchholz constructors closed under diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 59a47c6..1221bd6 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -34,12 +34,16 @@ Ongoing tracks at a glance (point-in-time, see `roadmap.adoc` for the live statu * *Identity claim.* `docs/retractions.adoc` R-2026-05-18 narrows the public claim to a *loss-graded reindexing modality* over a thin poset (not a graded comonad). Every newer artefact is stated within those narrowings. * *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. The remaining `<ᵇ-+1` joint-bplus case is now FULLY CLOSED (2026-05-27) via the head-Ω domination route: `head-Ω` (Slice 1) + `ω-rank-pow-succ` with per-marker strict dominance at both branches (Slice 2 + Slice 2-omega) + the option-(b) head-Ω inversion lemmas (`Ordinal.Buchholz.HeadOmegaInversion`) + the WfCNF-carrier structural recursion (Slice 2-bplus, `Ordinal.Buchholz.RankPowDomination.rank-pow-dominated-by-head-Ω`). See `docs/echo-types/buchholz-rank-obstruction.adoc`. +* *Ordinal / Buchholz track — Slice 3 (2026-05-28).* `Ordinal.Buchholz.RankPowSlice3` lands three primitives — `NonBzero` (left-spine non-bzero predicate), `ω-rank-pow-succ-≤-via-<Ω` (strict-jump bridge), and `head-Ω-lower-bound` (dual of `rank-pow-dominated-by-head-Ω`). On top of those, `Ordinal.Buchholz.RankPowSlice3Headline` closes the Slice 3 headline `rank-mono-<ᵇ-+1-via-head-Ω` via Route A — a clean chain through the four prerequisites with no structural recursion, taking the strict-head premise `head-Ω x₁ <Ω head-Ω y₁` as an *external hypothesis*. The umbrella case-split is the remaining wiring; the `bpsi = bpsi at equal markers` sub-case still needs `α`'s rank via rank-adm or rank-lex. +* *Canonical identity layer (Tier 1 + Tier 2 extensions, 2026-05-28).* `EchoImageFactorizationProp` lands the (epi, mono) earn-back module, module-parameterised in a truncation interface (Tier 2, adjacent to `EchoImageFactorization`). `EchoResidueTaxonomy`'s `ResidueForm f R` record gains `Search` and `Epistemic` instances alongside the existing four (trivial, identity, generic Σ-cert, linear-affine). +* *CI / foundational hygiene (2026-05-28).* Kernel-guard discipline scaled to the canonical-identity cohort: 18 previously-unclassified `Echo*.agda` modules (the canonical-identity / OFS cohort plus the application/extension modules — `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`, `EchoProbabilisticSupport`, `EchoDifferential`) are now classified in `docs/echo-types/echo-kernel-note.adoc`. The (now-stale) `N5Falsifier` xfail gate was removed from `.github/workflows/agda.yml` following the 2026-05-27 resolution of `proofs/agda/characteristic/N5Falsifier.agda` (the unsolved-metas were an inference blocker, not a content blocker; four `applyRole` / `applyGrade` call sites had their implicit `r` / `grade` pinned). This is infrastructure honesty, not a proof-content advance. * *Tutorial track (Lane 5).* Three worked walkthroughs under `tutorial/` (certified region-exit audit, epistemic erasure, provenance/debugging echo); each carries an honest-bound disclosure at the top and a matched-negative block at the bottom. The tutorial tree builds with the repo root added to the Agda include path; see `tutorial/README.adoc`. * *Establishment track (Pillar E).* Internal programme (Pillars A–D) complete since 2026-05-17. The paper (`docs/echo-types/paper.adoc`) is a living draft with remaining `[EXPAND]` tags; the venue + Zenodo + outreach plan sits in `docs/echo-types/pillar-e-offline.adoc` (author-driven). == Where to look first * `docs/echo-types/MAP.adoc` — the master map (every direction, status-tagged). +* `docs/echo-types/echo-kernel-note.adoc` — kernel-vs-derived classification; status SoT for the `Echo*.agda` dependency cone. * `roadmap.adoc` + `roadmap-gates.adoc` — lane structure + identity-claim gates. * `tutorial/README.adoc` — the pedagogy track if you want to read worked examples first. * `docs/retractions.adoc` — read before citing any claim above as final. diff --git a/README.md b/README.md index 8ac7641..590b6c4 100644 --- a/README.md +++ b/README.md @@ -32,8 +32,8 @@ flowchart TD F["Foundation
Echo f y := Σ (x : A) , (f x ≡ y)
= homotopy fibre"] AD["Pillars A–D (establishment plan, LANDED 2026-05-17)
A: echo↔fib · B: pullback UP · C: separating model · D: carrier-parametric"] PF["Pillar F gates (earn-back, ALL PASSED)
F1: graded-comonad witness · F2: 2nd Echo-functor model
F3: 2nd non-iso grade-monoid · F4: funext-qualified pullback UP
F5: funext-qualified full OFS"] - T1["Tier 1 · Canonical identity layer (2026-05-27)
EchoTotalCompletion (A ≃ Σ B Echo f) · OFS-witness · Image · no-section-of-collapsing-map"] - T2["Tier 2 · Classification grid
LossTaxonomy (function-side) · ResidueTaxonomy (residue-side) · DecorationStructure · _≡m_"] + T1["Tier 1 · Canonical identity layer (2026-05-27, extended 2026-05-28)
EchoTotalCompletion (A ≃ Σ B Echo f) · OFS-witness · Image · no-section-of-collapsing-map · ImageFactorizationProp (epi,mono earn-back)"] + T2["Tier 2 · Classification grid
LossTaxonomy (function-side) · ResidueTaxonomy (residue-side, 6 instances incl. Search + Epistemic) · DecorationStructure · _≡m_"] T3["Tier 3 · Qualified universal property (Gate F5)
echo-factorisation-strict · diagonal lifting · factorisation uniqueness up to iso"] AUD["Audience surfaces
EchoProvenance · EchoSecurity · EchoProbabilisticSupport · EchoDifferential"] SUITE["EchoCanonicalIdentitySuite
(curated single-file entry point)"] diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 22d9882..a7f42f4 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -78,8 +78,13 @@ in the Pillar F4 template style. * *Image factorisation* — `Image f := Σ B (Echo f)`; the proof- relevant image IS the total Echo space. Three classifications (Surjective, Injective, projection-uniqueness under injectivity). - The (epi, mono) truncation form is the next earn-back gate. `proofs/agda/EchoImageFactorization.agda`. +* *Image factorisation, (epi, mono) form (2026-05-28)* — the + (epi, mono) earn-back module, module-parameterised in a + truncation interface. Companion to `EchoImageFactorization`; + the previously-pending (epi, mono) form now lands without + committing the kernel to a specific truncation primitive. + `proofs/agda/EchoImageFactorizationProp.agda`. * *Generic no-section* — `no-section-of-collapsing-map`: for ANY collapsing map with two distinct elements landing on the same image, no section exists. Lifts the previous single-instance @@ -93,10 +98,11 @@ in the Pillar F4 template style. `proofs/agda/EchoLossTaxonomy.agda`. * *Residue taxonomy* (residue-side) — `record ResidueForm f R` packaging the per-output residue carrier + lowering shared by the - eight decoration modules. Four instances: trivial (⊤), identity - (`Echo f`), generic Σ-cert (`echoR-residue`), and the worked - `linear-affine-residue`. The other six decoration modules - documented as structurally compatible. + eight decoration modules. Six instances (as of 2026-05-28): trivial + (⊤), identity (`Echo f`), generic Σ-cert (`echoR-residue`), + `linear-affine-residue`, and the newer `Search` + `Epistemic` + forms. The other four decoration modules documented as structurally + compatible. `proofs/agda/EchoResidueTaxonomy.agda`. * *Decoration structure* (observation-side) — `record DecorationStructure G` packaging the seven-field decoration @@ -228,7 +234,12 @@ Staged Buchholz-style collapsing in `--safe --without-K`. * Proofs: `proofs/agda/Ordinal/` (`Buchholz/`, `Brouwer`, `CNF`, `Closure`, `Psi…`, `ExtendedOrder`, `RankPow`, `RankAdm`, - `RankLex`, `HeadOmega`, `HeadOmegaInversion`, `RankPowDomination`). + `RankLex`, `HeadOmega`, `HeadOmegaInversion`, `RankPowDomination`, + `RankPowSlice3` (2026-05-28 — `NonBzero` + strict-jump bridge + + head-Ω lower bound), `RankPowSlice3Headline` (2026-05-28 — Slice 3 + headline `rank-mono-<ᵇ-+1-via-head-Ω` closed under a strict-head + premise; umbrella case-split bumps `bpsi=bpsi at equal markers` + to rank-adm / rank-lex)). * Docs: `docs/buchholz-plan.adoc`, `docs/echo-types/buchholz-extended-wf.md`, `docs/echo-types/buchholz-rank-obstruction.adoc` (per-constructor diff --git a/readme.adoc b/readme.adoc index 2001c8e..e3e1f77 100644 --- a/readme.adoc +++ b/readme.adoc @@ -68,12 +68,13 @@ Tier 1 (the canonical identity layer itself): * `EchoTotalCompletion.agda` — `A ≃ Σ B (Echo f)` * `EchoOrthogonalFactorizationSystem.agda` — `ofs-witness` * `EchoImageFactorization.agda` — `Image f := Σ B (Echo f)` +* `EchoImageFactorizationProp.agda` — (epi, mono) earn-back form, module-parameterised in a truncation interface (2026-05-28) * `EchoNoSectionGeneric.agda` — `no-section-of-collapsing-map` Tier 2 (the classification grid): * `EchoLossTaxonomy.agda` — function-side four-axis (EQUIV / INJ / SURJ / CONST) -* `EchoResidueTaxonomy.agda` — `ResidueForm` record + instances +* `EchoResidueTaxonomy.agda` — `ResidueForm` record + 6 instances (trivial, identity, generic Σ-cert, linear-affine, Search, Epistemic; the last two added 2026-05-28) * `EchoDecorationStructure.agda` — `DecorationStructure` record + abstract degrade-compose * `EchoObservationalEquivalence.agda` — mode-indexed `_≡m_` on `LEcho`