proof(p3.2): A16 — typed ProgressiveCheckW + progressive-order monotonicity (#158)

## Summary

Closes the deferred half of PROOF-NEEDS §P3.2 — the "progressive-order
monotonicity under a typed `ProgressiveCheck`" claim that the 2026-04-18
A8 banner explicitly left as future work:

> the stronger "progressive-order" claim requires redesigning
`ProgressiveCheck` with a typed `level = S prevLevel` index and is left
as future work.

A16 lands that redesign as a **purely additive** `ProgressiveCheckW`
alongside the legacy `ProgressiveCheck`, built on top of the
standards#130 `LevelAttestationW` family (already in tree). Skipping
levels (advancing L1 → L5 in one step) and out-of-order attestations
(attaching `AttestL3W` to a `ProgressiveCheckW 5`) are now **type
errors** — they cannot construct.

## What lands

### `src/abi/TypedWasm/ABI/Proofs.idr` §A16 (~150 LOC appended)

\`\`\`idris
data ProgressiveCheckW : (highestLevel : Nat) -> Type where
  StartL1W : LevelAttestationW 1 -> ProgressiveCheckW 1
  AdvanceW : (n : Nat)
          -> ProgressiveCheckW n
          -> LevelAttestationW (S n)
          -> ProgressiveCheckW (S n)

data VisitedAt : (m : Nat) -> ProgressiveCheckW n -> Type where
  VAStartW : (att : LevelAttestationW 1) -> VisitedAt 1 (StartL1W att)
  VAHeadW  : (n : Nat) -> (prev : ProgressiveCheckW n)
          -> (att : LevelAttestationW (S n))
          -> VisitedAt (S n) (AdvanceW n prev att)
  VATailW  : VisitedAt m prev -> VisitedAt m (AdvanceW n prev att)

progressiveOrderW : (check : ProgressiveCheckW n)
                 -> (m : Nat) -> LT 0 m -> LTE m n
                 -> VisitedAt m check
\`\`\`

Plus:

- `lteSuccCases : {m, n : Nat} -> LTE m (S n) -> Either (m = S n) (LTE m
n)` — decidable LTE case-split helper used by the recursion.
- `chainAlwaysVisitsL1` — specialised corollary for the common "L1 is
the entry point" guarantee.
- `forgetProgressiveCheckW : ProgressiveCheckW n -> ProgressiveCheck` —
index-erasing bridge to the legacy untyped chain, so downstream
consumers can still feed `buildCertificate` via the typed API.

### `PROOF-NEEDS.md`

- New \`RECONCILIATION 2026-06-03 (A16 — P3.2 progressive-order half
closed)\` banner at the top.
- §P3.2 itself now records the closure with the typed-chain signature,
the bridge, and the "Purely additive" / "Zero escape hatches"
disclaimers.
- 3-line owner-line header normalisation (incidental hook compliance —
same micro-pattern as PR #153 / #155).

## Purely additive

The legacy `ProgressiveCheck`, `LevelAchievedIn`, `composeAchievedL/R`,
and the entire `buildCertificate` pipeline are untouched. No external
caller of `ProgressiveCheck` / `StartL1` / `Advance` exists in `src/` /
`examples/` / `tests/` (grep-verified before landing — the only
signature reference is in `tests/proof/regression.mjs`), so the
additivity preserves the typed-wasm public surface.

## Stacking

This PR is **stacked on #152** (`proof/epistemic-fresh-pin-102`) — same
reason as PR #155: the HEAD build break #152 fixes is required for the
package build to pass. Siblings on the same base.

When #152 merges, this PR will rebase forward to `main` as a 1-commit
fast-forward.

## Test plan

- [x] Whole-package build rc=0, 22/22 modules, 0 errors (only
pre-existing shadowing warnings in unrelated modules — Epistemic,
Tropical, Choreography).
- [x] `idris2 --check src/abi/TypedWasm/ABI/Proofs.idr` clean.
- [x] No `believe_me` / `assert_total` / `postulate` / `sorry` /
`Admitted` / `assert_smaller` introduced.
- [x] `%default total` preserved across the arc.
- [x] No SPDX-License-Identifier line changed in any file.
Owner-attribution normalisation only on `PROOF-NEEDS.md` (3-line header
addition — same micro-pattern as #153 / #155).
- [ ] CI green on stacked head.

## Cross-references

- Refs PROOF-NEEDS §P3.2 (the deferred half).
- Refs standards#130 — the `LevelAttestationW` family this PR builds on.
- Refs #102, #152, #153, #155 — companion proof work in flight (this PR
is a sibling of #155 on #152).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

.github/workflows/boj-build.yml

@@ -11,6 +11,7 @@ concurrency:
 jobs:
   trigger-boj:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

.github/workflows/c5-regenerate.yml

@@ -36,6 +36,7 @@ jobs:
   regenerate:
     name: Regenerate C5.1 fixtures and diff
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout typed-wasm

.github/workflows/cargo-audit.yml

@@ -36,6 +36,7 @@ jobs:
   cargo-audit:
     name: Cargo audit (RustSec advisories)
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository

.github/workflows/codeql.yml

@@ -23,6 +23,7 @@ permissions:
 jobs:
   analyze:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     permissions:
       contents: read
       security-events: write

.github/workflows/dogfood-gate.yml

@@ -26,6 +26,7 @@ jobs:
   a2ml-validate:
     name: Validate A2ML manifests
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository
@@ -76,6 +77,7 @@ jobs:
   k9-validate:
     name: Validate K9 contracts
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository
@@ -129,6 +131,7 @@ jobs:
   empty-lint:
     name: Empty-linter (invisible characters)
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository
@@ -193,6 +196,7 @@ jobs:
   groove-check:
     name: Groove manifest check
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository
@@ -251,6 +255,7 @@ jobs:
   dogfood-summary:
     name: Dogfooding compliance summary
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     needs: [a2ml-validate, k9-validate, empty-lint, groove-check]
     if: always()
 

.github/workflows/e2e.yml

@@ -30,6 +30,7 @@ jobs:
   structural:
     name: Structural E2E (no-build)
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository
@@ -44,6 +45,7 @@ jobs:
   smoke:
     name: Smoke test (Node.js AffineScript parser)
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository
@@ -118,6 +120,7 @@ jobs:
   build-e2e:
     name: Build + E2E (Idris2 + Zig)
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository
@@ -187,6 +190,7 @@ jobs:
   cargo-verify:
     name: Cargo build + test (typed-wasm-verify)
     runs-on: ubuntu-latest
+    timeout-minutes: 10
 
     steps:
       - name: Checkout repository

.github/workflows/hypatia-scan.yml

@@ -26,4 +26,5 @@ permissions:
 jobs:
   hypatia:
     uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@5eb28d7d8790d5389b7b6a5233fe6265a775e3d0
+    timeout-minutes: 15
     secrets: inherit

.github/workflows/rhodibot.yml

@@ -31,6 +31,7 @@ concurrency:
 jobs:
   rhodibot:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

.github/workflows/secret-scanner.yml

@@ -16,4 +16,5 @@ permissions:
 jobs:
   scan:
     uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@3e4bd4c93911750727e2e4c66dff859e00079da0
+    timeout-minutes: 10
     secrets: inherit