proofs: EchoSearchExample PWG-2ii (Agda receipt + Rocq and Lean legs, reconciled)

.github/workflows/agda.yml

@@ -115,3 +115,35 @@ jobs:
         run: bash scripts/setup-agda.sh
       - name: Typecheck isolated full-Cubical profile
         run: agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda
+
+  # PROOF-POLICY section 2 recheck legs for EchoSearchExample: hand
+  # re-proofs in Rocq and in Lean core (no Mathlib). Each fails on any axiom.
+  # Toolchains are version-asserted (Lean archive checksum-pinned); the
+  # section 6 deviation is recorded in proofs/RECHECK-EchoSearchExample.adoc.
+  rocq-recheck:
+    name: Rocq recheck leg
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - name: Install version-asserted Rocq (Coq 8.18.0)
+        run: bash scripts/setup-recheck.sh rocq
+      - name: Check the Rocq leg (no axioms)
+        run: bash scripts/check-recheck.sh rocq
+
+  lean-recheck:
+    name: Lean recheck leg
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - name: Install checksum-pinned Lean 4.30.0
+        run: bash scripts/setup-recheck.sh lean
+      - name: Check the Lean leg (no axioms)
+        run: bash scripts/check-recheck.sh lean

PROOF-STATUS.adoc

@@ -27,6 +27,56 @@ below. The ordinal lane, including its order-type *Fidelity* scaffold, moved to
 https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
 on 2026-10-20.
 
+== Proof Witness Grades (PROOF-POLICY §8)
+
+Grades are computed per theorem from receipts and §2.2 records. They are
+never assigned to the repository as a whole.
+
+[cols="2,1,4",options="header"]
+|===
+|Theorem |PWG |Record
+
+|`EchoSearchExample` headlines (`search-double-6-decided`, `search-as-echo`, `search-as-cost`, `search-as-dec`, `search-as-feasible`)
+|`PWG-2ii`, no axioms
+|link:proofs/RECHECK-EchoSearchExample.adoc[`proofs/RECHECK-EchoSearchExample.adoc`].
+The Agda receipt is the cold check at `ccec4d7` (2026-11-09). The Rocq and
+Lean legs are re-proved and kernel-checked with no axioms. They are
+`RECONCILED` by owner acceptance of the recorded statement comparison
+(2026-11-09). `PWG-1` additionally needs current pinned CI receipts for
+every witness.
+|===
+
+Census (PROOF-POLICY §8.4), counted per theorem on 2026-11-09 over the 722
+headline pins in the `using` clauses of `proofs/agda/Smoke.agda` (the pins
+include some definitions as well as theorems): `PWG-1` 0, `PWG-2ii` 5,
+`PWG-2i` 0, `PWG-3` 0, `ungraded` 717. The five graded theorems are the
+`EchoSearchExample` headlines above; every other pin is `ungraded` because no
+per-theorem record exists for it yet.
+Agda results for the whole closure are dated checks, not grades.
+
+== Agda cold check (2026-11-09)
+
+At source commit `ccec4d79866e3e433ae2268d2f8b7899396cb34f`, with a clean
+tree and the CI toolchain from `scripts/setup-agda.sh` (Agda 2.7.0.1;
+release archive sha256
+`975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a`; stdlib
+`8326c74`; absolute-zero `f486c29`), these all exited 0:
+
+* the five static guards (kernel, experimental aggregate wiring and
+  controls, invocation lint, foundation guardrail);
+* the seven `--safe --without-K --cubical-compatible` roots, cold
+  (`--ignore-interfaces`): `All`, `Smoke`, `AuditSmoke`,
+  `characteristic/All`, `examples/All`, `experimental/echo-additive/All`
+  and `NarrowingSmoke`;
+* the `--safe --cubical` island.
+
+The only warnings were the known `UnsupportedIndexedMatch` ones (triage
+remains open; see below). The log is
+`docs/receipts/agda-cold-2026-11-09.log.gz`; the uncompressed log has
+sha256 `7f9de4d1f874a0f249eadeb3fc675be346f437cb28cb31fd3e6db1b635e54eb0`.
+This is a local run of a clean commit with the pinned toolchain. It is not
+a GitHub Actions receipt.
+
 == CI coverage audit (2026-11-01)
 
 * `experimental/echo-additive/` has a separate aggregate entrypoint, but
