Add axis 8 (information-theoretic vs computational access)

Promotes the computational-access candidate from the "worth
considering" section in taxonomy.md to a full numbered axis, with
the same structural template used for axes 1-7 (definition,
distinguishing test, forcing example, Agda anchor, candidate
refinements, composition conjecture).

The axis is motivated by the cryptographic-hash example
(examples.md §8) which cannot be distinguished from a constructive
square-root by any of axes 1-7: both have the same extensional
shadow, intensional core, exactness, locality, canonicity,
compositionality, static-ness, and proof-relevance. The only real
distinction is whether a witness can be extracted in feasible
resources — which axes 1-7 do not name.

Four candidate refinements of `Echo` are listed for future
formalisation, roughly in increasing weight:

  1. Cost-indexed echo: pair Echo f y with a witness-extraction
     bound.
  2. Graded access modality: Echo^c f y at grade c meaning
     "reachable within c steps"; natural host is EchoGraded.agda.
  3. Decidability-respecting echo: Echo⁺ f y = Dec (Echo f y);
     separates mathematically-inhabited from feasibly-decidable.
  4. Witness-search abstract machine: model the extractor as a
     term in a bounded-step machine.

The four probably live on a small lattice of access-tracking
theories rather than being subsumed by a single definition.

Downstream updates in this commit:

  * examples.md §8 points to taxonomy.md axis 8 instead of
    treating the axis as a todo.
  * The cross-classification table in taxonomy.md adds an `Access`
    column; every current module is uniformly `Info` (information-
    theoretic only) with `EchoLinear` and `EchoGraded` marked
    `Info (proxy)` since their usage/grade semantics approximate
    cost-tracking without committing to an algorithmic
    interpretation.
  * The "Open: new axes" section in taxonomy.md has a history note
    explaining the promotion.
  * roadmap.md marks axis 8 [landed] and its immediate-ordering
    item now reads "pick one axis-8 refinement and formalise it".

No code is changed. Theory-only update.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

Author: claude

docs/echo-types/examples.md

@@ -152,13 +152,13 @@ Template used for every entry:
   enormous but enumerable (in principle) set.
 - **Extensional / intensional.** Intensional at the set-theoretic
   level (every preimage exists), but the security claim is about
-  *computational* access to the echo, not its existence. This
-  distinction is not captured by the current `Echo f y` definition
-  and is a genuine open question: what refinement of Echo Types
-  encodes computational vs information-theoretic residue?
-- **Informal.** Not in repo. Serves as the worked example for the
-  **computational-access axis** that the current taxonomy does not
-  yet include.
+  *computational* access to the echo, not its existence.
+- **Informal.** Not in repo. This is the example that forced the
+  promotion of the information-theoretic/computational access
+  axis — see `taxonomy.md` axis 8. Candidate refinements of `Echo`
+  that would capture the security claim (cost-indexed echo, graded
+  access modality, decidability-respecting echo, witness-search
+  abstract machine) are listed there.
 
 ---
 

docs/echo-types/roadmap.md

@@ -21,9 +21,11 @@ Paths marked **[unblocked]** can proceed today. Paths marked
 - **[unblocked]** Axis 2 (approximate echoes): settle the formal
   definition before touching Agda. Draft in `taxonomy.md` and
   `composition.md`.
-- **[unblocked]** Axis 8 (computational-access): new taxonomy axis
-  motivated by the cryptographic-hash example (examples §8). Write
-  up separately.
+- **[landed]** Axis 8 (information-theoretic vs computational
+  access): promoted from the candidates list to a numbered axis;
+  four candidate refinements of `Echo` (cost-indexed, graded access
+  modality, decidability-respecting, witness-search abstract
+  machine) are listed. Follow-up: pick one refinement and formalise.
 - **[unblocked]** Negative / co-echoes: formulate `CoEcho(f)` and its
   relationship to `Echo(f)`. Possibly resolves the quantitative /
   structural tension hinted at by `EchoTropical`.
@@ -137,15 +139,18 @@ tractable today:
    Concrete, compiling, unblocks the composition roadmap.
 3. **Gate 1 adjacency refresh against the new taxonomy** — 1 day.
    Cheap coherence pass on existing docs.
-4. **Theory: write up computational-access axis** — 1 day.
-   Fills a gap that the current taxonomy cannot capture.
+4. **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.
 5. **Agda: `EchoApprox.agda`** — 2–3 days. First artifact of axis 2.
 6. **Applications chapter: compiler-analysis residue** — 2 days.
    Largest reader value; entirely unblocked.
 7. **Per-decoration composition lemmas** — 1 day each. Useful
    coverage.
 
