feat(Append): completeness composition under init-uniformity + run_pure_verifier

[Abraxas1010]

First of the composition units discussed on #627 (the milestone comment there has the full context).

Adds two theorems to the Security section of Composition/Sequential/Append.lean, alongside (not replacing) the open general append_completeness:

1. Reduction.run_pure_verifier — for a reduction whose verifier is a pure function f of statement and transcript: (R.run stmt wit).run = liftM (R.prover.run stmt wit) >>= fun r => pure (some ((r.1, r.2), f stmt r.1)). This is the run characterization that the existing support_run_pure_verifier premise pattern suggests, factored out for reuse.

2. Reduction.append_perfectCompleteness_of_proverFactorization — perfect completeness composes across append given (a) pure verifiers, (b) the prover-level simulated factorization as a hypothesis (the distributional shadow of the open Prover.append_run — so this theorem is usable immediately, and the factorization can land separately; we have it proven for the 1-message ++ 1-message case, follow-up PR), and (c) the answer to this section's TODO ("when do these theorems hold?"): R₂'s completeness quantified over all initial states. The appended run hands R₂ whatever state R₁'s prover left, so a fixed-init premise cannot apply — and component completeness proofs (e.g. feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631's SendWitness) already satisfy the uniform form since they hold for arbitrary init/impl.

Design note recorded in the docstrings: a run-level factorization through R₂.run is false pointwise — the appended verifier chains V₁'s output statement while the appended prover chains P₁'s output statement, and these agree only on honest supports — which is why the hypothesis is prover-level.

Checks: no sorry; #print axioms = [propext, Classical.choice, Quot.sound]; the module and all importers (Sequential.General, CoordinateWiseSpecialSoundness/Composition, RingSwitching/*) build.

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

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Adds two theorems to the Security section of Composition/Sequential/Append.lean (the existing append_completeness remains):

  1. Reduction.run_pure_verifier – For a reduction whose verifier is a pure function f: (R.run stmt wit).run = liftM (R.prover.run stmt wit) >>= fun r => pure (some ((r.1, r.2), f stmt r.1)). This factors out the run characterization that the support_run_pure_verifier premise pattern suggests, making it reusable.
  2. Reduction.append_perfectCompleteness_of_proverFactorization – Proves that perfect completeness composes across append under three hypotheses:
     • (a) Both verifiers are pure (hf₁, hf₂),
     • (b) A prover-level simulated factorization (hfact) – the distributional analogue of Prover.append_run (proven for the 1‑message + 1‑message case; a follow-up PR will generalize),
     • (c) R₂’s completeness must hold for all initial states (because the appended run feeds R₂ the state left by R₁’s prover). Resolves a longstanding TODO (“when do these theorems hold?”).

• A design note in the docstring explains why a run‑level factorization through R₂.run is false pointwise: the appended verifier chains V₁’s output statement while the appended prover chains P₁’s output statement, and these agree only on honest supports. Hence the hypothesis is stated at the prover level.

• No sorry or admit are introduced; #print axioms remains [propext, Classical.choice, Quot.sound].

Context and Dependencies

• This is the first of the composition units discussed on issue Design: the BCS transform as a change of oracle implementation (QueryImpl), with a staged opening plan #627. The component completeness proofs (e.g. feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631’s SendWitness) already satisfy the uniform‑init form required by (c).
• The module itself builds, and all listed importers (Sequential.General, CoordinateWiseSpecialSoundness/Composition, RingSwitching/*) build.
• No infrastructure, CI, documentation, or refactoring changes are included.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	150
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 2 declaration(s)

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

• theorem append_perfectCompleteness_of_proverFactorization
• theorem run_pure_verifier

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

• Naming Conventions: No violations. Theorem names use snake_case (run_pure_verifier, append_perfectCompleteness_of_proverFactorization). Variable names follow conventions.
• Syntax and Formatting:
  • Line length: Multiple lines exceed 100 characters. Notable examples include the hfact hypothesis argument, the StateT.run lines after hfact, and the long simp only statements. These should be broken to stay under the limit.
  • Empty lines inside definitions: The proof of append_perfectCompleteness_of_proverFactorization contains blank lines between comment blocks and subsequent have statements (e.g., after -- Composed-run characterization and -- Extract stage facts). The style guide advises against empty lines inside proofs/definitions.
  • Parentheses: Heavy use of parentheses is present, especially in the hfact hypothesis and nested StateT.run expressions. While sometimes necessary, they could be reduced where possible to match the guideline to avoid parentheses.
• Documentation: Docstrings are present for both added theorems and follow the /-- ... -/ format. No issues noted.
• Other: The diff correctly uses fun x ↦ (not λ x,), places by at the end of the preceding line, and uses simp appropriately. No violations of variable conventions, import grouping, or citation standards are observed from the diff alone.

---

📄 **Per-File Summaries**

• ArkLib/OracleReduction/Composition/Sequential/Append.lean: 添加了两个定理：run_pure_verifier 将具有纯验证器的 reduction 的运行简化为 prover 的运行加上纯函数结果，可重用；append_perfectCompleteness_of_proverFactorization 在纯验证器假设（hf₁, hf₂）和 prover 级别的因子分解条件（hfact）下，证明了 append 后的 reduction 的 perfectCompleteness，解决了之前的一个 TODO。无 sorry 或 admit。

---

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