feat(AppendOneMsg): unconditional append perfect completeness at 1-message ++ 1-message

[Abraxas1010]

The capstone of the composition thread on #627: for single-message protocols with pure verifiers — the commit-then-reveal shape — perfect completeness composes across Reduction.append unconditionally. Sorry-free; axioms [propext, Classical.choice, Quot.sound].

New file Composition/Sequential/AppendOneMsg.lean:

• Field equation lemmas for Prover.append at the embedded literal indices — the Eq.mpr casts from the tactic-mode field definitions fall to a reusable eq_mpr_eq_cast/cast_heq/congr 1 recipe (left region, the i = m boundary handoff, input, output).
• append_run_components — the appended prover's run written entirely in component operations, each under an explicitly pinned direct lift (warning documented: a restated liftM can elect a two-hop route through a component's challenge-sum that is semantically but not definitionally equal to processRound's lift).
• Simulated bridges — the direct lifts wash out under any QueryImpl (simulateQ_liftM_eq_of_query at the pinned chain).
• hfact_oneMsg — the prover-level simulated factorization, i.e. feat(Append): completeness composition under init-uniformity + run_pure_verifier #635's hypothesis, proven through Prover.append's actual definition.
• append_perfectCompleteness_oneMsg — the crown: h₁ at init, h₂ uniformly in the initial state, pure verifiers ⟹ appended perfect completeness.

Notes for review:

• Stacked on feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631 and feat(Append): completeness composition under init-uniformity + run_pure_verifier #635 (their commits are included so CI builds; the new content is AppendOneMsg.lean + one ArkLib.lean import line). Happy to rebase once those land.
• The composition theorem is restated locally in a CompositionLocal section: applying the Append.lean copy at these concrete reducible specs runs into a pinned-vs-generic OracleInterface unification storm (whnf heartbeat divergence) — documented in-file; deduplicating is a follow-up once the instance story for concrete specs is settled.
• Toolchain note that will matter for the general Prover.append_run: rw/simp refuse the simulateQ_bind/StateT.run_bind rewrites on these goals; erw (or term-level congrArg+Eq.trans) is required. The full proof cadence is visible in hfact_oneMsg as a template.

With #631 + the reveal-round completeness from the #627 thread, stage-1 BCS completeness now assembles end-to-end.

From The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis

[github-actions]

🤖 PR Summary

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

This PR adds the AppendOneMsg.lean file, imports it, and patches a sorry in SendWitness.lean. The core new theorem append_perfectCompleteness_oneMsg (in AppendOneMsg.lean) proves that perfect completeness composes across Reduction.append for single-message protocols with pure verifiers, without the factorization hypothesis needed by the generic append_perfectCompleteness_of_proverFactorization in Append.lean. The supporting hfact_oneMsg theorem provides the prover-level simulated factorization. The file also contains extensive supporting lemmas for field equations, run decomposition, transcript alignment, simulation bridges, and a local restatement of the factorization-dependent lemma. A separate sorry in SendWitness.lean is replaced with a complete proof. The PR is stacked on #631 and #635.

Mathematical Formalization

AppendOneMsg.lean (new file)

• Main theorem: append_perfectCompleteness_oneMsg — unconditional perfect completeness for Reduction.append of two single-message protocols with pure verifiers.
• Supporting theorem: hfact_oneMsg — the prover-level simulated factorization (P₁.append P₂).run = P₁.run then P₂.run, proven through Prover.append's actual definition.
• Concrete specs: spec₁ and spec₂, each a single .P_to_V round with a message type.

Component-wise equation lemmas breaking the appended prover's operations:

• append_sendMessage_left, append_sendMessage_boundary, append_input, append_output.

Run decomposition: append_run_components expresses the appended run in terms of per-component operations under direct lifts.

Transcript alignment: transcript_align shows the nested transcript concatenation equals the ++ₜ of the two single-message transcripts.

Simulation bridges:

