verity: discharge C13 layer-1 bridge axioms

[Th0rgal]

Summary

• remove the two C13 layer-1 bridge axioms from C13ResidualLayer1Inputs
• thread the bridge facts as explicit parameters through the residual layer-1 assembly theorem
• discharge those facts later in Proofs.lean, where the existing layer-0/after-Merkle facts are already available

Verification

• cd verity && ./scripts/build.sh SphincsMinusVerifiers.Proofs
• #print axioms SphincsMinusVerifiers.c13_refines_spec reports only [propext, Classical.choice, Quot.sound]

---

Note

Low Risk
Lean-only proof refactor with no runtime behavior change; risk is localized to whether the new bridge proofs are correct relative to the removed axioms.

Overview
Removes the two layer-1 bridge axioms from C13ResidualLayer1Inputs and replaces them with explicit hypotheses on the residual layer-1 theorems: first-layer stepLayer keeps seed at memory 0x00, and the second-layer guard’s "currentNode" binding matches d.root0.

Call sites in C13ResidualLayer1Assembly and the large Proofs.lean layer-1 residual chain now take hStepSeed and hCurrent0RootBridge instead of proving those facts locally from axioms. Proofs.lean supplies the proofs: seed via existing layer-0 stepLayer / memory-zero lemmas (rewritten through residual guard-state equalities), and c13_layer1_current0Root_of_layer0_wotsPk, which derives "currentNode" from the already-composed layer-0 after-Merkle WOTS-PK / XMSS climb facts.

^{Reviewed by Cursor Bugbot for commit 6f37525. Bugbot is set up for automated code reviews on this repo. Configure here.}