@@ -43,7 +93,7 @@ on 2026-10-20.
   other three) in warm and cold jobs under the standard profile. A local
   cold check now succeeds as detailed below; the changed workflow has not
   yet had a successful CI run. The exhibit remains outside the shipped
-  `All.agda` closure and is not a clean-commit Grade 3 receipt.
+  `All.agda` closure and is not a clean-commit `PWG-3` receipt.
 * On 2026-11-01 the local cold checks and static guards passed with Agda
   `2.7.0.1-cf6e2d9` and stdlib v2.3. The compiler is not the latest
   upstream stable; CI's compiler remains unpinned (#322). Full provenance,
@@ -110,7 +160,7 @@ with an unsolved hole was rejected (exit 42); it is not a theorem check.
 * Complete combined stdout/stderr is preserved in
   `docs/receipts/agda-local-2026-11-01.log.gz` (uncompressed SHA-256
   `617263834bee297a9f8e092c32e7cd9934af940f1e9fa7f9e19663b44cde99ad`).
-  No new clean-commit Grade 3 promotion is asserted on this basis.
+  No new clean-commit `PWG-3` promotion is asserted on this basis.
 
 In separate copied proof trees, replacing `fin-injective refl = refl` in
 experimental `Grade` with a hole caused its aggregate to exit 42, while

docs/proof-witness-audit.adoc

@@ -1,6 +1,21 @@
 // SPDX-License-Identifier: MPL-2.0
 = Proof-witness audit: Echo Types and Mathesis
 
+[NOTE]
+====
+*Superseded scale (2026-11-09).* This dated audit uses the Mathesis brief's
+grade definitions. PROOF-POLICY §8, by owner ruling of 2026-11-04, now
+governs, and corrects the brief in two places:
+
+* `PWG-2ii` means both the Rocq leg and the Lean leg count. A non-DTT
+  witness is the tag `+foundation-diverse`, not a condition of the grade
+  (§8.3).
+* Every grade carries the `PWG-` prefix.
+
+The audit text below is kept as written. Current per-theorem grades are
+in `PROOF-STATUS.adoc` §"Proof Witness Grades".
+====
+
 Audit date: 2026-11-01. Echo Types source base:
 `b0982c44f36133acd2d0e1d4e03cf031fff7a470` (working tree also has
 uncommitted CI/documentation edits). This is a source and receipt inspection,

proofs/RECHECK-EchoSearchExample.adoc

