feat(Append): construct the challenge-oracle SubSpec embeddings

[Abraxas1010]

Fills the two sorry'd instances in Composition/Sequential/Append.lean:

instance : [(pSpec₁).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ
instance : [(pSpec₂).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ

Construction. A SubSpec instance is a lens plus a coherent monadLift. Here the lens is:

• onQuery: ChallengeIdx.inl/.inr on the oracle index (the embeddings already in SeqCompose.lean), identity on the trivial Unit query;
• onResponse: transport along the challenge-type equalities Challenge_inl / Challenge_inr — two new lemmas proved by Fin.append_left/Fin.append_right (these are the equalities sketched in the commented-out challengeOracleInterface_append_* lemmas in SeqCompose.lean).

monadLift is spelled directly in lens form, so the coherence field liftM_eq_lift holds by rfl — per the design note in VCVio/OracleComp/Coercions/SubSpec.lean this keeps lifted queries transparent to isDefEq, which matters for the downstream append_run factorization work.

Motivation. These instances are prerequisites for stating/proving Prover.append_run and the append security theorems (they let a component prover's challenge queries be replayed inside the appended protocol). Part of the sequential-composition thread discussed on #627; smallest complete unit, nothing else touched.

Checks. lake build of the module and all importers (Sequential.General, Security/CoordinateWiseSpecialSoundness/Composition, RingSwitching/*) passes; sorry delta −2; no new axioms.

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

[github-actions]

🤖 PR Summary

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

Mathematical Formalization

• Challenge type equalities: Proved two new theorems ProtocolSpec.Challenge_inl and ProtocolSpec.Challenge_inr in ArkLib/OracleReduction/Composition/Sequential/Append.lean. These establish that for the appended protocol pSpec₁ ++ₚ pSpec₂, the challenge type at a left-embedded index (ChallengeIdx.inl) equals pSpec₁'s challenge type, and symmetrically for ChallengeIdx.inr. Proofs use Fin.append_left/Fin.append_right.

• SubSpec embeddings: Implemented the two previously sorry-d instances:

  • [(pSpec₁).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ
  • [(pSpec₂).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ

  Construction details:

  • onQuery uses ChallengeIdx.inl/.inr on the oracle index, identity on Unit query
  • onResponse transports responses via cast using the new Challenge_inl/Challenge_inr theorems
  • monadLift is spelled in direct lens form, making liftM_eq_lift hold by rfl per the design in SubSpec.lean

Proof Completion (sorries removed)

• Removed 2 sorrys: The two placeholder instances in Append.lean are now fully constructed, marking the completion of oracle embedding for sequential composition. Sorry delta: -2.
• No new axioms introduced.

Motivation / Context

• These embeddings are prerequisites for the Prover.append_run factorization and the sequential-composition security theorems, part of the thread from issue Design: the BCS transform as a change of oracle implementation (QueryImpl), with a staged opening plan #627.
• They allow a component prover's challenge queries to be replayed inside the appended protocol.

Infrastructure / CI

• lake build passes for the module and all importers: Sequential.General, Security/CoordinateWiseSpecialSoundness/Composition, RingSwitching/*.
• No other files are modified; the change is self-contained to one file.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	29
❌ Lines Removed	2

---

Lean Declarations

✏️ Added: 2 declaration(s)

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

• theorem _root_.ProtocolSpec.Challenge_inl (i : pSpec₁.ChallengeIdx) :
• theorem _root_.ProtocolSpec.Challenge_inr (i : pSpec₂.ChallengeIdx) :

---

sorry Tracking

✅ Removed: 2 `sorry`(s)

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

• def StateFunction.append (L323)
• def StateFunction.append (L324)

---

📋 **Additional Analysis**

The diff is being reviewed against the ArkLib contribution guidelines. The changes implement embedding instances for sequential protocol composition, which aligns with the project's roadmap and style guide.

Key observations:

• Title format adheres to <type>(<scope>): <subject> using feat: the diff adds new feature instances.
• The diff uses imperative present tense in the commit subject (implied by the PR, not shown).
• The code uses backtick-quoted Lean names, sectioning comments with /-!, and follows naming conventions (Challenge_inl, Challenge_inr as snake_case theorems).
• File header, imports, and spacing follow the style guide.
• The diff adds two instance definitions and two theorem definitions; no deprecations or style violations are present.
• The diff does not touch files marked as active formalizations or address open issues directly; it is a new feature for sequential composition.
• No blueprint references appear in the diff, but the feature is small enough that a blueprint may not be required per guidelines.
• No citation or licensing issues in the diff.

No violations of the style guide or contribution guidelines are detected.

---

📄 **Per-File Summaries**

• ArkLib/OracleReduction/Composition/Sequential/Append.lean: This diff replaces two sorry-filled instance declarations with two new theorems and two properly implemented instances. The theorems ProtocolSpec.Challenge_inl and ProtocolSpec.Challenge_inr compute the challenge type of an appended protocol at a left- or right-embedded index, equating it to the original left or right protocol's challenge type via Fin.append_left/Fin.append_right. The new instance embeddings [(pSpec₁).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ and [(pSpec₂).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ now provide concrete monadLift, onQuery, and onResponse fields that use ChallengeIdx.inl/ChallengeIdx.inr and transport responses using cast with the corresponding Challenge_inl/Challenge_inr theorem. This eliminates the previously stubbed-out sorrys, making oracle embedding for sequential composition fully constructive.

---

Last updated: 2026-07-10 20:21 UTC.