Characterize sound partial recovery through decidable Echo fibres

.machine_readable/descriptiles/AGENTIC.a2ml

@@ -7,7 +7,7 @@ repository = "hyperpolymath/epistemic-types"
 author = "Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>"
 version = "0.1.0"
 status = "prototype"
-last-updated = "2026-11-01"
+last-updated = "2026-11-07"
 
 [agent-permissions]
 can-edit-source = true        # Agda modules under src/EpistemicTypes/
@@ -57,10 +57,10 @@ release-claim-requires-hard-pass = true
 [verification]
 # The single source of truth for "does it hold".
 command = "just check"
-underlying = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+underlying = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh && bash tests/check-approval-seal-mutations.sh"
 agda-version = "2.6.4.3"
 entrypoint = "scripts/check.sh (recursive source gate; All.agda is the aggregate module)"
-expected = "22 source modules accepted, 13 intended rejections, strict profile/import/escape-hatch policy and planted-postulate control pass"
+expected = "25 source modules accepted, 19 intended rejections, strict profile/import/escape-hatch policy and planted-postulate control pass"
 
 [automation-hooks]
 # on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml.

.machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -5,7 +5,7 @@ project = "epistemic-types"
 ecosystem = "hyperpolymath"
 version = "0.1.0"
 status = "prototype"
-last-updated = "2026-11-01"
+last-updated = "2026-11-07"
 
 [position]
 type = "formal-methods-library"
@@ -17,7 +17,7 @@ options = "--safe --without-K --cubical-compatible; source also declares --exact
 libraries = "core: none — --no-libraries against Agda.Builtin.*, Agda.Primitive and local modules; optional CanonicalEcho integration has pinned external source/stdlib"
 machine-readable = "a2ml + Nickel/k9"
 docs = "AsciiDoc"
-check = "just check == policy inventory/negative control + all 22 source modules + all 13 expected rejections"
+check = "just check == policy inventory/negative control + all 25 source modules + all 19 expected rejections"
 notes = "Single-tool Agda library. The core has no runtime dependencies; CI uses a pinned Debian verification container."
 
 [core]
