cert: certify a match on a List

[jasisz]

First container for the certificate: a match on a List.

What changes

• Wall (Grammar, GrammarLower, GrammarSound): the patterns [] (emptyList) and [head, ..tail] (cons head tail), and the two-arm List match the emitter lowers: both arms in either order, or either one first with _ second (listPick, the pick of emit_mir_list_match). The lowering stashes the subject, tests it with ref.is_null, runs the [] arm in then, and in else reads the head (field 0) and tail (field 1) of the cons struct into the arm's binders before the cons arm. The soundness case is in agreement_step; the root theorems keep the axioms propext, Classical.choice, Quot.sound. No helper, no runtime contract, no schema change. The wall id rotates.
• Producer: the printer prints the two patterns; plan_check.rs carries the Rust twins of the pick, the typing and the lowering.
• Tests: printer unit test; cert_hardening_spec: the clean List certificate checks, and a plan with the arm results exchanged, the List cons structs declared for each other's instantiation, and a cons pattern with head and tail slots exchanged each decline. Goal matrix, fibonacci blocker pins, json/payment_ops counts moved deliberately.
• Ratchet: 54 gains, no loss (--allow-drop not used).
• Bridge fix found on the way (second commit): a type table long enough to be written in pieces (types_records_0, …) left those pieces folded in a bridge's typing simp. btc-listener's records crossed that length with the new exports, and 65 bridges plus one bridged law fell to sorry until the typing step unfolded the pieces.
• Docs: format §6.1/§6.3, certification.md, CHANGELOG.

Measurements

aver-cert check of btc-listener (commit 5698c8e), main vs this branch:

	main	this branch
checked exports	632	765
law-claims credited	109 / 119	109 / 119
bridged-laws credited	16 / 17	16 / 17
source-bridges credited	494 / 494	494 / 494
check wall time	1316 s	1694 s

Other programs (producer admission):

	before	after
examples + projects + fixtures certified	550	710
payment_ops	59	101
workflow_engine	70	94

A List argument has no source-bridge decoder yet, so the new exports carry no bridge; bridges and laws on bytes do not move until that decoder lands.

Strict aver-cert verify of a three-export List probe: CERTIFIED.

Not in this PR

Non-empty List literals, the List helpers (len, reverse, concat, take, drop, contains), the List bridge decoder, and Vector/Map (a store model and proved helper templates; #1444 is on main and declines every Vector-typed plan until then).

Merged with main

main gained #1444 (wasm-gc Vector versions). The one conflict was the plan-grammar paragraph of docs/certification.md: it keeps this branch's List match and #1444's sentence that a function touching a Vector is declined, and drops the fused Vector.get read from the admitted list. The wall id, the snapshots and the ratchet baseline merged without conflict: #1444 does not touch the wall, the snapshots are unchanged, and tools/cert_ratchet.py passes on the merged baseline as it is (the cellAt drop came with #1444). Re-run after the merge: cargo test -p aver-cert --all-features, cert_hardening_spec (38), cert_certify_spec cert_projects_, the snapshot tests, the cert_verify_spec tripwires (43) and cert_one_build_spec, all passing.