• bridge_c / bridge_d prove that simulating a directly-lifted oSpec computation through the composed challenge-sum QueryImpl equals simulating it through the lifted base implementation.

Local restatement: append_perfectCompleteness_of_proverFactorization with the hfact hypothesis, used to derive the unconditional theorem by supplying hfact_oneMsg.

Notes (in-file): The composition theorem is restated locally because applying the generic Append.lean copy at these concrete reducible specs runs into OracleInterface unification issues (whnf heartbeat divergence). rw/simp refuse certain rewrites; erw or term-level congrArg+Eq.trans is required.

Append.lean

• run_pure_verifier: For a reduction whose verifier is pure, Reduction.run collapses to a lift of the prover's run.
• append_perfectCompleteness_of_proverFactorization: Perfect completeness composes across Reduction.append under assumptions of pure verifiers, prover-level simulated factorization hfact, and that R₂ is complete uniformly in the initial state. Addresses a previous TODO.

Execution.lean

• Prover.runToRound_succ: One-step unfolding of runToRound (prover.runToRound i.succ stmt wit = prover.processRound i (prover.runToRound i.castSucc stmt wit)), for collapsing concrete protocol executions round by round.

Proof Completion (sorries removed)

SendWitness.lean

• reduction_completeness: Replaced sorry with a complete proof. Uses simp, rw, refine with two subgoals: (1) probability of failure is zero via probOutput_eq_zero_of_not_mem_support and simulateQ_pure; (2) every support element corresponds to a valid input by rewriting through StateT.run_pure and map_pure.

Infrastructure / CI

• ArkLib.lean: Added import of ArkLib.OracleReduction.Composition.Sequential.AppendOneMsg.
• Stacked on feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631 and feat(Append): completeness composition under init-uniformity + run_pure_verifier #635 (commits included for CI; new content is AppendOneMsg.lean + import line). Happy to rebase once those land.

No remaining sorry or admit

Per the PR body: "Sorry-free; axioms [propext, Classical.choice, Quot.sound]." No sorry/admit appear in any per-file summary.

PR Body Discrepancy

The PR body states "With #631 + the reveal-round completeness from the #627 thread, stage-1 BCS completeness now assembles end-to-end", but the per-file summaries do not mention BCS or reveal-round completeness directly. The actual code changes do provide the missing piece for that assembly, so the body is incomplete but not contradictory.

Dependency Note

Stacked on #631 and #635. The core change is in AppendOneMsg.lean; the remaining files are mechanical (import, one-shot lemma, sorries fixed).

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	772
❌ Lines Removed	2

---

Lean Declarations

✏️ Added: 23 declaration(s)

ArkLib/OracleReduction/Composition/Sequential/Append.lean (2)

• theorem append_perfectCompleteness_of_proverFactorization
• theorem run_pure_verifier

ArkLib/OracleReduction/Composition/Sequential/AppendOneMsg.lean (20)

• @[reducible] def liftc {M₁ M₂ α : Type} (x : OracleComp oSpec α) :
• @[reducible] def liftd {M α : Type} (x : OracleComp oSpec α) :
• @[reducible] def spec₁ (M₁ : Type) : ProtocolSpec 1
• @[reducible] def spec₂ (M₂ : Type) : ProtocolSpec 1
• theorem append_input (ctx : S₁ × W₁) :
• theorem append_output (st : (P₁.append P₂).PrvState (Fin.last (1 + 1))) :
• theorem append_perfectCompleteness_of_proverFactorization
• theorem append_perfectCompleteness_oneMsg
• theorem append_runToRound_one :
• theorem append_run_components :
• theorem append_run_raw :
• theorem append_sendMessage_boundary (st : (P₁.append P₂).PrvState (Fin.castSucc 1)) :
• theorem append_sendMessage_left (st : (P₁.append P₂).PrvState (Fin.castSucc 0)) :
• theorem bridge_c {α : Type} (X : OracleComp oSpec α) :
• theorem bridge_d {M α : Type} (X : OracleComp oSpec α) :
• theorem hfact_oneMsg
• theorem oneMsg_run_raw {S W S' W' M : Type}
• theorem processRound_one_eq
• theorem run_pure_verifier
• theorem transcript_align (y₁ : M₁) (y₂ : M₂) :

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)

