cert: certify non-empty List literals

[jasisz]

Second List step for the certificate, stacked on #1445: non-empty List literals.

The first commit is #1446 (the acceptance proofs read the type section only through its cut). Without it, btc-listener's check runs past the 9000-second limit after #1444, so the measurements below need it. It drops out of this diff once #1446 is on main and this branch is rebased.

What changes

• Wall (Grammar, GrammarLower, GrammarSound, TypeTable, SchemaCore, AcceptedArtifactCore, AcceptanceSoundness): the node list t items now admits a non-empty literal. Its typing needs the cons helper the type table declares for the element type (TypeTable.listCons, the new MCtx.listCons), with the planned signature (t, List<t>) -> List<t>, and every item typed at t. Its lowering is the items, ref.null of the cons struct, and one call of the helper per item. This is exactly emit_mir_list_literal, and the last item is consed first. Its meaning is the cons cells of the items in order (consAll).
• The helper is proved, not assumed. The producer offers the cons helper as a planned internal function. The new acceptance conjunct consPinned requires every declared helper to be a planned function whose body is the wall's cons plan, one List.prepend of its two parameters (isConsPlan). The agreement proof takes the helper's Contract plus the model fact that its meaning is List.prepend (hConsF), and folds the calls over the reversed items (consCalls_run). fn_certified_group discharges that model fact from the plan (groupModel_consPlan), and fn_certified_total threads it through. The root theorems keep the axioms propext, Classical.choice, Quot.sound. There is no schema change, and the wall id rotates.
• Producer: the printer prints the items and declares the helper per element type. produce.rs offers the helper with the literal's function, counts it as a call target, and keeps a listCons entry only when its helper is offered. plan_check.rs has the Rust twins of the typing and lowering. Plans.lean writes listCons only when it is non-empty, so a module without literals renders as before, and the snapshots move only by the wall id. Bridge steps gained the simp lemmas that unfold a literal, so a function that returns a literal is now bridged.
• Byte-binding lint: the pin checks only the helper's body. Checking its slot count and locals as well made the lint count those FnPlan fields as bound for every plan, and lint_flags_the_removed_code_entry_pin caught it.
• Tests: a printer unit test. In cert_hardening_spec, the clean literal certificate checks, and each of these is refused: the List<Int> helper declared as a user function of the same signature whose plan returns the tail, the helper's own plan changed to return the tail, and the List<Int> and List<String> helpers exchanged. The payment_ops count pin moves from 101 to 106. A strict aver-cert verify of a seven-export literal probe returns CERTIFIED, with 6 of 6 bridges credited.
• Ratchet: 5 exports and 4 bridges gained in payment_ops, nothing lost (--allow-drop not used).
• Docs: format §6.1, §6.3 and §7.3, certification.md, CHANGELOG.

Measurements

aver-cert check of btc-listener (commit 5698c8e), one Lean process, AVER_CERT_PHASE_TIMEOUT_SECS=9000:

	#1445 merged with main, plus #1446	this branch
checked exports	765	823
law-claims credited	109 / 119	109 / 119
bridged-laws credited (laws on bytes)	16 / 17	16 / 17
source-bridges credited	494 / 494	535 / 535
check wall time	1331 s	1611 s

The census predicted +58 for btc, and all 58 arrive. Examples, projects and certificate fixtures (producer admission): 706 → 733.

Laws on bytes do not move yet. The laws over List functions need bridges for List arguments, which is the decoder PR that comes next.

Tests run

cargo test -p aver-cert --all-features, the printer unit tests, the certificate snapshots, cert_one_build_spec, cert_hardening_spec (42), cert_certify_spec (39, with the payment_ops pin moved), and the cert_verify_spec tripwires (43). Also cargo fmt --check and clippy on both crates.