docs(fork-choice): clarify equal-slot tie resolution wording (#1143)

The latest-vote extraction docstring said the first vote seen wins on
equal slots, while an adjacent comment noted that all proofs under one
attestation data share a slot. Read together these could seem to
contradict each other.

Reword the docstring to state that equal-slot collisions arise only
across distinct attestation data, so the first-inserted-wins rule
applies at the distinct-data level, consistent with the loop comment.

Docs-only change. just check passes.

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: tcoratger

src/lean_spec/spec/forks/lstar/fork_choice.py

@@ -628,7 +628,8 @@ def extract_attestations_from_aggregated_payloads(
         Map each participating validator to the latest vote it cast.
 
         This is the LMD view fork choice runs on.
-        On equal slots the first vote seen wins, since the slot comparison is strict.
+        Two votes share a slot only across distinct attestation data, never within one data.
+        On such an equal-slot tie the strict comparison keeps the first distinct data inserted.
 
         A vote whose head sits at or below the finalized slot carries no fork-choice weight.
         Such stale votes are skipped here, so callers pass their pool without pre-filtering.