From f67fbe61232f81d3bd5a162292a5d906c3612cd2 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 11:37:10 +0000 Subject: [PATCH 1/2] =?UTF-8?q?proof(entropy):=20entropy-blind-parametric?= =?UTF-8?q?=20=E2=80=94=20parametric-distribution=20non-distinguishing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalises EchoEntropy's discrete fibre-count blindness (Headline 3, entropy-shadow-blind, a function of a single ℕ count) to the parametric form the companion remark flagged open: any information functional H : (Fin 2 → W) → X of any fibre-determined distribution over the fibre of collapse at tt agrees on echo-true and echo-false (entropy-blind-parametric), paired with the matched-negative that a witness-determined distribution distinguishes (entropy-witness-distinguishes, via sigma-distinguishes). The non-distinguishing now holds for ANY real-/rational-/abstract-valued entropy, Renyi entropy or mutual-information functional once supplied — no reals/log library needed, the blindness is structural. Constructing a concrete real-valued H(P) = -Sigma p log p remains an orthogonal reals+logarithm task, independent of Echo, and is deliberately not attempted. Verified: agda proofs/agda/Smoke.agda + proofs/agda/All.agda exit 0 under --safe --without-K, zero postulates, no funext. Both headlines pinned in Smoke.agda. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG --- proofs/agda/EchoEntropy.agda | 100 ++++++++++++++++++++++++++++++----- proofs/agda/Smoke.agda | 2 + 2 files changed, 90 insertions(+), 12 deletions(-) diff --git a/proofs/agda/EchoEntropy.agda b/proofs/agda/EchoEntropy.agda index 6668456..fc5d7c1 100644 --- a/proofs/agda/EchoEntropy.agda +++ b/proofs/agda/EchoEntropy.agda @@ -53,13 +53,21 @@ -- -- matched-negative: proj₁ DOES -- distinguish (cited from -- sigma-distinguishes) +-- * entropy-blind-parametric -- parametric: any functional of any +-- fibre-determined distribution is blind +-- * entropy-witness-distinguishes -- matched-negative (parametric): a +-- witness-determined distribution +-- distinguishes -- --- Scope guardrail. The theorem proved here is the discrete form: --- "any function factoring through the fibre count is constant on --- echo-true vs echo-false". The real-valued form quantifying over --- a parametric probability distribution is a strict generalisation --- and is NOT formalised — see the companion remark at the end of --- the file. +-- Scope guardrail. Two non-distinguishing forms are proved: the +-- discrete one ("any function of the fibre count is constant on +-- echo-true vs echo-false") and its parametric generalisation +-- (`entropy-blind-parametric`: any functional of any fibre-determined +-- distribution is constant, with `entropy-witness-distinguishes` the +-- matched-negative). What is NOT formalised is only the *construction* +-- of a concrete real-valued `H(P) = -Σ p log p` — an orthogonal +-- reals/logarithm task; the non-distinguishing already covers any such +-- functional once supplied. See the companion remark at the end. module EchoEntropy where @@ -206,15 +214,83 @@ witness-distinguishes-where-entropy-cannot : (λ g → g echo-true ≢ g echo-false) witness-distinguishes-where-entropy-cannot = sigma-distinguishes +---------------------------------------------------------------------- +-- Parametric generalisation: arbitrary distribution, arbitrary +-- information functional. +-- +-- Headline 3 (`entropy-shadow-blind`) covers any function of the +-- fibre *count* — a single `ℕ`. The strictly stronger statement the +-- companion remark flags as open quantifies instead over a whole +-- *distribution* across the fibre — the data a real-valued +-- `H(P) = -Σ p log p` actually consumes — valued in an arbitrary +-- weight type `W` and fed to an arbitrary information functional +-- `H : (Fin 2 → W) → X` (Shannon / Rényi entropy, mutual +-- information, the raw probability vector, …). +-- +-- The fibre of `collapse` at `tt` is the whole domain `Fin 2`, +-- shared by both echoes. A distribution *read off the fibre* (not off +-- the witness `proj₁ e`) does not mention the echo, so any functional +-- of it is blind. This discharges the *non-distinguishing* content of +-- the "parametric probability distribution" item for ANY such +-- functional, with no reals/log library required — the blindness is +-- structural. Constructing a concrete real-valued `-Σ p log p` is an +-- orthogonal analysis task (a reals + logarithm formalisation), +-- independent of Echo, and is deliberately NOT attempted here. +---------------------------------------------------------------------- + +-- A fibre-determined distribution valued in `W`: a weight per fibre +-- index, chosen independently of which echo is held. It ignores its +-- echo argument — that is exactly what "read off the fibre, not the +-- witness" means. +fibre-distribution : {W : Set ℓ} → (Fin 2 → W) → Echo collapse tt → (Fin 2 → W) +fibre-distribution P _ = P + +---------------------------------------------------------------------- +-- Headline 6 (positive, parametric). Any information functional `H` +-- of any fibre-determined distribution `P` agrees on `echo-true` and +-- `echo-false`. Strictly generalises Headline 3 from a function of +-- the count to a functional of the full distribution — covering +-- real-/rational-/abstract-valued entropy the moment such a +-- functional is supplied. Definitional: `fibre-distribution P` +-- ignores its echo argument. +---------------------------------------------------------------------- + +entropy-blind-parametric : + {W X : Set ℓ} + (P : Fin 2 → W) (H : (Fin 2 → W) → X) → + H (fibre-distribution P echo-true) ≡ H (fibre-distribution P echo-false) +entropy-blind-parametric P H = refl + +---------------------------------------------------------------------- +-- Headline 7 (negative companion, parametric). A distribution read +-- off the WITNESS — here every index carries the distinguishing bit +-- `proj₁ sigma-distinguishes e` — DOES separate the two echoes under +-- a functional that samples it. Matched-negative for Headline 6: +-- blindness holds for fibre-determined distributions and fails for +-- witness-determined ones, mirroring the fibre-vs-witness split of +-- the discrete result. +---------------------------------------------------------------------- + +witness-distribution : Echo collapse tt → (Fin 2 → Bool) +witness-distribution e _ = proj₁ sigma-distinguishes e + +entropy-witness-distinguishes : + Σ ((Fin 2 → Bool) → Bool) + (λ H → H (witness-distribution echo-true) ≢ H (witness-distribution echo-false)) +entropy-witness-distinguishes = (λ d → d zero) , proj₂ sigma-distinguishes + ---------------------------------------------------------------------- -- Companion remark on what is NOT claimed. -- --- * Real-valued Shannon entropy `H(P) = -Σ p log p` for a parametric --- probability distribution `P` is NOT formalised. The proof above --- uses the discrete fibre-count proxy, which is the uniform-prior --- surrogate. Lifting to a parametric distribution requires either --- a rationals/reals layer or an axiomatic `Probability` interface, --- neither of which lives in this repo. +-- * The *non-distinguishing* content for a parametric distribution is +-- now formalised: `entropy-blind-parametric` (Headline 6) shows any +-- information functional of any fibre-determined distribution is +-- witness-blind, and `entropy-witness-distinguishes` (Headline 7) is +-- the matched-negative for witness-determined distributions. What +-- remains unformalised is only the *construction* of a concrete +-- real-valued `H(P) = -Σ p log p` — a reals + logarithm formalisation, +-- an analysis task orthogonal to Echo. Headline 6 already covers it +-- for ANY such functional the moment one is supplied. -- -- * Mutual information `I(X; Y) = H(X) - H(X|Y)` is not formalised -- either. The corresponding Echo-side statement would be: diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index a002a2e..14f4068 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -572,6 +572,8 @@ open import EchoEntropy using ; entropy-shadow-blind ; shannon-shadow-blind ; witness-distinguishes-where-entropy-cannot + ; entropy-blind-parametric + ; entropy-witness-distinguishes ) open import EchoThermodynamicsFinite using From ff206ace9c4b1e1ead83d0754962ac0f3c3253ce Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 19:11:48 +0000 Subject: [PATCH 2/2] docs(wiki): refresh status to 2026-06-21 + add developer/maintainer/end-user split - Home.adoc: add a "Who is this for?" tri-split with reading orders for developers (proof discipline + build), maintainers (gates + CI cone + 6a2), and end users (FOUNDATION_CONTRACT + Overview + EchoTypes.jl). Refresh the one-line status to 2026-06-21: ordinal track RETIRED (D-2026-06-21); variance resolved (#243); aggregation generalised (#175); establishment Pillar E in-repo half complete with order-type fidelity the one named OPEN external problem (D-2026-06-14). - Roadmap.adoc: reframe the ordinal track from "active bottleneck" to RETIRED, with the extraction disposition, verified firewall, and frozen open items (tracking #263); fix the carried-debt line that still pointed at the moved ordinal WF items. Refs #263. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG --- wiki/Home.adoc | 68 +++++++++++++++++++++++++++++++++++++++++++---- wiki/Roadmap.adoc | 39 +++++++++++++++------------ 2 files changed, 85 insertions(+), 22 deletions(-) diff --git a/wiki/Home.adoc b/wiki/Home.adoc index a7cd86d..387136d 100644 --- a/wiki/Home.adoc +++ b/wiki/Home.adoc @@ -46,6 +46,48 @@ toc::[] affine mode. |=== +== Who is this for? + +echo-types serves three audiences. Find your lane, then follow the reading order. + +[cols="1,3", options="header"] +|=== +| You are… | Start here, in order + +| *A developer* + + (writing or extending proofs) +| 1. <> — the non-negotiable discipline + (`--safe --without-K`, zero postulates, Smoke pins, `All.agda` wiring). + + 2. `CLAUDE.md` — current rung-state + the per-arc *DO NOT reopen* lists. + + 3. <> + `docs/echo-types/MAP.adoc` — the + module map and where a new theorem belongs. + + 4. *Build:* `bash scripts/provision-agda.sh`, then + `agda -i proofs/agda proofs/agda/All.agda` (and `Smoke.agda`) must exit 0. + +| *A maintainer* + + (gates, releases, governance) +| 1. <> + `roadmap-gates.adoc` — the three identity + gates and their *failure actions* (gates are reassessed every tagged + release). + + 2. `docs/retractions.adoc` — how a failed gate is recorded (never silently + revised). + + 3. `scripts/kernel-guard.sh` + `.github/workflows/agda.yml` — the CI cone + that must stay green. + + 4. `.machine_readable/6a2/STATE.a2ml` (EI-2 record + current state) and + `docs/bridges/cross-repo-bridge-status.md` (downstream ledger). + +| *An end user* + + (wiring Echo into another language) +| 1. `FOUNDATION_CONTRACT.md` — the stable `Echo.*` interface and the boundary + invariant *Echo IS-NOT a resource instance*. Read this first. + + 2. <> — what Echo adds and, crucially, what it does + *not* add (honest scope). + + 3. *EchoTypes.jl* — the executable Julia shadow; falsifies-by-counterexample + on concrete finite data. + + 4. <> — a worked first-class echo property to + see the shape of a consumer-facing result. +|=== + == Canonical sources of truth This wiki is a *distillation*. The authoritative records are: @@ -61,11 +103,27 @@ This wiki is a *distillation*. The authoritative records are: * `.machine_readable/6a2/STATE.a2ml` — EI-2 record (permanent) + current-state block. * `docs/bridges/cross-repo-bridge-status.md` — cross-repo bridge ledger. -== One-line status (as of 2026-06-13) - -* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon). -* *Ordinal track* — partial (Buchholz; Slice 3+4 Route A; target Bachmann–Howard ψ₀(Ω_ω)). -* *Establishment track* — Pillars A–D + Pillar F (F1–F4) closed; Pillar E paper open. +== One-line status (as of 2026-06-21) + +* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon). No open + headline items. +* *Establishment track* — Pillars A–D and F (F1–F4) closed; the in-repo half of + Pillar E is complete at the bounded-claim level. One named *OPEN external* + problem remains: *order-type fidelity* to ψ₀(Ω_ω) (decision-log + `D-2026-06-14`). +* *Variance* — resolved (`EchoVariance.agda`, #243): an echo is a graded + *monad of accumulation* with a section/retraction adjunction exact on the + grade-0 fibre — *not* a graded comonad (that reading is the lossless + complement-storing writer). +* *Aggregation* — `EchoAggregation.agda` generalised to the monoid/group form + (`aggregation-as-fold`; #175), with `no-canonical-disaggregation` (the + Sonnenschein–Mantel–Debreu / representative-agent critique, stated + type-theoretically). +* *Ordinal track* — *RETIRED from echo-types* (owner decision `D-2026-06-21`): + the transfinite Buchholz/Veblen ladder outgrew the project. The landed + artifact is correct and stays; the disposition is *extraction to its own + ordinal-notation repo* (the physical cut is the owner's; tracking: #263). + See <>. * *Deniability track* — `EchoDeniability.agda` landed: perfect/partial duality, `IsConstantOpener` boundary, no-section / section duality as a checked theorem pair. diff --git a/wiki/Roadmap.adoc b/wiki/Roadmap.adoc index 77da45c..7df31cc 100644 --- a/wiki/Roadmap.adoc +++ b/wiki/Roadmap.adoc @@ -55,21 +55,25 @@ The base accumulation iso, cancellation iso, and pentagon coherence are all landed and packaged as `_↔_`. No open headline items; further work is consolidation / doc-threading. -=== Ordinal track — partial (the active bottleneck) - -Target: *Bachmann–Howard* ψ₀(Ω_ω). Open, in priority order: - -. *Unbudgeted `_<ᵇʳᶠ_` global WF* — the GLOBAL form over native `_<ᵇ_` - is *walled* (all five standard routes; native `_<ᵇ_` is ordinally - unsound — see `buchholz-rank-obstruction.adoc`). The SOUND-CARRIER - form is *DONE* (2026-06-14, PR #212): `RecursiveSurfaceSound.wf-<ᵇʳᶠ²` - is unbudgeted, built over `_<ᵇ²_` + the doubled-ladder `rank2` - embedding. Remaining open is only the global-over-native form, whose - realistic close-out is a falsifiable "cannot close under - `--safe --without-K`" verdict rather than a positive proof. -. *Full constructor set beyond the admitted core* — the K-limited shared-binder - cases `<ᵇ-ψα`, `<ᵇ-+2`. -. *Push the surface-route WF back* into `Order.agda`'s main `_<ᵇ_` package. +[#ordinal] +=== Ordinal track — RETIRED from echo-types (owner decision D-2026-06-21) + +The transfinite Buchholz/Veblen ascent *outgrew echo-types* and is *no longer +echo-types work*. The landed artifact is correct (`--safe --without-K`, zero +postulates, in the green closure) and *stays compiling*; *no new ordinal rung +is opened here*. The disposition is *extraction to its own ordinal-notation +repository* — the physical cross-repo cut is the owner's. Tracking: *#263*. + +* *Hand-off record* (frontier + inventory for the extracted repo, NOT a + resume-here plan): `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`. +* *Firewall (verified):* `OmegaMarkers` ← `Buchholz.Syntax` ← `EchoOrdinal` + STAY (Echo Core's bridge); everything else under `proofs/agda/Ordinal/` MOVES. +* *Frozen open items* (for the extracted repo only — NOT echo-types TODOs): + unbudgeted `_<ᵇʳᶠ_` global WF over native `_<ᵇ_` (the sound-carrier form + `RecursiveSurfaceSound.wf-<ᵇʳᶠ²` is already DONE, PR #212); the full + K-limited shared-binder constructor set (`<ᵇ-ψα`, `<ᵇ-+2`); and order-type + fidelity to ψ₀(Ω_ω) (`D-2026-06-14`, an OPEN *external* problem — retirement + neither closes nor over-claims it). === Establishment track — Pillar E only @@ -92,8 +96,9 @@ Pillar E is complete at the bounded-claim level. Remaining: The full debt list, with effort/impact, lives in `.machine_readable/agent_instructions/debt.a2ml`. Highlights: -* *Should:* the two ordinal WF items above; image factorisation (epi, mono) - earn-back (needs propositional truncation — a substantial design decision). +* *Should:* image factorisation (epi, mono) earn-back (needs propositional + truncation — a substantial design decision). (The ordinal WF items moved out + with the ordinal-track retirement — see #263.) * *Could:* decoration-zoo wiring (Cost/Search/Indexed/Epistemic as ResidueForm/DecorationStructure instances); the Q2.1 truncation generalisation; rsr-conformance chores (@sha256 pins, README/roadmap