feat(fc): prove FC-6 update_head preserves the store invariants

[adust09]

Summary

The head-walk theorems (FC-2/FC-4) assume Store.WellFormed, but nothing proved the store's own operations maintain it — the main gap flagged in the safety audit. This PR closes it for update_head, the one mutator the Lean model currently has: all six WellFormed clauses survive updateHead (Store.updateHead_wellFormed).

Argument

update_head rewrites only head and latest_finalized, so five clauses carry over untouched. The substantive clause is justifiedDescendsFromFinalized — the re-derived finalized checkpoint (the head chain's ancestor at the head state's finalized slot) must still sit on the justified chain:

1. descendToSlot_ancestorOrEqual — the finalized re-derivation walk never leaves the head's ancestor chain.
2. FC-2's computeLmdGhostHead_descends — the head descends from the justified root.
3. properAncestor_comparable / ancestors_comparable — parent links are unique, so two ancestors of one block are slot-ordered on one chain; the wrong order contradicts the slot bounds.
4. ancestorWalk_complete — completeness of the Boolean _checkpoint_is_ancestor walk against the relational ancestry. The fuel argument counts distinct stored blocks at or below the walk's position (slotCount), which strictly shrinks every step, so blocks.length + 1 fuel always suffices (a slot-difference bound would not — slot gaps can exceed the block count).

Two store invariants that on_block maintains outside update_head's reach enter as explicit hypotheses rather than growing WellFormed: the justified checkpoint records its own block's slot, and no stored post-state finalizes past the store's justified slot (backed by ST-4). Both are documented in the theorem docstring and the catalog entry.

ancestorWalk and descendToSlot are de-privatized so the lemmas can reason about each step — the same treatment ghostWalk got for FC-2.

Catalog

FC-6 entry added; progress table now 32 proved / 1 axiom / 33 total.

Verification

lake build succeeds (36 jobs); #print axioms for updateHead_wellFormed → [propext, Classical.choice, Quot.sound] only; no sorry.