[SamuelSchlesinger]

Part of #4817 (crypto readability, residual lane, item R3). Builds on #4878 (I1).

Session: rerand (Jetski, conversation 4f342748), branch readability/residual-r3-sequence.

Change

This changes how the two sequence-hybrid statements in Computational/Hybrid/Sequence.lean are written. They now use the I1 forms, and their meaning is unchanged.

• sequenceTest_gap is stated with Pr[…], as Pr[replicate count original >>= test] - Pr[replicate count replacement >>= test] = dyadicSize count * (Pr[original >>= sequenceTest …] - Pr[replacement >>= sequenceTest …]). Before, each of the four terms was (Game.succProbability (ProbComp.eval …) : ℝ). The two forms are equal by rfl (Game.coe_succProbability).
• sequenceTest_advantage is stated with Experiment.advantage on the four programs. Experiment.advantage e₀ e₁ is the reducible abbreviation Game.advantage (eval e₀) (eval e₁), so the statement is the old one unfolded, and it no longer needs ProbComp.eval. Its proof uses Experiment.coe_advantage.
• ComputationallyIndistinguishable.replicate_bind is the in-file caller and representative client. It now closes its per-n goal with exact sequenceTest_advantage … in ℝ≥0 once its four game equalities are rewritten. This removes the NNReal.eq step, the hgap restatement and its 7-lemma cast/abs rewrite chain.

Other clients get proof-only edits; none of their statements change. Their owners were notified on the swarm board first:

• GGM/Reduction levelTest_gap: Game.coe_succProbability is added to its closing simpa.
• Pseudoentropy/Masking maskedSequence_prediction_gap: its simp only [Game.coe_succProbability] at hgap is deleted, because the lemma is already in its Pr form.
• GMW/Simulator gmwViewReduction_advantage and GMW/Sequential/Simulator gmwSeqView_advantage_le: these state their goals with Game.advantage (eval …), which rw cannot match against the Experiment.advantage head. They unfold the instantiated lemma with simp only [Experiment.advantage] before rewriting, which adds 3 lines and 1 line.

Manual impact

• Operator's Manual: no edit. Neither theorem is named in manual/. The security-games chapter already presents Experiment.advantage and Pr[…] as the statement forms (from I1).
• Agent Operator's Manual: no edit, because the workflow and tooling are unchanged.
• guide/, ROADMAP.md and CslibFrontierResults have no references. results/goldreich-2007.md (8.6) cites replicate_bind, whose statement is unchanged.

Validation

• lake build --wfail --iofail passes on Sequence, the 4 clients, the other importers (Commitment, Hybrid/SavedPrediction) and the 3 tests that use sequenceTest (Presample, GMWPointwise, SavedPrediction). This is 7606 jobs on main 1334f1b.
• lake lint passes on the 5 changed modules.
• check_changed_files.py --source-only, check_hygiene.py --check-simp, and the projection-chain and encoding-readability ratchets pass.
• Also in this PR: the stale GMW/Simulator.lean: 1 projection-chain baseline entry is lowered, as the ratchet asks. That file has no counted chains on main either; this PR touches only a proof there.
• Hosted CI provides full validation.

Limitations: the GMW proofs and levelTest_gap keep their Game.advantage/Game.succProbability statements. Restating them is outside this item, which only restates the two Sequence theorems. There are no deprecated aliases (pre-release policy).

AI assistance

The refactor and this description were written by an AI agent (Claude, via Jetski) working as a worker in the crypto readability swarm. Agent review is pending; no human has reviewed it yet.

[SamuelSchlesinger]

Agent review (Jetski mac session 30c9671c), head f7dfff7: APPROVE

The restated sequenceTest_gap (Pr[…]) and sequenceTest_advantage (Experiment.advantage) are definitionally the old Game.succProbability/Game.advantage (ProbComp.eval …) statements, since Experiment.advantage is an abbrev and Experiment.coe_succProbability is rfl. So the mathematical claims are unchanged. replicate_bind now closes directly with sequenceTest_advantage, which removes the NNReal.eq/cast chain. That is a real simplification for this client.

I checked every caller on the head (git grep sequenceTest_): GGM levelTest_gap, Masking, both GMW simulators and Hybrid/Sequence.replicate_bind. All are migrated. Dropping the stale GMW/Simulator.lean projection-chain baseline entry is correct. The branch merges cleanly with current main.

Optional, non-blocking: the private gmwViewReduction_advantage still states its result with Game.advantage (ProbComp.eval …), so it now needs simp only [Experiment.advantage] at hattempts hpads before the rw. Restating it with Experiment.advantage would let the rewrite apply directly. That belongs with a later GMW statement pass, which the Limitations section already scopes out.

This is an agent review, not a human review.