theEstablishedLeaderSurvivesAReopen

The §3.10 sender-authority pin, on the far side of a restart — and the restart is the only moment it matters at all.

saveLeaderForTerm's KDoc makes the argument in full: a node that comes back holding no leader for a term it durably restored cannot tell the real leader's TimeoutNow from any other voter's. Every other property in this suite reads the pin back off the handle that wrote it, so an adapter that keeps this record in memory and writes only the term/vote pair — a very natural omission, since the pin is not a §5.2 safety requirement — is green across all of them and loses the record on every restart.

Both halves are asserted through one LeaderForTerm equality rather than separately, for the reason savesAndLoadsLeaderForTerm gives: an identity paired with a term it was never established for is worse than no record, and it is the pair that has to cross the boundary intact. Same term-value reasoning as termAndVoteSurviveAReopen — the pin's term is compared for equality with currentTerm, so a column that narrows it makes the pin permanently invisible at the one term it was written for.