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

[hyperpolymath]

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 docs(proof-needs): 2026-06-02 reconciliation — five silent P0/P1 closures + A14 (#102) #153 / proof(verifier-spec): ADR-0005 — MkTrustedFixture audit boundary (closes #103) #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

• Whole-package build rc=0, 22/22 modules, 0 errors (only pre-existing shadowing warnings in unrelated modules — Epistemic, Tropical, Choreography).
• idris2 --check src/abi/TypedWasm/ABI/Proofs.idr clean.
• No believe_me / assert_total / postulate / sorry / Admitted / assert_smaller introduced.
• %default total preserved across the arc.
• 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 docs(proof-needs): 2026-06-02 reconciliation — five silent P0/P1 closures + A14 (#102) #153 / proof(verifier-spec): ADR-0005 — MkTrustedFixture audit boundary (closes #103) #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 Epistemic.idr: Fresh and ExplicitSync constructors lack FieldVersion pinning (residual gap after A11) #102, proof(epistemic): pin Fresh to FieldVersion (A14, closes #102) + composeWitness fix #152, docs(proof-needs): 2026-06-02 reconciliation — five silent P0/P1 closures + A14 (#102) #153, proof(verifier-spec): ADR-0005 — MkTrustedFixture audit boundary (closes #103) #155 — companion proof work in flight (this PR is a sibling of proof(verifier-spec): ADR-0005 — MkTrustedFixture audit boundary (closes #103) #155 on proof(epistemic): pin Fresh to FieldVersion (A14, closes #102) + composeWitness fix #152).

🤖 Generated with Claude Code