---

📋 **Additional Analysis**

The diff introduces a new file AppendOneMsg.lean and modifies several existing files. Overall it is a substantial addition that advances the formalization goals. However, several violations of the ArkLib style guide and documentation standards are present. The most significant issues are excessive line lengths, missing docstrings for many theorems, and empty lines inside proofs. Several minor style issues are also noted. The duplication of theorems is intentional but should be documented more clearly. The review below lists the violations by category.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added an import of ArkLib.OracleReduction.Composition.Sequential.AppendOneMsg, making a new module available that likely provides definitions or theorems for appending a single message in sequential oracle-reduction compositions.
• ArkLib/OracleReduction/Composition/Sequential/Append.lean: The file adds two new theorems: run_pure_verifier, which states that for a reduction whose verifier is a pure function of statement and transcript, the Reduction.run monad collapses to a lift of the prover's run, providing a reusable lemma for pure-verifier reductions; and append_perfectCompleteness_of_proverFactorization, which proves that perfect completeness composes across Reduction.append under the assumptions of pure verifiers, a prover-level simulated factorization hfact, and that R₂ is complete uniformly in the initial state (addressing a previous TODO by requiring completeness for all initial states, not just a fixed one). The latter theorem uses run_pure_verifier and the existing append_perfectCompleteness infrastructure.
• ArkLib/OracleReduction/Composition/Sequential/AppendOneMsg.lean: This new file AppendOneMsg.lean proves that perfect completeness composes across Reduction.append for single-message protocols with pure verifiers, removing the factorization hypothesis left open by the generic Reduction.append_perfectCompleteness_of_proverFactorization in Append.lean. It introduces the concrete protocol specs spec₁ and spec₂ (each a single-round .P_to_V followed by a message type), and establishes the main results append_perfectCompleteness_oneMsg (the unconditional composition theorem) and hfact_oneMsg (the prover-level simulated factorization (P₁.append P₂).run equals P₁.run then P₂.run). Supporting this are: component-wise equation lemmas (append_sendMessage_left, append_sendMessage_boundary, append_input, append_output) breaking the appended prover's operations into those of P₁ and P₂; a run decomposition append_run_components expressing the appended run in terms of per-component operations under direct lifts; transcript_align showing the nested transcript concatenation equals the ++ₜ of the two single-message transcripts; bridge lemmas (bridge_c, bridge_d) proving that simulating a directly-lifted oSpec computation through the composed challenge-sum QueryImpl equals simulating it through the lifted base implementation; and a local restatement append_perfectCompleteness_of_proverFactorization with the hfact hypothesis, used to derive the final unconditional theorem by supplying hfact_oneMsg.
• ArkLib/OracleReduction/Execution.lean: Added the theorem Prover.runToRound_succ (for i : Fin n, stmt, wit, prover) that states prover.runToRound i.succ stmt wit = prover.processRound i (prover.runToRound i.castSucc stmt wit). This provides a one-step unfolding of runToRound and is intended as a workhorse for collapsing concrete protocol executions round by round (e.g., in component completeness proofs). No sorry or admit were introduced.
• ArkLib/ProofSystem/Component/SendWitness.lean: This diff replaces a sorry placeholder in the reduction_completeness theorem with a complete proof. The proof uses simp, rw, and refine with two subgoals: the first shows that the probability of failure is zero by invoking probOutput_eq_zero_of_not_mem_support and simulateQ_pure, and the second shows that every element of the support corresponds to a valid input by rewriting through StateT.run_pure and map_pure. No other changes are made in the file.

---

Last updated: 2026-07-11 01:52 UTC.