fix(ProtocolSpec): prove the partial-transcript splitters and index equivalences for sequential composition (6 sorries removed)

[Abraxas1010]

Summary

Removes all six sorrys from ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean:

1. Transcript.fst / Transcript.snd (3 sorries) — the partial-transcript splitters for an appended protocol. Redefined uniformly (no if-split on k ≤ m) as honest casts along two new type-transport lemmas:

   • append_Type_castAdd : (pSpec₁ ++ₚ pSpec₂).Type (Fin.castAdd n i) = pSpec₁.Type i
   • append_Type_natAdd : (pSpec₁ ++ₚ pSpec₂).Type (Fin.natAdd m i) = pSpec₂.Type i

   Keying the transport on castAdd/natAdd keeps Nat subtraction out of the types; the min k m and k - m bounds are discharged by omega at the index level. The signatures are unchanged, so existing consumers (e.g. the StateFunction clauses in Composition/Sequential/Append.lean) are unaffected.

2. FullTranscript.rtake_append_right (1 sorry) — the cast residue after rw! (castMode := .all) (⋯ ▸ cast ⋯ (T' i) = cast ⋯ (T' i)) dissolves through HEq: both sides are transports of T' i, so eq_of_heq + eqRec_heq/cast_heq closes it.

3. seqComposeChallengeEquiv.left_inv / seqComposeMessageEquiv.left_inv (2 sorries) — discharged with the existing Fin.splitSum_embedSum via rw! (castMode := .all), then rfl (structure eta collapses the rebuilt Sigma/Subtype pair).

Motivation

The partial-transcript splitters are load-bearing for sequential composition: the round-by-round StateFunction soundness clauses and any Prover.append_run-style run-assembly statement are phrased over Transcript.fst/.snd. As long as they were sorry, every downstream statement mentioning them was building on unproved infrastructure. The two index Equivs similarly complete the challenge/message index bookkeeping for seqCompose.

Verification

• lake build ArkLib — full library, warning-free at the changed file (pre-existing linter warnings elsewhere untouched).
• grep -c sorry ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean → 0.
• No signature changes; no downstream proof required adjustment.

[github-actions]

🤖 PR Summary

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

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	33
❌ Lines Removed	17

---

Lean Declarations

✏️ Added: 2 declaration(s)

ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean (2)

• theorem append_Type_castAdd (i : Fin m) :
• theorem append_Type_natAdd (i : Fin n) :

---

sorry Tracking

✅ Removed: 6 `sorry`(s)

ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean (6)

• def fst (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₁.Transcript ⟨min k m, by omega⟩ (L122)
• def fst (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₁.Transcript ⟨min k m, by omega⟩ (L125)
• def seqComposeChallengeEquiv {m : ℕ} {n : Fin m → ℕ} (pSpec : ∀ i, ProtocolSpec (n i)) : (L500)
• def seqComposeMessageEquiv {m : ℕ} {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)} : (L524)
• def snd (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₂.Transcript ⟨k - m, by omega⟩ (L133)
• theorem rtake_append_right (T : FullTranscript pSpec₁) (T' : FullTranscript pSpec₂) : (L189)

---

📋 **Additional Analysis**

The diff introduces new transport lemmas, fills in previously stubbed Transcript.fst and snd, patches a rtake_append_right proof, and fixes left_inv proofs for two equivalence definitions. The changes are generally well-aligned with the project's style guide, with a few minor formatting issues.

---

📄 **Per-File Summaries**

• ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean: The diff completes two previously sorry-ridden definitions in Transcript (fst and snd) by providing concrete implementations that use the new append_Type_castAdd and append_Type_natAdd lemmas, respectively, along with a cast to type-transport the underlying transcript entry. It adds those two new lemmas about the Type field of a concatenated spec at Fin.castAdd and Fin.natAdd indices. It also repairs the rtake_append_right theorem in the FullTranscript section, replacing a sorry with an equality of heterogeneous equalities (eq_of_heq with eqRec_heq/cast_heq). Finally, it fills in the left_inv proofs of seqComposeChallengeEquiv and seqComposeMessageEquiv, which were previously incomplete after a simp, by rewriting with Fin.splitSum_embedSum and then rfl.

---

Last updated: 2026-07-12 02:25 UTC.

[alexanderlhicks]

Thank you!