feat(fc): prove incremental weight maintenance agrees with the naive tally

[adust09]

Summary

Delivers the weight-delta layer of #67 (verified equivalence of incremental LMD-GHOST head vs naive spec walk).

New file LeanSpec/Forks/Lstar/Store/IncrementalWeights.lean proves the algebraic core that makes proto-array-style incremental maintenance a refinement of the naive re-tally:

• Weights.Equiv — extensional equality of weight maps (get-equal; entry order and explicit zeros are irrelevant), with Weights.get_bump characterizing bump as pointwise +1.
• creditChain_get_add / accumulateAncestorWeights_append — the vote tally is pointwise additive: crediting a batch is the pointwise sum of crediting its parts. This is exactly what makes per-vote weight deltas well-defined.
• accumulateAncestorWeights_perm — the tally is order-free: any permutation of the vote list yields the same weight function, so incremental updates may be applied in any order.
• ghostWalk_congr_weights / computeLmdGhostHead_incremental — the GHOST descent (child enumeration, threshold filter, comparison, tie-break included) reads weights only through get; any maintained map extensionally equal to the full tally selects exactly the head of the naive spec walk.

Together: a client maintaining the weight map incrementally — batching and reordering however it likes — computes the same head as _compute_lmd_ghost_head, provided its map is get-equal to the full tally. Well-posedness of the statement rests on the content-derived tie-break (leanEthereum/leanSpec#1181), already modeled in votePrecedence.

creditChain is made public (was private) so the lemmas can reason about each step — same precedent as ghostWalk.

All theorems sorry-free; lake build passes.

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

The best-child/best-descendant cache layer of proto-array (propagation invariants, cache validity). Its correctness statement reduces to the walk over the same weight function proved here.

Refs #67