feat+docs: Lane 5 Walkthrough 3 (provenance / debugging) — layer-1 section + layer-2 no-section contrast

Lane 5 Walkthrough 3 lands; the originally-scaffolded Lane 5 triplet
(region-exit audit, epistemic erasure, provenance / debugging) is now
complete in Agda.

Domain: 4-element `State` with two orthogonal sign bits. Visible
output `firstSign : State → Bool`; class predicate
`secondSign : State → Bool` is injective within each firstSign-fibre.
Three residue layers walked: full echo (Layer 0), class residue with
secondSign (Layer 1), trivial residue (Layer 2).

Headlines (all pinned in tutorial/provenance_debugging/Smoke.agda):

* `states-distinct-at-true` — Layer 0 distinguishes pp vs pn at the
  same visible output.
* `classes-remain-distinct` — Layer 1 still distinguishes them.
* `recover-section-at-layer-1` (POSITIVE) — Layer 1 has a section;
  `recover-from-class` is a right inverse of `state-to-class`.
* `trivials-collapse` — Layer 2 collapses the two echoes.
* `no-recovery-from-trivial` (NEGATIVE) — Layer 2 has no section;
  structural mirror of EchoResidue.no-section-collapse-to-residue.
* `provenance-walk-contrast` — section / no-section pair as a Σ.

New pedagogical shape: W1 and W2 each ship a one-sided no-section;
W3 ships BOTH a section (Layer 1) and its absence (Layer 2),
exhibiting the boundary at which type-level recovery flips. The
mechanical load is that secondSign is injective within each fibre.

Honest-bound + matched-negative discipline inherited from W2 — Agda
file and README both open with the type-level disclosure (NOT a
runtime debugger), `NotProved-*` block at the file's bottom catalogues
out-of-scope properties.

Build invariant held: All.agda + Smoke.agda + tutorial/All.agda +
tutorial/provenance_debugging/Smoke.agda all exit 0 under
--safe --without-K, zero postulates, no funext.

Files:
* tutorial/provenance_debugging/ProvenanceDebugging.agda (worked example)
* tutorial/provenance_debugging/Smoke.agda (headline pins)
* tutorial/provenance_debugging/All.agda (aggregator)
* tutorial/provenance_debugging/README.adoc (narrative)
* tutorial/All.agda — registers W3
* tutorial/README.adoc — W3 flipped from design-doc to LANDED
* CLAUDE.md — Session arc 2026-05-27 entry

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

Author: hyperpolymath

CLAUDE.md

@@ -191,7 +191,95 @@ 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-20 daytime (theory closure waves 1 + 2 + 3)
 

tutorial/All.agda

@@ -4,11 +4,11 @@
 -- Tutorial-track aggregator. Mirrors `proofs/agda/All.agda` for the
 -- Lane 5 walkthrough track.
 --
--- Walkthroughs 1 (`tutorial.region_exit_audit`) and 2
--- (`tutorial.epistemic_erasure`) are currently realised in Agda.
--- Walkthrough 3 (provenance / debugging) remains at scaffold/
--- design-doc level per `tutorial/README.adoc` — it should be
--- registered here when it lands.
+-- Walkthroughs 1 (`tutorial.region_exit_audit`), 2
+-- (`tutorial.epistemic_erasure`), and 3
+-- (`tutorial.provenance_debugging`) are all realised in Agda as of
+-- 2026-05-27. The originally-scaffolded triplet from
+-- `tutorial/README.adoc` is complete.
 --
 -- Build:
 --   agda --library-file=/tmp/agda-libs -i . -i proofs/agda \
@@ -19,3 +19,4 @@ module tutorial.All where
 
 import tutorial.region_exit_audit.All
 import tutorial.epistemic_erasure.All
+import tutorial.provenance_debugging.All

tutorial/README.adoc

@@ -13,15 +13,18 @@ rather than re-deriving the pedagogy.
 
 [IMPORTANT]
 ====
-*Lane 5 unpark status (updated 2026-05-27).* Walkthroughs 1
-(certified region-exit audit) and 2 (epistemic erasure with honest
-bound) are LANDED. Walkthrough 1 was accepted as the killer-app
+*Lane 5 unpark status (updated 2026-05-27, evening).* Walkthroughs
+1 (certified region-exit audit), 2 (epistemic erasure with honest
+bound), and 3 (provenance / debugging with layer-1 section + layer-2
+no-section) are all LANDED. The originally-scaffolded triplet is
+complete in Agda. Walkthrough 1 was accepted as the killer-app
 candidate per `roadmap.adoc` §"Lane 5 [PARKED]" second unblocking
 condition. Walkthrough 2 followed as the second realisation,
 addressing the "does echo-types prove key zeroing?" category-error
