verity: discharge the 4 remaining residual assembly axioms

[Th0rgal]

Context

After #6, the refinement theorems rest on a minimal trust surface (verity/SphincsMinusVerifiers/AXIOMS.md):

• #print axioms c13_refines_spec = Lean logic + 3 residual assembly axioms
• #print axioms c12_refines_spec = Lean logic + 1 residual assembly axiom
• The SHA-2 variant separately keeps slhDsaSha2_128_24_refines_byte_spec + its opaque Primitives (blocked on byte-addressed memory modeling, out of scope here)

The 4 remaining axioms (all in Proofs.lean):

1. c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0 (L11296)
2. c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1 (L11607)
3. c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual (L12014)
4. c12_layer3_after3_current_node_root_residual (L12263)

Each is a concrete-state instantiation of a generic lemma already proved axiom-clean (C13WotsPkKeccak.lean etc.); what remains is wiring, not new math.

State

Standalone proof scripts for axioms 1-3 are written and committed in verity/probes/ (see probes/README.md). They are complete proofs awaiting validation: each compile peaks at ~22 GB RSS, so they have not all been run yet.

• probe_inputs_layer0.lean: a validation compile is in progress
• probe_reverted_layer0.lean, probe_layer1.lean: written, not yet compiled

Remaining work

• Compile each probe (LEAN_NUM_THREADS=2 lake env lean probes/<probe>.lean from verity/, one at a time, ~22 GB RSS each; use an RSS watchdog on constrained hosts) and confirm a clean #print axioms
• Fold the three proofs into Proofs.lean, replacing the axiom declarations. Note: the layer-1 theorem derives "currentNode" from the layer-0-only residual c13_ok_afterMerkle_initial_wotsPk_residual_layer0 (L11812), so it must move after that declaration and its consumers (L11645+) must be reordered
• Attempt c12_layer3_after3_current_node_root_residual (deep C12 layers 0-3 roundtrip; the heaviest of the four, may need a >64 GB machine)
• Full rebuild via scripts/build.sh (never bare lake build on <64 GB machines), zero sorry, strictly smaller axiom cones
• Update AXIOMS.md / READMEs, remove verity/probes/

End state: c13_refines_spec and c12_refines_spec rest on Lean's logic alone (the SHA-2 bridge axiom remains the only model-specific assumption in the repo).