[fradamt-agent]

The bound that a link's source epoch is below its target epoch moves from a private lemma of direct safety to Transition/TargetSlots.lean, next to JustifiedSeparated. The finality and slack proofs of FFG justification read it instead of repeating its arithmetic. Part of #2187: this is the link_source_lt item of the #2187 status after #2482.

The problem

A link of FFG justification takes the current or the previous justified checkpoint as its source, and the current or the previous epoch as its target. Once justification runs, from the third epoch on, its source is older than its target. A private lemma, link_source_lt in DirectSafety/Fields.lean, stated that. It reads two facts about the state:

• JustifiedSettled: the current justified epoch is at most the previous epoch;
• JustifiedSeparated: from the third epoch on, the previous justified epoch is below the previous epoch.

processJustificationAndFinalization_slackBits (FfgFinality.lean) and processJustificationAndFinalization_slackJustifiedCheckpoints (FfgSlack.lean) derived the same inequalities inline.

The idea

The fact is about the justified checkpoints, not about direct safety, so it belongs with JustifiedSeparated. As a public theorem it is stated on epochs, so callers need no placeholder checkpoint:

before (private, DirectSafety/Fields.lean):
  link_source_lt (settled) (separated) (later) (current : Bool) (target : Checkpoint)
    (targetEpoch : target.epoch = if current then getCurrentEpoch state else getPreviousEpoch state) :
    (if current then state.currentJustifiedCheckpoint else state.previousJustifiedCheckpoint).epoch
      < target.epoch

after (public, Transition/TargetSlots.lean):
  JustifiedSeparated.source_lt (separated) (settled) (later) (current : Bool) :
    (if current then state.currentJustifiedCheckpoint else state.previousJustifiedCheckpoint).epoch
      < if current then getCurrentEpoch state else getPreviousEpoch state

The two statements are equivalent: the two direct-safety callers rewrite with their target-epoch equation first.

Example

At current epoch 10, the previous epoch is 9.

• current = true: the source is the current justified checkpoint, at most 9 by JustifiedSettled, and the target is epoch 10.
• current = false: the source is the previous justified checkpoint, below 9 by JustifiedSeparated, and the target is epoch 9.

For reviewers

• Readers: the two private epoch lemmas of DirectSafety/Fields.lean, and the two FFG proofs above.
• FfgFinality reads it for the current epoch only; for the previous epoch it keeps separated late, which is that case exactly.
• The module header of TargetSlots.lean gains one line for the new result.

Checks

At head db6a4d0e7, merged with master 094a4a19b:

• lake build --wfail on the four touched modules, their direct importers and EthLib.Consensus.Proofs: passed.
• leanchecker on TargetSlots, FfgFinality, FfgSlack and DirectSafety.Fields: passed.
• scripts/check_writing.py --base upstream/master: no suggestions.
• scripts/check_lean_layout.py --base upstream/master: no findings.
• git grep link_source_lt on master: only the removed private lemma and its two callers.

Earlier checks by the author, at head f8e78d39d4 with master 57c573efa1: full lake build --wfail, check-decls, check-accessors, soundness_facts.py --check, check_layers.py, ty check, tests/downstream, and #print axioms on the changed theorems (only propext, Classical.choice, Quot.sound).

🤖 Generated with Claude Code

[tcoratger]

Reviewed: the move removes the private copy and adds one shared theorem, stated on epochs so callers need no placeholder checkpoint. The two direct-safety callers prove the same facts as before; no statement weakens. Touched modules and importers build with --wfail and replay with leanchecker.