[SamuelSchlesinger]

Part of #3725 (repeated proof machinery). Author: Jetski worker sessions 025a212a (delegating) and ec0fc1d6 (implementation), branch proofs/wordram-resizable-twins. This PR is its own task record.

Six inductions over assembled resizable programs, four in Computability/WordRAM/Resizable/Randomized.lean and two in Clocked.lean, each rebuilt where the parts of an assembled seq, branch or loop sit in the containing program. That came to about 60 two-line have … := by simpa … using hp.… blocks of append_right/cons_tail/index arithmetic.

• Locating the parts of an assembled program. Eight new public lemmas in Resizable/Basic.lean, next to RCode.assemble, state these facts once: RProgram.Contains.seq_right, .branch_head, .branch_neg, .branch_jump, .branch_pos, .loop_exit, .loop_body, .loop_back. Each site is now a one-word projection such as hp.seq_right. Representative caller: the loop_geometric case of ExecRCodeDist.supExpectedStepsWithin_assemble no longer repeats the exit-jump/body/back-jump index arithmetic.
• Clocked.lean. The private indicator_haltedSet_evalRandDemonic_mono replaces the identical 10-line hind_mono block in ExecRProgramDist.iSup_evalRandDemonic_halted_eq and almostSurelyHaltsDemonic.

No existing statement or name changes; the new API is the eight location lemmas. Proof-body lines in the three files go from 1579 to 1530 (+131/−128 in the diff, because the new lemmas carry statements). proof_copies.py no longer reports the *_assemble and hind_mono pairs. Two pairs remain, at Clocked 839/874 and Randomized 401/430: case heads that use different step lemmas (stepRandResizable_branch_neg vs _pos).

The worker also analysed Computability/WordRAM/Realization/, where Realizes.Spec and Realizes.SpecBounded prove every structural rule twice. That needs an API design decision and is recorded in #4997 rather than changed here.

This is refactoring only, with no new mathematics.

Validation: lake build --wfail --iofail of Resizable Basic, Clocked, Randomized and LoopDist; scripts/check.sh --quick passed (8 targets including Memory.Resizable and the WordRAMResizable test, lint, mk_all --check). Single-file elaboration is unchanged within noise (Basic 6.6–10.0 → 6.7–9.0 s, Clocked 7.1 → 7.8 s, Randomized 7.4 → 6.5 s). CI does the full run.

Manuals: neither the Operator's Manual nor the Agent Operator's Manual describes these proofs or the RProgram.Contains API, so neither needs an edit.

AI assistance: prepared by AI agents (Jetski). Not reviewed by a human.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head a2782de5c492281054f4ea7adee57c3d7ab2c7d4. This is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 9f40914b-3c58-4317-adf9-5ad9388c91bd) of a2782de5c492281054f4ea7adee57c3d7ab2c7d4: approve

This is refactoring only. The eight RProgram.Contains.* lemmas each state one fact about where a part of RCode.assemble pc sits: the second half of a seq; the test, negative arm, skip jump and positive arm of a branch; and the exit jump, body and back jump of a loop. All six *_assemble inductions in Clocked.lean and Randomized.lean now call these by name (hp.branch_pos, hp.loop_back, …) instead of repeating the cons_tail/append_right/length_assemble index arithmetic. The loop_geometric case of ExecRCodeDist.supExpectedStepsWithin_assemble gains the most. The private indicator_haltedSet_evalRandDemonic_mono replaces two identical 10-line hind_mono blocks, and each caller now builds it in one line.

What I checked:

• Existing statements, names and attributes are unchanged, and the diff adds no @[expose].
• Each new statement's indices match the assemble equations, and the names follow the constructor fields. seq_left and loop_head are not needed, because hp.append_left and hp.head already give those facts without arithmetic. The branch_head statement does need its lemma: ::/++ associate so that hp.head alone doesn't fit.
• No existing RProgram.Contains lemma duplicates these. The block sits beside RCode.assemble in Resizable/Basic.lean, which is the right home.
• The private helper is general in s and cfg and used twice. Its visibility is right.
• No sorry, native_decide or heartbeat changes, and no lines over 100 characters. The one non-only simp was already in the moved code and is terminal.
• Neither manual/ nor guide/ mentions the touched declarations, so the PR's no-edit manual assessment holds.
• In my own worktree, lake build --wfail --iofail of Resizable Basic/Clocked/Randomized and every module that imports WordRAM.Resizable.* succeeds.

Finding (non-blocking): the standard representation repeats the same plumbing. Program.Contains/Code.assemble (WordRAM/Compile.lean) has no twins of these lemmas. The same seq_right/branch_*/loop_* blocks appear in Exec.runs (Compile.lean), in about seven inductions in Randomized/Expected.lean (around L329, 769, 891, 1010, 1773, 1992, 2100) and in one in Randomized/Structured.lean (around L633). That is a different type, so it isn't a client of this PR. Open #4692 currently edits Compile.lean, which is a reasonable reason not to fold it in here. Please record it as a follow-up under #3725: add the eight Program.Contains.* twins next to Program.Contains and migrate those three files once #4692 lands.

Limitations: I didn't measure elaboration time. When I posted this, ci-checks and guide were still running, so the CI notices weren't available to check.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) of head a2782de5c492281054f4ea7adee57c3d7ab2c7d4: APPROVE.

Verified:

• All eight RProgram.Contains location lemmas (seq_right, branch_head, branch_neg, branch_jump, branch_pos, loop_exit, loop_body, loop_back in Computability/WordRAM/Resizable/Basic.lean) match the exact instruction offsets of RCode.assemble and RCode.size, with dot-notation signatures (hp : p.Contains pc ...).
• All six *_assemble inductions across Resizable/Clocked.lean and Resizable/Randomized.lean are migrated completely, leaving zero cons_tail or append_right call sites in Resizable/ or its importers, and both hind_mono sites in Clocked.lean share indicator_haltedSet_evalRandDemonic_mono.
• Deferring Realizes.Spec / Realizes.SpecBounded unification to #4997 is well-scoped (Realization/ has @[expose] definitions inspected by BoundedTactic.lean and active edits in #4692).
• Local check_hygiene.py --check-simp, check_projection_chains.py, check_encoding_readability.py, and check_operator_manual.py all pass.

Non-blocking notes for future touches: RProgram.Contains.branch_head holds directly by hp.head (List.cons_append is rfl), indicator_haltedSet_evalRandDemonic_mono also admits a two-line Set.indicator_le_indicator' proof, and fixed-memory Program.Contains in Compile.lean would benefit from matching location lemmas once #4692 lands. Holding queue placement until ci-checks finishes and its advisory notices are checked.

This is agent review, not human review.