-Steps 1–4 are ~4–5 days of honest work that require nothing from
+Steps 1–4 are ~5–6 days of honest work that require nothing from
 proof assistants, external repos, or the blocked Buchholz path.
 Steps 5–7 extend into Agda but depend only on infrastructure we
 already have in-suite.

docs/echo-types/taxonomy.md

@@ -176,33 +176,130 @@ is load-bearing there.
 
 ---
 
+## Axis 8 — Information-theoretic vs computational access
+
+*Definition.* An echo is **information-theoretically accessible**
+when `Echo f y` is merely *inhabited* as a type — i.e. a witness
+`(x , p : f x ≡ y)` exists in the metatheory. An echo is
+**computationally accessible** when a concrete procedure produces
+such a witness in bounded resources given `y`. Information-theoretic
+accessibility is a property of the type; computational accessibility
+is a property of an accompanying algorithm.
+
+*Distinguishing test.* Does the echo's usefulness collapse when we
+restrict to witness-extraction algorithms of a fixed complexity
+class?
+
+*Example forcing the distinction.*
+- `H : {0,1}* → {0,1}ⁿ`, a cryptographically strong hash function.
+  `Echo H y` is information-theoretically inhabited for every `y ∈
+  image(H)` (pigeonhole — there exist preimages), but computationally
+  inaccessible under the standard security assumption (no
+  polynomial-time algorithm produces a witness). See `examples.md` §8.
+- `square⁻¹ : ℕ → ℕ` under the constructive square-root algorithm.
+  Same information content as `Echo square`, but the witness is
+  produced in `O(log n)` operations. Computationally accessible.
+
+*Why it is a separate axis.* Axes 1–7 are properties of the echo
+type as a mathematical object — they do not depend on any notion of
+cost, algorithm, or resource. Axis 8 does. Two echoes can be
+identical on every other axis (same extensional shadow, same
+intensional core, same proof relevance, etc.) and differ only in
+whether a witness is reachable by a feasible algorithm. The security
+of every modern cryptosystem depends on this axis being real.
+
+*Agda anchor.* None directly — Agda's type system does not express
+complexity bounds, so computational access cannot be named at the
+type level in the current formalisation. Adjacent machinery in
+stdlib:
+- `Data.Nat.Logarithm.⌊log₂⌋` and arithmetic complexity conventions
+  admit informal-level statements like "this function runs in `O(n
+  log n)`", but without a cost monad.
+- `EchoLinear.agda` and `EchoGraded.agda` restrict what one can *do*
+  with witnesses via usage modes and grades. These are proxies for
+  resource control, not full computational-access tracking.
+
+*Candidate refinements of `Echo` that would capture this axis.*
+
+1. **Cost-indexed echo.** Pair `Echo f y` with a witness-extraction
+   bound: `CEcho f y cost = Σ (Echo f y) (λ _ → Extractor f y cost)`.
+   Requires a resource monad or a cost-passing semantics.
+
+2. **Graded access modality.** `Echo^c f y` at grade `c` means
+   "witness is reachable with `≤ c` steps". A graded semiring on the
+   cost indexes gives composition. `EchoGraded.agda` is the natural
+   host; the grade would need a complexity-class interpretation
+   (e.g. polynomial vs super-polynomial).
+
+3. **Decidability-respecting echo.** `Echo⁺ f y = Dec (Echo f y)`
+   pairs the echo with a *constructive decision procedure*. Weaker
+   than full cost-tracking but enough to distinguish "feasibly
+   decidable" from "mathematically inhabited".
+
+4. **Witness-search abstract machine.** Model the extractor as a
+   term in a bounded-step abstract machine and pair it with the
+   echo. Heavier; more faithful to actual cryptographic modelling.
+
+*Open question.* Is there a single refinement that subsumes all four?
+My guess is no: (1) and (4) track asymptotic cost, (2) and (3)
+track discrete feasibility classes. They probably live on a small
+lattice of access-tracking theories.
+
+*Composition conjecture.* Computational accessibility composes
+**multiplicatively** along `g ∘ f` in the canonical case — the
+cost of extracting a `g ∘ f` witness is bounded by the product of
+component costs. This is the standard complexity composition and
+should carry over; would need to be stated carefully since the
+accumulation iso of `composition.md` §1 introduces an intermediate
+`b : B` whose extraction cost is implicit.
+
+*Worked example motivating the axis.* Hash chains in a blockchain.
+Each block's header is a pre-image echo over the previous block's
+hash. Information-theoretically, the entire chain's residue structure
+is determined by any final hash value. Computationally, reconstructing
+earlier blocks from the final hash alone is infeasible — precisely
+the property that makes the chain tamper-evident. The current Echo
+Types framework cannot name this distinction as a type-level fact.
+
+---
+
 ## Cross-classification table
 
 A first cut at placing existing modules on the axes. Entries marked
 `?` are not yet pinned down. Entries marked `·` are not applicable.
-
-| Module | Ext/Int | Exact/Approx | Local/Global | Canonical | Compositional | Static/Dynamic | Proof-rel |
-|---|---|---|---|---|---|---|---|
-| `Echo` | Int | Exact | Global | Canon | Expected | Static | Yes |
-| `EchoCharacteristic` | Both | Exact | Local | Canon | ? | Static | Yes |
-| `EchoResidue` | Int→Shadow map | Exact | Global | Canon | ? | Static | Yes |
-| `EchoIndexed` | Int | Exact | Global | Pres-dep by role | ? | Static | Yes |
-| `EchoChoreo` | Int | Exact | Local | Pres-dep | ? | Dynamic | Yes |
-| `EchoEpistemic` | Int | Exact | Global | Pres-dep by agent | ? | ? | Yes |
-| `EchoLinear` | Int | Exact | Global | Canon | ? | Static | Yes |
-| `EchoGraded` | Int | Exact | Global | Canon | Expected | Static | Yes |
-| `EchoTropical` | Int | Approx-ish | Local | Pres-dep | ? | Static | Yes |
-| `EchoOrdinal` | Int | Exact | Local | Canon | ? | Static | Yes |
+The access column uses `Info` for information-theoretic only (typical
+for a theorem-prover module with no resource semantics) and is the
+uniform default at this stage — no module currently models
+computational access as a first-class property.
+
+| Module | Ext/Int | Exact/Approx | Local/Global | Canonical | Compositional | Static/Dynamic | Proof-rel | Access |
+|---|---|---|---|---|---|---|---|---|
+| `Echo` | Int | Exact | Global | Canon | Expected | Static | Yes | Info |
+| `EchoCharacteristic` | Both | Exact | Local | Canon | ? | Static | Yes | Info |
+| `EchoResidue` | Int→Shadow map | Exact | Global | Canon | ? | Static | Yes | Info |
+| `EchoIndexed` | Int | Exact | Global | Pres-dep by role | ? | Static | Yes | Info |
+| `EchoChoreo` | Int | Exact | Local | Pres-dep | ? | Dynamic | Yes | Info |
+| `EchoEpistemic` | Int | Exact | Global | Pres-dep by agent | ? | ? | Yes | Info |
+| `EchoLinear` | Int | Exact | Global | Canon | ? | Static | Yes | Info (proxy) |
+| `EchoGraded` | Int | Exact | Global | Canon | Expected | Static | Yes | Info (proxy) |
+| `EchoTropical` | Int | Approx-ish | Local | Pres-dep | ? | Static | Yes | Info |
+| `EchoOrdinal` | Int | Exact | Local | Canon | ? | Static | Yes | Info |
 
 Multiple `?` entries are open research: the compositional behaviour
 of the choreographic, epistemic, and tropical echoes has not been
 systematically checked and may turn out to differ from the clean
-composition law for the base `Echo`.
+composition law for the base `Echo`. The `Info (proxy)` marks on
+`EchoLinear` and `EchoGraded` indicate modules whose usage modes and
+grade semirings *approximate* cost-tracking at the access axis but
+do not commit to an algorithmic-cost interpretation.
 
 ---
 
 ## Open: new axes worth considering
 
+Axes listed here have distinguishing examples but have not been
+developed far enough to promote to a numbered axis.
+
 - **Reversibility axis.** Does `f` admit a section? Partial section?
   No section? The shape of `Echo(f)` changes sharply across these.
   Evidence: `no-section-collapse` in `EchoCharacteristic.agda`.
@@ -213,3 +310,9 @@ composition law for the base `Echo`.
   types may themselves form a category with interesting properties
   (e.g. all morphisms factor through a residue). Currently indirect
   in `EchoCategorical.agda`; worth an explicit axis once developed.
+
+*History note.* Axis 8 (information-theoretic vs computational
+access) was promoted from this list on the same commit that added
+it as a numbered axis. The cryptographic-hash example in
+`examples.md` §8 was the case that forced the promotion: no other
+axis could distinguish "preimage exists" from "preimage is findable".