feat(fc): prove FC-5 block-production iteration terminates

[adust09]

Summary

Final FC proposition — the fork-choice domain is now fully proved (5/5). The catalog marked FC-5 "expressed via WellFoundedRecursion. High difficulty."

Approach

Store/BlockProduction.lean mirrors build_block's fixed-point selection (block_production.py, post leanEthereum/leanSpec#1181 — candidate order and every tie-break content-derived):

• candidatePrecedence — candidates ordered once by (target.slot, hash_tree_root)
• candidateEligible — the per-candidate filter chain (head known, source at the justified anchor, lies on chain, source justified, target not already justified with the genesis self-vote exemption)
• selectionPass — one pass with the MAX_ATTESTATIONS_DATA proposer budget
• selectionLoop — the while True fixed point, defined by well-founded recursion on the unprocessed candidate count with no fuel. The decreasing measure (selectionPass_rest_lt: a pass that accepted something strictly shrinks the remainder) is exactly upstream's own termination argument — "the chosen set only grows, and is bounded". Lean accepts the definition only because the iteration provably terminates: that is FC-5.
• buildBlockAttestations — build_block's setup (slot advancement, genesis anchoring, justified-window extension, chain-view assembly, candidate sort) feeding the loop

The explicit finite-rounds statement

build_block_selection_terminates: the loop reaches its fixed point within payloads.length + 1 passes, for any coverage picker.

Modeling choices (documented in the module docstring)

• The coverage picker (select_proofs_for_coverage) is a parameter: its choices never steer the loop's control flow (a pass continues on which data were accepted, not which proofs), and its tie-break needs encode_bytes of XMSS aggregates (Arklib side) — so FC-5 holds for every picker
• Python re-scans the full sorted list skipping the processed set; the model consumes accepted candidates and re-enters on the remainder — equivalent for distinct dict keys with a fixed order
• The post-loop per-data collapse is packaging outside the fixed point and is not modeled

Catalog: FC-5 checked — FC 5 proved / 0 open, progress table 21/9/1. lake build passes with no sorry, no warnings.