feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ

[Abraxas1010]

Summary

Fills the open sorry in SendWitness.reduction_completeness — per the coordination note on #627 (no claim was raised, so bringing the proof as offered) — and adds the general step lemma its investigation surfaced:

• Prover.runToRound_succ (Execution.lean, beside runToRound_zero_of_prover_first): prover.runToRound i.succ = prover.processRound i (prover.runToRound i.castSucc) — a one-line term via Fin.induction_succ. This is the round-by-round unfolding brick for collapsing concrete protocol executions; its absence is why component completeness proofs were stuck.
• SendWitness.reduction_completeness — proven. The interesting discovery: for this component the entire Reduction.run collapses definitionally — have hrun : (reduction …).run stmtIn witIn = pure ((Transcript.concat witIn default, (stmtIn, witIn), ()), (stmtIn, witIn)) := rfl — the kernel reduces the monad lifts, the direction match, the Fin.induction, and the transcript concat in one step (the key is ascribing default at the literal index 0, where the Transcript instance synthesizes). The probabilistic legs then follow the Reduction.id_perfectCompleteness template exactly (one_le_probEvent_iff → probEvent_eq_one_iff → the OptionT/simulateQ/StateT change-chains).

#print axioms: reduction_completeness = [propext, Classical.choice, Quot.sound]; runToRound_succ = [propext, Quot.sound].

Notes

• The oracle-reduction variants further down the file (their own sorrys) are untouched — this PR is deliberately the smallest complete unit; the same rfl-collapse + template recipe should apply there and we're happy to follow up.
• This is the completeness demonstrator for the BCS transform plan in Design: the BCS transform as a change of oracle implementation (QueryImpl), with a staged opening plan #627: our phase-2 (reveal round) completeness is exactly SendWitness-shaped.
• Full lake build of both touched modules green; no new axioms; no native_decide/bv_decide.

---

Contributed by The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[github-actions]

🤖 PR Summary

sorry delta: -1 (1 removed) — net proof progress

Mathematical Formalization

• Prover.runToRound_succ (ArkLib/OracleReduction/Execution.lean): A new theorem that gives a one-step unfolding of runToRound: for any index i : Fin n, prover.runToRound i.succ stmt wit = prover.processRound i (prover.runToRound i.castSucc stmt wit). This identity is a one-liner via Fin.induction_succ and serves as a workhorse for collapsing concrete protocol executions round by round, providing the missing brick that unblocks component completeness proofs (such as the one in this PR). The lemma uses only [propext, Quot.sound] as axioms.

Proof Completion (sorries removed)

• SendWitness.reduction_completeness (ArkLib/ProofSystem/Component/SendWitness.lean): Previously stubbed with sorry, this theorem is now fully proved. It establishes the perfect completeness of the reduction from oSpec Statement Witness. The key discovery is that the entire Reduction.run collapses definitionally: reduction.run stmtIn witIn reduces to pure ((Transcript.concat witIn default, (stmtIn, witIn), ()), (stmtIn, witIn)) by rfl, as the kernel reduces the monad lifts, direction match, Fin.induction, and transcript concatenation in one step (the default at index 0 resolves via the Transcript instance). The probabilistic legs follow the Reduction.id_perfectCompleteness template exactly: one_le_probEvent_iff → probEvent_eq_one_iff → the OptionT/simulateQ/StateT change-chains. The final proof uses simp, rw, probEvent_eq_one_iff, one_le_probEvent_iff, probOutput_eq_zero_of_not_mem_support, and simulateQ_pure. The #print axioms show [propext, Classical.choice, Quot.sound] — no new axioms beyond standard classical ones, and no native_decide/bv_decide.

Scope and Context

• This PR is deliberately the smallest complete unit: it fills only the SendWitness sorry and adds the lemma that was missing for that proof. The oracle-reduction variants further down the file (their own sorrys) are untouched; the same rfl-collapse plus template recipe is expected to apply there in follow-ups.
• The PR is a step toward the BCS transform plan (see coordination note on Design: the BCS transform as a change of oracle implementation (QueryImpl), with a staged opening plan #627): the phase-2 (reveal round) completeness is exactly SendWitness-shaped.
• Full lake build of both touched modules passes; no new sorry or admit placeholders are introduced.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	53
❌ Lines Removed	2

---

Lean Declarations

✏️ Added: 1 declaration(s)

ArkLib/OracleReduction/Execution.lean (1)

• theorem Prover.runToRound_succ (i : Fin n)

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

ArkLib/ProofSystem/Component/SendWitness.lean (1)

• theorem reduction_completeness : (L77)

---

📄 **Per-File Summaries**

• ArkLib/OracleReduction/Execution.lean: Added a new theorem Prover.runToRound_succ to ArkLib/OracleReduction/Execution.lean. This theorem provides a one-step unfolding of runToRound, establishing that for any index i : Fin n, prover.runToRound i.succ stmt wit equals prover.processRound i (prover.runToRound i.castSucc stmt wit). This is intended to serve as a workhorse for collapsing concrete protocol executions round by round, for instance in component completeness proofs.
• ArkLib/ProofSystem/Component/SendWitness.lean: The reduction_completeness theorem, which states the perfect completeness of the reduction from oSpec Statement Witness, was previously stubbed with sorry and is now fully proved. The proof uses simp and rw to unfold definitions, then applies probEvent_eq_one_iff and one_le_probEvent_iff to show both that the probability of failure is zero (via probOutput_eq_zero_of_not_mem_support and simulateQ_pure) and that every output is a valid witness (by analyzing the support of the run). This eliminates the incomplete stub and establishes the completeness direction for the reduction's perfect completeness property.

---

Last updated: 2026-07-10 19:12 UTC.