Fix etcd leader completeness to use commit terms

[Qian-Cheng-nju]

LeaderCompletenessInv rejects a legal execution: an entry created in term 1 is committed in term 3 while a disconnected term-2 leader still has a different log. The predicate compares leader terms with the entry's creation term instead of its commit term.

Record commit observations and election-time logs, retain both histories across restarts, and require each later-term election to contain the earlier committed prefix. Protocol actions and assumptions are preserved. Regenerate the flat and module task contexts and source digest, retaining all eight target statements and IDs.

Validation:

• 21 etcd regression tests pass across source, flat, and module layouts. The old predicate fails after 47 transitions; corrected 67-state scenarios cover later elections, follower commit observations, and crashes. Removing vote log-freshness checking violates the corrected property.
• 117 generator, manifest, and dataset-integrity tests pass.
• Complete module-suite verification: 0 errors. Flat regeneration passed SANY and nondegeneracy gates.
• Ruff lint, formatting, and git diff --check pass.

These are finite regression checks, not an unbounded TLAPS proof. Existing experiments retain their frozen inputs and results; runs against this corrected context must be identified separately.