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.

[Abraxas1010]

Rebased onto current main (66da7fa6).

Why: this branch was still pinned to leanprover/lean4:v4.30.0 while main has moved to v4.31.0. GitHub reported the PR mergeable and all checks green, but that CI run is from 11 July against 4.30-era main — it was no longer evidence about the current tree. Rebasing makes the green mean something again.

The rebase was textually clean, and no proof needed repair. Full lake build ArkLib green locally at Lean 4.31 (4122 jobs), no new sorry.

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

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Added two theorems to ArkLib/OracleReduction/Composition/Sequential/Append.lean:

  • Reduction.run_pure_verifier: an equational characterization of Reduction.run when the verifier is a pure function f of statement and transcript. The theorem states:
    (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 a pattern anticipated by the existing support_run_pure_verifier premise, making it directly reusable.

  • Reduction.append_perfectCompleteness_of_proverFactorization: proves that perfect completeness composes across Reduction.append under three assumptions:

    • both verifiers are pure (hf₁, hf₂),
    • the appended prover factorizes into the two sequential prover runs (hfact, a prover-level hypothesis that is the distributional counterpart of Prover.append_run;
      this avoids a pointwise false run-level factorization), and
    • the second reduction (R₂) is perfectly complete for every initial state (quantified over init'), not just a fixed init — necessary because the appended run hands R₂ whatever state R₁'s prover leaves.

• No sorry or admit appear in the added code; #print axioms reports only [propext, Classical.choice, Quot.sound].

• Architectural significance: This is the first in a planned sequence of composition units (context from issue Design: the BCS transform as a change of oracle implementation (QueryImpl), with a staged opening plan #627). The uniform init quantification resolves a prior TODO about the condition under which sequential completeness composes. The theorem is immediately usable because the prover-level factorization hypothesis is a separate concern (proven for the 1‑message ++ 1‑message case in a follow‑up PR).

• Build impact: Only Append.lean is changed; the file itself and all its importers (Sequential.General, CoordinateWiseSpecialSoundness/Composition, RingSwitching/*) build cleanly.

---

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**

The diff introduces a new theorem run_pure_verifier and a new theorem append_perfectCompleteness_of_proverFactorization to Append.lean. The review checks compliance with the provided ArkLib contribution guidelines, focusing on style, naming, documentation, and the presence of necessary citations. There are three issues to address: a typo in the deprecation date format in the guidelines (not in the code but noted for awareness), a missing ## References section (cosmetic as code body is not a module docstring), and an unused variable h₂ in h₁supp' (style/cleanliness). No findings related to the specific formalization (blueprint, roadmap, active formalizations) are present as the diff is a general theorem addition. The code generally adheres to guidelines but needs minor cleanup.

---

📄 **Per-File Summaries**

• ArkLib/OracleReduction/Composition/Sequential/Append.lean: The diff adds two theorems to Append.lean. The first, run_pure_verifier, provides a simplified equational characterization of Reduction.run when the verifier is a pure function (given by f and hf): the run collapses to the prover's run followed by applying f to the generated transcript. The second, append_perfectCompleteness_of_proverFactorization, proves that perfect completeness composes across Reduction.append under the assumptions that both verifiers are pure (hf₁,hf₂), the appended prover factorizes into the two sequential prover runs (hfact), and the second reduction is perfectly complete for every initial state (h₂ quantified over init'). No sorry or admit appear in the added code.

---

Last updated: 2026-07-28 14:55 UTC.

[Abraxas1010]

Note on the red checks: both failures are pre-existing on main, not from this PR.

CI — the Lean build is green. lake build ArkLib completes (✔ Built ArkLib) with no errors; the job then fails in ./scripts/validate.sh on:

Errors:
  - Paper page without matching BibTeX key: docs/kb/papers/NOZ26.md

docs/kb/papers/NOZ26.md is on main and was added upstream in June; this branch adds no docs/kb files. The same error reproduces byte-for-byte on unrelated open PRs — e.g. #574 (guruswami-sudan), whose CI ran after this one.

Build and Deploy Website to GitHub Pages — fails on the blueprint declaration check:

Fold.folding_preserves_listdecoding_base is missing.
Fold.folding_preserves_listdecoding_bound is missing.
Fold.folding_preserves_listdecoding_base_ne_subset is missing.
WhirIOP.whir_rbr_soundness is missing.

This workflow has failed on every run for at least the past two weeks, across every contributor's branch (#574, #610, #503, ElijahVlasov/*, tr/*, …). None of those declarations are touched here.

Logs: CI run · Pages run

Happy to open a separate fix for the NOZ26 BibTeX entry if that would help unblock CI repo-wide.