feat(fc): define store pruning and prove the finalized-slot memory bound

[adust09]

Summary

Delivers the memory-bound and invariant halves of #71 (verified safety of store pruning below the finalized root).

New file LeanSpec/Forks/Lstar/Store/Prune.lean:

Memory bound

• Store.prune — concrete pruning: drop every block/state whose root is not in the finalized subtree, decided by the same checkpointIsAncestor walk fork choice already uses. Control fields (checkpoints, head, vote pools) untouched.
• mem_prune_blocks_iff — a block survives iff the finalized checkpoint is its ancestor.
• prune_block_slot_ge / prune_blocks_length_le — the memory bound: the live store after pruning is bounded by the blocks at or above the finalized slot. This is the statable upper bound Verified safety of store pruning below the finalized root (via ST-6 / FC-2) #71 feeds upstream (today the reference store grows without bound).
• prune_blocks_sublist — pruning only drops entries.

Invariant preservation (second commit)

• getBlock?_prune_iff / getState?_prune_iff — pruned-store lookups return the original entry exactly when pruning keeps it (assoc-list find?/filter characterization under key uniqueness).
• ancestorWalk_sound — walk success exhibits the relational ancestry plus the ancestor block at the checkpoint slot (converse of ancestorWalk_complete).
• keepBlock_of_ancestorOrEqual — every finalized-subtree block survives pruning.
• properAncestor_prune — finalized-rooted ancestry derivations transfer to the pruned store.
• prune_wellFormed — pruning preserves WellFormed. The justified anchor survives with its finalized ancestry: the justified root lies on the finalized subtree (M-1 clause), the transferred relation is re-run by walk completeness inside the pruned store (via an auxiliary store whose justified checkpoint is the finalized one, breaking the WellFormed circularity), and congruence maps the result back.

All theorems sorry-free; lake build passes.

Not in this PR (follow-up per #71)

The observational-equivalence half (update_head/on_block/checkpoint evolution agree between st and prune st). It builds directly on the subtree-transfer lemmas proved here.

Refs #71