-question. Walkthrough 3 (provenance / debugging) remains at
-scaffold/design-doc level pending either Lane 1 close-out or
-independent unparking decisions.
+question. Walkthrough 3 lands the dual: a *positive* recovery
+result at layer 1 paired with the negative at layer 2, making
+explicit which residue layer carries the load-bearing information
+for source reconstruction in a small fixed domain.
 
 The Smoke gate (`proofs/agda/Smoke.agda`), the top-level
 `proofs/agda/All.agda`, and the identity-claim gates still do not
@@ -135,34 +138,54 @@ write-up of echo for an applied audience."
 
 === Walkthrough 3: provenance / debugging echo
 
-*Status.* Design-doc only. Agda lands at unpark time.
-
-*The pedagogy.* Model a small state-reconstruction example: an
-agent observes a single Boolean output `b : Bool` from an opaque
-computation `f : State → Bool` on a 4-element `State`. `Echo f b`
-retains the source state; iterated `degrade` operations
-(`keep → residue → forget` per `EchoResidue`) walk a debugger
-through what information is available at each provenance level.
-The walkthrough closes by exhibiting how the residue-level
-`collapse-via-residue` lemma supports a class-level claim ("the
-state was in the 'sign-positive' class") even when the full state
-is no longer recoverable.
+*Status.* LANDED 2026-05-27. See
+`tutorial/provenance_debugging/ProvenanceDebugging.agda` for the
+worked example and `tutorial/provenance_debugging/README.adoc` for
+the narrative.
+
+*The pedagogy.* A 4-element `State` with two orthogonal sign bits.
+The visible output of the echo is the first sign (`firstSign :
+State → Bool`); the residue carrier at layer 1 is the second sign
+(`secondSign : State → Bool`). The walkthrough walks the source
+through three layers — full echo, class residue, trivial residue
+— and exhibits the load-bearing contrast: at layer 1 a *section
+exists* (`recover-from-class` is a right inverse of
+`state-to-class`); at layer 2 *no section exists*
+(`no-recovery-from-trivial`, mirroring the structural argument of
+`EchoResidue.no-section-collapse-to-residue`). The pair is
+packaged as `provenance-walk-contrast`. The mechanical content:
+`secondSign` is injective within each `firstSign`-fibre, which is
+exactly the property that makes the layer-1 recovery work.
+
+*The crucial honest disclosure.* This walkthrough is *not* a
+runtime debugger. It is a *type-level* statement about which
+residue layer carries the load-bearing information for source
+reconstruction in a fixed 4-element domain. Conflating it with
+operational debugging is a category error — exactly the kind of
+mistake the project's retraction discipline
+(`docs/retractions.adoc`) exists to prevent. The walkthrough opens
+with the disclosure, then states the actual claims (layer-1
+section + layer-2 no-section), then walks the proofs.
 
 *Files when landed.*
 
-* `tutorial/provenance_debugging/README.adoc` — narrative.
+* `tutorial/provenance_debugging/README.adoc` — narrative with the
+  bound disclosure as the *opening* sentence, not a footnote.
 * `tutorial/provenance_debugging/ProvenanceDebugging.agda` — the
-  worked example, building on `EchoExampleProvenance.agda`.
+  worked example, building on `EchoExampleProvenance.agda` +
+  `EchoResidue.agda`.
 * `tutorial/provenance_debugging/Smoke.agda` — per-walkthrough
   Smoke pins.
+* `tutorial/provenance_debugging/All.agda` — walkthrough-local
+  aggregator, imported by `tutorial/All.agda`.
 
 *Why this walkthrough exists.* The two harder walkthroughs (audit,
-erasure) both ship as `LEcho affine` content where information is
-*not* recoverable. This third walkthrough exhibits the dual: where
-the iterated degradation makes some information unrecoverable but
-others survive (the residue layer). It is the gentlest of the
-three; readers who bounce off the audit and erasure walkthroughs
-land here.
+erasure) both ship as one-sided no-section content where
+information is *not* recoverable. This third walkthrough exhibits
+the dual: a positive recovery result paired with the negative,
+making explicit *which* residue layer is load-bearing for
+reconstruction. It is the gentlest of the three; readers who
+bounce off the audit and erasure walkthroughs land here.
 
 == Discipline that applies to all three walkthroughs
 

tutorial/provenance_debugging/All.agda

@@ -0,0 +1,10 @@
+{-# OPTIONS --safe --without-K #-}
+
+------------------------------------------------------------------------
+-- Aggregator for Lane 5 Walkthrough 3.
+------------------------------------------------------------------------
+
+module tutorial.provenance_debugging.All where
+
+import tutorial.provenance_debugging.ProvenanceDebugging
+import tutorial.provenance_debugging.Smoke