@@ -28,6 +28,7 @@ modules = [
   "EpistemicTypes.Warrant — Warrant / Epi / SoundWarrant",
   "EpistemicTypes.Access — Preorder + AccessibleModality transport 'increase'",
   "EpistemicTypes.EchoBridge — certified residue and separately measured bounds 'Echo C y', kept distinct from E κ A",
+  "EpistemicTypes.PartialRecovery / PartialRecoveryExamples — pair-only partial recovery, separate success soundness, explicit image decision, fallback totalization and finite boundary controls",
   "EpistemicTypes.SurrealBridge — SurrealAccess carrier + GradedSurrealModality + daySurrealAccess finite birthday tower",
   "EpistemicTypes.Examples",
   "EpistemicTypes.ProofTransport — standpoint-indexed proof transport across trust boundaries",

.machine_readable/descriptiles/PLAYBOOK.a2ml

@@ -5,7 +5,7 @@
 [metadata]
 version = "0.1.0"
 status = "prototype"
-last-updated = "2026-11-01"
+last-updated = "2026-11-07"
 repo = "hyperpolymath/epistemic-types"
 single-tool = "agda"
 
@@ -18,7 +18,7 @@ ci = "Proof and security CI enabled; see docs/ci-safety.adoc"
 [gate]
 # The single source of truth for 'is the library healthy?'.
 command = "just check"
-expands-to = "tests/check-policy.sh; tests/check-proofs.sh over all 22 source modules; tests/check-rejections.sh over all 13 fixtures"
+expands-to = "tests/check-policy.sh; tests/check-proofs.sh over all 25 source modules; tests/check-rejections.sh over all 19 fixtures; tests/check-approval-seal-mutations.sh over four fixed mutants"
 agda-version = "2.6.4.3"
 options = "--safe --without-K --cubical-compatible; source hardening --exact-split --no-sized-types --no-guardedness"
 dependencies = "core: Agda builtins/primitive and local modules only; optional canonical integration pins Echo source and stdlib"

.machine_readable/descriptiles/STATE.a2ml

@@ -1,7 +1,7 @@
 [metadata]
 project = "epistemic-types"
 version = "0.1.0"
-last-updated = "2026-11-01"
+last-updated = "2026-11-07"
 status = "prototype"  # prototype | active | paused | archived
 
 [project-context]
@@ -26,17 +26,18 @@ secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the sta
 checker = "Agda 2.6.4.3 (CI-matched)"
 command = "just check"
 entry-point = "scripts/check.sh — local agda when present, else 'guix shell -D -f build/guix.scm -- bash scripts/check.sh'"
-expands-to = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+expands-to = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh && bash tests/check-approval-seal-mutations.sh"
 dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'"
 ci-entry-point = ".github/workflows/agda.yml asserts 'Agda version 2.6.4.3', then runs 'bash scripts/check.sh'"
 warning-policy = "-W error with only noUnsupportedIndexedMatch disabled: locally for Kripke.Belief's indexed relation elimination and at the pinned external integration boundary. No Cubical transport computation is claimed for those functions."
-proof-status = "AGDA-VERIFIED; Mathesis Grade 3. Proof Safety run 41326349568 passed both core/rejection/policy and pinned integration jobs at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Rocq/Lean/bridge legs remain open."
+proof-status = "AGDA-VERIFIED; historical hosted receipt below, new local partial-recovery receipt in docs/partial-recovery.adoc. Proof Safety run 41326349568 passed both core/rejection/policy and pinned integration jobs at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Rocq/Lean/bridge legs remain open."
 aggregator = "src/EpistemicTypes/All.agda imports the full source graph; the recursive gate separately checks every source file, including modules not publicly re-exported."
 
 [modules]
 # Agda modules under src/EpistemicTypes/.
 list = [
   "EpistemicTypes.Access",
+  "EpistemicTypes.Applications.ApprovalSeal",
   "EpistemicTypes.Applications.IntegerModel",
   "EpistemicTypes.Applications.OrderedGroup",
   "EpistemicTypes.Applications.QCriterion",
@@ -53,6 +54,8 @@ list = [
   "EpistemicTypes.Kripke.Frame",
   "EpistemicTypes.Kripke.Indexed",
   "EpistemicTypes.Kripke.Residual",
+  "EpistemicTypes.PartialRecovery",
+  "EpistemicTypes.PartialRecoveryExamples",
   "EpistemicTypes.ProofTransport",
   "EpistemicTypes.ProofTransportExample",
   "EpistemicTypes.ReadConsistency",
@@ -65,6 +68,7 @@ base = "Modality / LawfulModality / FactiveModality / BeliefModality / ReturnMod
 warrant = "Warrant / Epi / SoundWarrant."
 access = "Preorder + AccessibleModality transport 'increase'."
 echo-bridge = "Certified residue Echo C y, explicit source compatibility, recovery/migration laws and measured resource bounds; distinct from E κ A."
+partial-recovery = "Pair-only partial recovery; success soundness is separate. Sound partial recovery and separation plus explicit image decision construct each other. A chosen source fallback totalizes partial recovery; empty/collision/off-image controls and actual canonical Echo-fibre adapter are checked. See docs/partial-recovery.adoc for local receipt and sibling proposals."
 surreal-bridge = "SurrealAccess carrier + GradedSurrealModality + daySurrealAccess finite birthday tower."
 examples = "Worked instances exercising the interfaces."
 proof-transport = "proofSound derives Meaning holder artifact claim from an accepted sound checker. Receipts alone do not certify; transfer requires the target-holder meaning."
@@ -106,7 +110,7 @@ items = [
 ]
 
 [progress-summary]
-note = "Prototype. Authoritative inventory: 22 source modules and 13 expected-rejection fixtures. The map-only core, explicit warrant/factivity boundary, proof transport, store consistency, certified Echo residue with separate measured bounds, finite-day surreal adapter, RapidNJ integer certificate, and scoped constructive Kripke semantics are implemented. The 2026-11-01 canonical profile is --safe --without-K --cubical-compatible; hosted receipt status and Mathesis grade are in PROOF-STATUS.adoc. Open work includes data-dependent warrant soundness, residual owning-record correspondence, lawful instances, rational/rescaling and update obligations, independent Rocq/Lean legs, and runtime refinement."
+note = "Prototype. Authoritative inventory: 25 source modules and 19 expected-rejection fixtures. The map-only core, explicit warrant/factivity boundary, proof transport, store consistency, certified Echo residue with separate measured bounds, finite-day surreal adapter, RapidNJ integer certificate, and scoped constructive Kripke semantics are implemented. The 2026-11-01 canonical profile is --safe --without-K --cubical-compatible; hosted/local receipts and the proof-weight grading boundary are in PROOF-STATUS.adoc. Open work includes data-dependent warrant soundness, residual owning-record correspondence, lawful instances, rational/rescaling and update obligations, independent Rocq/Lean legs, and runtime refinement."
 
 [blockers-and-issues]
 # No active blockers.

0-AI-MANIFEST.a2ml

@@ -4,7 +4,7 @@ title = "epistemic-types — universal AI agent entry point"
 version = "0.1.0"
 format = "a2ml"
 status = "prototype"
-last-updated = "2026-11-01"
+last-updated = "2026-11-07"
 
 [project]
 name = "epistemic-types"
@@ -36,12 +36,12 @@ format = "AsciiDoc (.adoc) is the default. README.adoc is the overview, explainm
 machine-readable-location = "Project specifications live under .machine_readable/. The root 0-AI-MANIFEST.a2ml universal pointer and coordination.k9 session entry point are the explicit operational exceptions."
 license = "MPL-2.0"
 build = "just check"
-build-expansion = "bash scripts/check.sh → policy gate + all 22 source modules + all 13 expected rejections"
+build-expansion = "bash scripts/check.sh → policy gate + all 25 source modules + all 19 expected rejections + four approval-seal mutation controls"
 agda-options = "--safe --without-K --cubical-compatible plus source hardening --exact-split --no-sized-types --no-guardedness; -W error with UnsupportedIndexedMatch disabled only alongside an exact 23-source-span audit; no postulates; core imports only builtins/primitive/local modules"
 agda-version = "2.6.4.3"
 echo-distinction = "Do not collapse Echo C y and E κ A. Echo retains certified residues; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality."
 ci = "Proof and security workflows configured; required merge checks are described in docs/ci-safety.adoc"
-proof-status = "AGDA-VERIFIED; Mathesis Grade 3. Canonical Proof Safety receipt 41326349568 at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Independent Rocq/Lean/bridge legs remain open."
+proof-status = "AGDA-VERIFIED; historical hosted receipt below, new local partial-recovery receipt in docs/partial-recovery.adoc. Canonical Proof Safety receipt 41326349568 at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Independent Rocq/Lean/bridge legs remain open."
 secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone production home (D153/D154). Do not add a Secret API, IFC implementation or confidentiality theorem here. #29 stays closed; #32 closed on 2026-10-05 with no transfer and must not be reopened/duplicated (guard #39). Source-reviewed at standalone f581f8295bdee854f76291ab884a16cc8114dc6f on 2026-11-01: generic TINI and its two-point instance are PROVEN; termination-sensitive noninterference and declassification remain OPEN. No theorem is imported here."
 
 [first-run]
@@ -55,6 +55,7 @@ aggregator = "src/EpistemicTypes/All.agda"
 modules = [
   "EpistemicTypes.Access",
   "EpistemicTypes.All",
+  "EpistemicTypes.Applications.ApprovalSeal",
   "EpistemicTypes.Applications.IntegerModel",
   "EpistemicTypes.Applications.OrderedGroup",
   "EpistemicTypes.Applications.QCriterion",
@@ -70,6 +71,8 @@ modules = [
   "EpistemicTypes.Kripke.Frame",
   "EpistemicTypes.Kripke.Indexed",
   "EpistemicTypes.Kripke.Residual",
+  "EpistemicTypes.PartialRecovery",
+  "EpistemicTypes.PartialRecoveryExamples",
   "EpistemicTypes.ProofTransport",
   "EpistemicTypes.ProofTransportExample",
   "EpistemicTypes.ReadConsistency",
@@ -82,6 +85,7 @@ Base = "Modality / LawfulModality / FactiveModality / BeliefModality / ReturnMod
 Warrant = "Warrant / Epi / SoundWarrant — explicit warrant objects."
 Access = "Preorder plus AccessibleModality transport ('increase') across the access preorder."
 EchoBridge = "Certified Echo C y residues, explicit migration/recovery and separately measured resource bounds."
+PartialRecovery = "Pair-only Maybe decoder, separate success soundness, constructive image-decision characterization, explicit fallback totalization and finite boundary controls; see docs/partial-recovery.adoc."
 SurrealBridge = "SurrealAccess carrier plus GradedSurrealModality plus daySurrealAccess finite-birthday tower."
 Examples = "Worked instances of the abstract interfaces."
 ProofTransport = "Standpoint-indexed proof transport across trust boundaries."
@@ -112,7 +116,7 @@ step-3 = "Read .machine_readable/descriptiles/META.a2ml for architecture and des
 step-4 = "Read .machine_readable/descriptiles/ECOSYSTEM.a2ml for ecosystem position and sibling repos."
 step-5 = "Read .machine_readable/descriptiles/AGENTIC.a2ml, NEUROSYM.a2ml, and PLAYBOOK.a2ml for agent guidance."
 step-6 = "Read README.adoc and explainme.adoc for the human-facing overview."
-step-7 = "Run 'just check' (→ scripts/check.sh: local Agda or Guix/dev container) to enforce policy, check all 22 source modules and validate all 13 expected rejections before and after changes."
+step-7 = "Run 'just check' (→ scripts/check.sh: local Agda or Guix/dev container) to enforce policy, check all 25 source modules and validate all 19 expected rejections plus four mutation controls before and after changes."
 
 [policy]
 rules = [

PROOF-NEEDS.adoc

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = epistemic-types — proof needs
-:revdate: 2026-11-04
+:revdate: 2026-11-07
 :toc:
 
 This queue records only obligations that remain relevant to this repository.
@@ -27,8 +27,11 @@ planted-postulate negative control | CLOSED — run `41326349568`
 | CLOSED — run `41326349568`
 |===
 
-Closing P0 establishes Mathesis Grade 3 for the checked Agda revision. It does
-not establish independent cross-prover agreement.
+The P0 receipts establish `AGDA-VERIFIED` for their checked revisions, not
+independent cross-prover agreement. The earlier "Mathesis Grade 3" label is
+distinct from the canonical PWG vocabulary; see the policy clarification in
+link:PROOF-STATUS.adoc[]. The new partial-recovery local receipt is separate
+from these historical hosted runs.
 
 == P1 — theorem-level independent rechecks
 
@@ -50,8 +53,14 @@ modality, totality, and assumption translations | BRIDGE-PENDING
 than weakening the Agda statement | OPEN
 |===
 
-No Grade 2i, Grade 2ii, Grade 1, or `RECONCILED` claim is made until the
-applicable rows close.
+No independent prover or `RECONCILED` claim is made until the applicable rows
+close. For a bounded next translation, PR-1/PR-2/C-4 in the proof ledger now
+identify the partial-recovery statements: `Set` carriers, builtin intensional
+equality, untruncated Sigma fibres, pair-only Maybe decoding, separate success
+soundness, an explicit image decision and an explicit fallback source where
+used. The checked source and full assumptions are in
+link:docs/partial-recovery.adoc[]. Translating those exact statements and
+comparing their propositions in Rocq/Lean remains OPEN.
 
 == P2 — local mathematical obligations