test: pin equal-slot LMD tie determinism across hash seeds (leanEthereum#1025)

State the invariant that all proofs under one attestation data share a slot,
so the strict slot comparison never overwrites between them and native set
iteration order is non-consensus. The equal-slot equivocation vectors plus
the cross-hash-seed determinism check already prove an identical head; this
comment locks the reasoning at the loop a future refactor could break.

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

Author: tcoratger

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

@@ -668,6 +668,9 @@ def extract_attestations_from_aggregated_payloads(
             if attestation_data.head.slot <= latest_finalized_slot:
                 continue
 
+            # Every proof here shares one attestation data, so they share one slot.
+            # The strict slot comparison below never overwrites between them.
+            # Set iteration order is therefore non-consensus and safe to leave native.
             for proof in proofs:
                 for validator_index in proof.participants.to_validator_indices():
                     # Keep this vote only when it is newer than the one already stored.