[SamuelSchlesinger]

Removes the positional projection chains from the public definitions and statements of GMW/Sequential, MPC/DDHOT and MPC/OTCommitment/Opening (#1764). The census goes from 13 + 16 + 6 to 3 + 0 + 0. Part of #4817 (mpc-10).

• DDHOT: the three protocol steps, ddhOTOutput and ddhOTAttackBothMessages bind the local state and the reply by name, e.g. fun (((m, c), _), w) => ddhOTSenderReply g m c (w rfl), instead of st.1.1.1 st.1.1.2 (st.2 rfl).
• Opening: the row test in openPairs reads fun ((c, r), (x₀, x₁)) => (x₀ ^^ x₁) == b && (if c then x₁ else x₀) == r. openPairs_ofFn now unfolds with dsimp only instead of restating the whole checker body in a change.
• GMW/Sequential:
  • oneSessionStep and sessionStep destructure the (rem, q, cfg) state.
  • mem_support_oneSessionStep is stated on named components (rem ≤ T → … → (rem', q', cfg') ∈ support … → rem' ≤ rem ∧ q' ≤ q ∧ …) instead of st.2.2/next.2.1. Its two callers destructure the state first.
  • runSeq_sessionStep_two_add binds fun ((rem', cfg'), _) => ….

All rewritten definitions are definitionally equal to the old ones. The IsOraclePPTOn proofs, the DDHOT rfl lemma and the tests compile unchanged.

The 3 remaining chains are the uncurried input of isOraclePPTOn_sessionStep, an IsOraclePPTOn statement that automation looks up by head. #5036 adds IsOraclePPT* to the checker's efficiency exemption, so those chains stay. Chains 13+16+6 → 3+0+0; the baseline is left to the pruning PR (#1276), so this PR doesn't edit projection_chains_baseline.json.

Validation: lake build --wfail --iofail on the 3 modules and all 32 transitive importers (the GMW simulator, ZK amplification, nonuniform ZK, the whole OTCommitment stack and its tests, and the DDHOT test); lake lint on the 3 modules; check_changed_files --source-only; hygiene; projection-chain and encoding-readability ratchets.

Manuals: no edit needed. The Operator's Manual cites openPairs, openPairs_ofFn and the DDHOT results by name, and none of those names or statements changed meaning. The Agent Operator's Manual has nothing on these modules.

AI disclosure: prepared by an AI agent (mpc, Jetski swarm) for Samuel Schlesinger.

[SamuelSchlesinger]

Review: APPROVE at 7ba00e6172e8bbf765634cbef88f8d81e3dad47e. Reviewer: revb-2 (Jetski session 823e1915-b7be-458e-959e-1b7d8141259d). This is agent review, not human approval.

Each rewrite binds exactly the component the old projection read:

• DDHOT: (_, (a, _)) matches st.2.1; ((σ, b), u) matches st.1.1 st.1.2 st.2; (((m, c), _), w) matches st.1.1.1 st.1.1.2 st.2; ((((σ, b), _), _), reply) matches st.1.1.1.1 st.1.1.1.2 st.2. In ddhOTAttackBothMessages, ((e₀, c₀), (e₁, c₁)) gives c₀ - b₀ • e₀ = reply.1.2 - b₀ • reply.1.1, and likewise for the second pair.
• Opening: the row test is the same.
• Sequential: oneSessionStep and sessionStep are the same.

Pattern fun and let on Prod reduce to the projections by structure eta, so the definitions are defeq, as the body says.

mem_support_oneSessionStep on named components is equivalent to the old triple form, and both callers destructure before applying it. The dsimp only in openPairs_ofFn replacing the six-line restating change is a real simplification.

Checks:

• The remerge diff of 7ba00e6 is empty, and git merge-tree with current origin/main is clean.
• The projection list gives Sequential 3, all in isOraclePPTOn_sessionStep's uncurried efficiency input, which stays under the refactor(Logics,Algorithms,WordRAM): make 42 API and general declarations public again (#926) #937 ruling and chore(scripts): count IsOraclePPT predicates as efficiency predicates in the chain check #5036. DDHOT and Opening are at 0, so the baseline edits are right. The encoding ratchet is 0.
• No expose no-ops, and no new line over 100 characters.
• The manuals cite openPairs, openPairs_ofFn and ddhOTAttackBothMessages_eq by name only, so no edit is needed in either manual.

I'll queue once ci-checks and guide are green.

[SamuelSchlesinger]

Advisory notices at 7ba00e6172e8bbf765634cbef88f8d81e3dad47e (ci-checks run 43381046804): 0 repeated proof blocks in 74 proofs, 0 parallel definitions among 7 declarations, 0 duplicate statements among 6 theorems, and all 10 backticked names in the description are declared. The PR doesn't touch manual/, so no rendered check applies. ci-checks and guide are green, and the PR is CLEAN with 0 threads. I've queued the approved head. Recorded by revb-2 (Jetski session 823e1915-b7be-458e-959e-1b7d8141259d); this is agent review.

[SamuelSchlesinger]

Restack delta review: APPROVE ff74af2. revb-2 (Jetski session 823e1915-b7be-458e-959e-1b7d8141259d). This is agent review, not human approval.

git show --remerge-diff ff74af21c (7ba00e6 + main 470e193) changes only scripts/projection_chains_baseline.json. The PR's GMW/Sequential.lean: 3 is kept, along with #5018's deletion of GMW/Simulator.lean: 1. check_restack.py 7ba00e617 ff74af21c reports only that hunk, and the head merges cleanly with main cd4dc42.

Not re-queued yet. Simulating the queue in order, this head conflicts with queued #5049 in the same file. #5049 deletes Garbling/SizeLowerBound.lean on the line next to this PR's DDHOT.lean deletion. Once #5049 lands, one more baseline-only main merge (keeping both deletions) is needed, and I'll queue that head when CI is green on it.

[SamuelSchlesinger]

Delta review, ff74af2 → 89f870c (agent review by revb-2, session 823e1915-b7be-458e-959e-1b7d8141259d; not human approval): APPROVE.

• git diff ff74af21c 89f870c99 only touches scripts/projection_chains_baseline.json, restoring the merge-base (470e193) entries per the program-wide baseline rule. The PR diff against its merge base is now just the 3 Lean files (+39/−39), unchanged since the approved ff74af2.
• Since the merge base, main has changed only DDHOT.lean among these files (refactor(Probability): name the uniform-mask bijections at their call sites (F8) #5001, at L533+ in the idealJoint_ddhOT_sender / bind_unchosen_* proofs). This PR's DDHOT hunks are the step and output definitions at L245–345, so merge-tree with main 956da62 auto-merges without conflict. The proofs refactor(Probability): name the uniform-mask bijections at their call sites (F8) #5001 rewrites are untouched here and already elaborated against these definitions. The PR CI merge build covers the combination.
• An in-order simulation against the current 46-entry merge queue is clean.

I'll queue this head when ci-checks and guide go green. No manual change, so no rendered check is needed.

[SamuelSchlesinger]

CI advisory notices at 89f870c, from the green ci-checks run 43401554144. Recorded by revb-2, session 823e1915-b7be-458e-959e-1b7d8141259d (agent review, not human approval):

• Repeated proof blocks: none in the 74 proofs examined.
• Parallel definitions: none among the 7 declarations examined.
• Duplicate statements: none among the 6 theorems examined.
• PR description names: all 10 are declared.

The PR is CLEAN with 0 unresolved threads. An in-order simulation against the current 54-entry merge queue on main 2c5906b is clean. Queueing at 89f870c.