Verified equivalence of incremental (proto-array-style) LMD-GHOST head vs naive spec walk

[adust09]

Context

Upstream's _compute_lmd_ghost_head re-tallies votes on every call — a naive walk. Production clients use proto-array / incremental weight-delta structures instead. Today, every client team re-derives the correctness of that optimization informally.

Our proof assets already cover the naive side: FC-1 (update_head_deterministic, computeLmdGhostHead_in_store), FC-2 (head_descends_from_justified), FC-4 (fork_choice_acyclic via properAncestor_slot_lt).

Proposal

1. Model an incremental weight-cache head computation (proto-array style: per-block weight deltas, best-child/best-descendant propagation) in LeanSpec/Forks/Lstar/Store/.
2. Prove the refinement theorem: for any Store.WellFormed store, incremental head = computeLmdGhostHead head (including tie-break behavior, which is content-derived since fix(fork-choice): make the equal-slot equivocation tie deterministic leanEthereum/leanSpec#1181 — insertion-order independence is what makes this statement well-posed).
3. Publish the theorem as a conformance target: clients implementing proto-array can point at a machine-checked proof that their algorithm agrees with the reference spec.

Why

Highest-value item in the verified-refinement direction: the spec stays naive and readable, while the one optimization every client actually ships gets a mechanized correctness proof shared across teams. Divergent tie-break or delta-propagation bugs in this layer are exactly the cross-client interop failures the reference spec exists to prevent.

Estimated scope

Medium — requires new modeling (weight deltas, propagation invariants), not just re-plumbing existing lemmas. Good milestone after the fuel-removal work (see companion issue), since the walk lemmas get cleaner first.

[adust09]

Weight-delta layer delivered in #74 (merged at c9253b7): Weights.Equiv, pointwise additivity (accumulateAncestorWeights_append), order-freedom (accumulateAncestorWeights_perm), and computeLmdGhostHead_incremental — any incrementally-maintained map extensionally equal to the full tally selects the spec head, tie-break included.

Remaining for full proto-array refinement: the best-child/best-descendant cache layer (propagation invariants); its correctness reduces to the walk over the same weight function already proved. Keeping this open for that layer.