@@ -0,0 +1,235 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= EchoSearchExample: Agda source, Rocq and Lean recheck legs
+:toc:
+
+This is the per-theorem record that PROOF-POLICY §2.2, §5 and §8.5 ask
+for (https://github.com/metadatastician/standards/blob/9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5/3-practice/PROOF-POLICY.adoc[standards@9bdf864]).
+It covers the headlines of `proofs/agda/EchoSearchExample.agda` (echo-types
+#353), a theory development: a worked axis-8 exhibit with no dependence on
+any one system's code. The Agda proof is the source of truth.
+
+[IMPORTANT]
+====
+*Grade: `PWG-2ii`, not rested on axioms.* The Agda source is `PROVEN`. Both
+recheck legs (Rocq and Lean) are kernel-checked as `PROVEN` with no axioms,
+and are `RECONCILED` (§2.2), so both legs count (§8.2).
+
+*How the legs were reconciled.* An agent wrote the statement comparison
+below. The owner accepted it on 2026-11-09 (echo-types#368), without a
+separate line-by-line review. Treat the comparison, the residual
+differences and the owner's acceptance together as the bridge record.
+
+`PWG-1` additionally needs current receipts from the pinned CI lanes
+(`check`, `cold-check`, `rocq-recheck`, `lean-recheck`) on the exact source
+commit for every witness. Those lanes run on pull requests, on pushes to
+`main` and `master`, and on manual dispatch; a push to any other branch with
+no open pull request produces no receipt.
+====
+
+== Ledger
+
+[cols="2,1,1,1,1,3",options="header"]
+|===
+|Leg |Route |§5 token |§2.2 state |Axioms |Receipt
+
+|Agda (source)
+|—
+|`PROVEN`
+|`AGDA-VERIFIED`
+|none
+|Cold check at echo-types `ccec4d79866e3e433ae2268d2f8b7899396cb34f`, 2026-11-09. See "Receipts".
+
+|Rocq
+|`re-proved`
+|`PROVEN`
+|`RECONCILED`
+|none (`Print Assumptions`: closed)
+|`proofs/rocq/EchoSearchExample.v`, Coq 8.18.0, 2026-11-09.
+
+|Lean 4
+|`re-proved`
+|`PROVEN`
+|`RECONCILED`
+|none (`#print axioms`: none)
+|`proofs/lean4/EchoSearchExample.lean`, Lean 4.30.0, 2026-11-09.
+|===
+
+Record (§8.5): `pwg: 2ii`, `foundation_diverse: false`. All three legs: `PROVEN`, with no axioms. Rocq and Lean: route `re-proved`, §2.2 `RECONCILED` (owner acceptance, 2026-11-09).
+
+*Why re-proved, not transported.* The policy prefers Dedukti transport
+(§2). No Agda→Dedukti→Rocq/Lean pipeline is set up in this repo. Separately,
+no released Lambdapi Lean exporter exists, so the Lean leg would be a
+re-proof in any case (§2). The theorems are small and concrete, so a hand
+re-proof against the same definitions is the direct route.
+
+== Statement correspondence
+
+The comparison was made by reading: each Rocq and Lean definition restates
+the Agda definition it mirrors, clause by clause.
+
+[cols="1,3,3,3",options="header"]
+|===
+|Headline |Agda |Rocq |Lean 4
+
+|`double`
+|`double zero = zero`; `double (suc n) = suc (suc (double n))`
+|same two clauses on `nat`
+|`double 0 = 0`; `double (n+1) = double n + 2` (= `succ (succ (double n))` by `Nat.add` unfolding)
+
+|`search-double-6`
+|`EchoS countUp double 6 4`, witness `(3 , s≤s⁴ z≤n , refl)`
+|`EchoS countUp double 6 4`, `existT _ 3 (le_n 4, eq_refl)`
+|`EchoS countUp double 6 4`, `⟨3, by decide, rfl⟩`
+
+|`search-double-6-decided`
+|`bounded-search-is-decidable _≟_ countUp double 6 4 ≡ yes search-double-6`, by `refl`
+|`bounded_search_is_decidable nat_eq_dec countUp double 6 4 = yes search_double_6`, by `reflexivity`
+|`boundedSearchIsDecidable Nat.decEq countUp double 6 4 = Dec.yes searchDouble6`, by `rfl`
+
+|`search-as-echo`
+|`Echo double 6`
+|`Echo double 6`
+|`Echo double 6`
+
+|`search-as-cost`
+|`EchoC search-steps 4 double 6` (`Cost stepCostAlgebra`)
+|`EchoC search_steps 4 double 6`
+|`EchoC searchSteps 4 double 6`
+
+|`search-as-dec`
+|`EchoDec double 6`
+|`EchoDec double 6`
+|`EchoDec double 6`
+
+|`search-as-feasible`
+|`CEcho feasible double 6`, by `degrade-access free≤feasible`
+|`CEcho feasible double 6`, by `degrade_access free_feasible`
+|`CEcho .feasible double 6`, by `degradeAccess .freeFeasible`
+|===
+
+The definitions behind them:
+
+* `Echo f y = Σ A (λ x → f x ≡ y)` (`Echo.agda`). Rocq writes it as
+  `{x : A & f x = y}` (`sigT`), Lean as `(x : A) ×' (f x = y)` (`PSigma`).
+* `EchoS enum f y n = Σ ℕ (λ k → (k < n) × (f (enum k) ≡ y))`
+  (`EchoSearch.agda`). Both targets use a proof-relevant Σ over `k` with the
+  same two components.
+* `bounded-search-is-decidable` recurses structurally on the budget, and its
+  successor step tests the new top index `n` first, then recurses. The
+  targets recurse the same way and in the same order, so the `decided`
+  equation computes to the same witness. The Agda comment notes this is one
+  comparison, not an ascending walk.
+* `EchoC` at `stepCostAlgebra = (ℕ, 0, _+_, _≤_, …)`: `Cost stepCostAlgebra`
+  unfolds to `Σ A (λ x → (f x ≡ y) × (cost x ≤ c))`. The targets restate
+  that instance directly, not the generic `CostAlgebra` record. The generic
+  record and its laws are not part of these headlines.
+* `search-steps = suc`; `count-up-search-to-cost` re-pairs, because `k < n` is
+  `suc k ≤ n` definitionally. This holds in all three systems: stdlib `_<_`;
+  Rocq `lt n m := S n <= m`; Lean `Nat.lt n m := Nat.le (n+1) m`.
+* `EchoDec f y = Dec (Echo f y)`; `search-to-dec s = yes (echo-search-forget s)`.
+* `CEcho`, `_≤a_` (15 Hasse pairs) and `degrade-access` are restated in full,
+  case for case.
+
+== Residual differences and assumptions
+
+These do not change what the headlines state about this example, but they
+are differences between the systems and are listed as the policy requires.
+
+. *Identity type.* Agda's `_≡_` is used under `--without-K`. Rocq's `eq` lives
+  in `Prop`, with no UIP axiom assumed. Lean's `Eq` lives in `Prop` with
+  definitional proof irrelevance, so K holds in Lean. Every proof here is a
+  closed computation (`refl` / `reflexivity` / `rfl`) or a re-pairing, so
+  none of them uses K. The Lean leg is still checked in a strictly stronger
+  theory.
+. *Order and decision types.* Agda's `_<_` is a data type in `Set`; in Rocq
+  and Lean it is a `Prop`. Agda's stdlib `Dec` is a record (`does`/`proof`);
+  the targets use a local `yes`/`no` inductive with the same two cases.
+  Decidable equality on ℕ is stdlib `_≟_` in Agda, a `decide equality` term
+  in Rocq, and `Nat.decEq` in Lean.
+. *Universes.* Agda is universe-polymorphic with `Lift` padding in `CEcho`.
+  Rocq uses `Type` with template polymorphism; Lean uses `Type u` with
+  `PUnit`. Both targets use the unit type where Agda uses `Lift (a ⊔ b) ⊤`.
+. *Scope.* The `CostAlgebra` laws (`≤-refl`, `≤-trans`, `+-identityˡ`,
+  `+-mono-≤`) are not restated, because no headline in this module depends
+  on them. They are Agda-only facts for this theorem.
+
+== Receipts
+
+*Agda (PWG-3 receipt).*
+
+* Source: echo-types `ccec4d79866e3e433ae2268d2f8b7899396cb34f`, clean tree.
+  `proofs/agda/EchoSearchExample.agda` sha256
+  `b73a9bb1fab531531f2442ea5f23cda74bd933e6e80e12e84986aa8ef716be33`.
+* Checker: Agda 2.7.0.1 from `scripts/setup-agda.sh`, release archive sha256
+  `975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a`.
+  Pins: stdlib `8326c7475af1fa456ca04a0203c168d5d7ff842b`, absolute-zero
+  `f486c29903434589117fa0662c6f29b0f17d1d5f`.
+* Invocation: `agda --no-libraries -i $AGDA_STDLIB -i $ABSOLUTE_ZERO_AGDA
+  --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda
+  proofs/agda/All.agda`. That is the §2.1 profile, cold; `All` imports
+  `EchoSearchExample`.
+* The same run also checked `Smoke`, `AuditSmoke`, `characteristic/All`,
+  `examples/All`, `experimental/echo-additive/All`, `NarrowingSmoke`, the
+  `--safe --cubical` island and the five static guards. All exited 0.
+* Import cone (§1.1): first-party `EchoSearchExample`, `Echo`, `EchoCost`,
+  `EchoDecidable`, `EchoAccess`, `EchoSearch`, plus the pinned stdlib.
+  Compiled under `--safe`, which refuses `postulate`. A comment-aware scan of
+  the first-party cone finds zero postulates. Postulate count: 0.
+* Warnings: `UnsupportedIndexedMatch` (Cubical computation on transports)
+  appears in the cone, including `EchoSearch.agda` lines 192–204 (the
+  decider) and `EchoAccess.agda`. These are the known warnings triaged in
+  `PROOF-STATUS.adoc`. They are not errors and not postulates.
+* Log: `docs/receipts/agda-cold-2026-11-09.log.gz`. The uncompressed log has
+  sha256 `7f9de4d1f874a0f249eadeb3fc675be346f437cb28cb31fd3e6db1b635e54eb0`.
+
+*Rocq leg.* Source: `hyperpolymath/echo-types` at commit
+`7e9b5f446a50cc6e78faa815e8a5efe7092cdb0b`. `proofs/rocq/EchoSearchExample.v` sha256
+`2a016469af61f11daf2df82ca5ecae6d6ec4b0a2d2a6406b18fef2b516836068`, checked
+with Coq 8.18.0 (OCaml 4.14.1; Ubuntu `coq 8.18.0+dfsg-1build2`). Invocation:
+`bash scripts/check-recheck.sh rocq`, which runs `coqc -q` and requires every
+`Print Assumptions` to report "Closed under the global context" and requires
+one for each of the five headlines by name. Result: six checks (the five
+headlines and `search_as_cost_witness`), all closed, no axioms.
+
+*Lean leg.* Source: `hyperpolymath/echo-types` at commit
+`7e9b5f446a50cc6e78faa815e8a5efe7092cdb0b`. `proofs/lean4/EchoSearchExample.lean` sha256
+`fdb271bfbaa9b1feeee99fce767cf269c8dbaa3da374d870300413ffa4068d94`, checked
+with Lean 4.30.0 (commit `d024af099ca4bf2c86f649261ebf59565dc8c622`; release
+archive sha256 `4dad74141c2c119ca1aa626656be83b8e14238afba97271fd7bf1eb3f081b319`).
+Core only, with no imports and no Mathlib. Invocation:
+`bash scripts/check-recheck.sh lean`, which requires no error, warning or
+`sorry`, every `#print axioms` to report none, and an axiom-free result for
+each of the five headlines by name. Result: six checks (the five headlines
+and `searchAsCostWitness`), no axioms.
+
+*Sensitivity.* Planted errors make each leg fail: `double` changed to add one,
+and the decided budget changed from 4 to 3, which leaves the witness out of
+reach. Each mutant exits non-zero in both Rocq and Lean.
+
+*CI.* The `rocq-recheck` and `lean-recheck` jobs in `.github/workflows/agda.yml`
+run the same scripts on every push and pull request. These are the
+per-commit receipts that `PWG-1` will need.
+
+== Toolchain deviation (§6)
+
+* Legs affected: Rocq and Lean, for this theorem.
+* Tools: Coq 8.18.0 from the Ubuntu 24.04 archive (`coq 8.18.0+dfsg-1build2`);
+  Lean 4.30.0 from the upstream release archive at the sha256 above.
+  `scripts/setup-recheck.sh` asserts both versions and fails on a mismatch.
+* Why not Guix or the container: the repo's Agda lane already installs from a
+  checksum-pinned release archive (`scripts/setup-agda.sh`). These legs follow
+  the same pattern, so that every prover in CI comes from one method, until
+  the Guix manifest carries pinned Rocq and Lean.
+* State: `open`.
+
+== Revalidation triggers
+
+Re-run all three legs, and recompute the grade from the receipts (§8.4.4),
+if any of the following changes:
+
+* the Agda sources in the cone;
+* either target file;
+* the Agda, stdlib, absolute-zero, Coq or Lean pin.
+
+A failing leg drops the grade.