feat(opening): expose response splicing

ComplexityTheory/ProofComplexity/CanonicalOpening/FiniteStrategy.lean

@@ -29,6 +29,65 @@ end OpeningStepResult
 
 namespace CanonicalOpening
 
+/-- A verifier either audits one global response or opens one local response. -/
+inductive GlobalLocalChallenge (Index : Type) where
+  /-- Audit the response intended to establish the global relation. -/
+  | global
+  /-- Open the response at one challenged local index. -/
+  | opening (index : Index)
+
+/--
+A one-round strategy commits before the challenge, then supplies separate
+global and local responses. The local response function is semantic strategy
+state, not a claim that its entire table is transmitted.
+-/
+structure SeparatedResponseStrategy
+    (Commitment GlobalResponse Index LocalResponse : Type) where
+  /-- The message fixed before the verifier reveals its challenge. -/
+  commitment : Commitment
+  /-- The response used on the global audit branch. -/
+  globalResponse : GlobalResponse
+  /-- The response used at each local opening branch. -/
+  localResponse : Index → LocalResponse
+
+namespace SeparatedResponseStrategy
+
+/-- Run the branch selected by a global-or-local challenge. -/
+def run
+    {Commitment GlobalResponse Index LocalResponse ChildClaim : Type}
+    (global : Commitment → GlobalResponse → OpeningStepResult ChildClaim)
+    (localStep : Commitment → Index → LocalResponse → OpeningStepResult ChildClaim)
+    (strategy : SeparatedResponseStrategy Commitment GlobalResponse Index LocalResponse) :
+    GlobalLocalChallenge Index → OpeningStepResult ChildClaim
+  | .global => global strategy.commitment strategy.globalResponse
+  | .opening index => localStep strategy.commitment index (strategy.localResponse index)
+
+/--
+A separated strategy survives every challenge exactly when its global response
+and every independently selectable local response are safe. This equivalence
+is the response-splicing seam that a real commitment mechanism must close.
+-/
+theorem safeForEveryChallenge_iff
+    {Commitment GlobalResponse Index LocalResponse ChildClaim : Type}
+    (childTrue : ChildClaim → Bool)
+    (global : Commitment → GlobalResponse → OpeningStepResult ChildClaim)
+    (localStep : Commitment → Index → LocalResponse → OpeningStepResult ChildClaim)
+    (strategy : SeparatedResponseStrategy Commitment GlobalResponse Index LocalResponse) :
+    (∀ challenge, (strategy.run global localStep challenge).isSafe childTrue = true) ↔
+      (global strategy.commitment strategy.globalResponse).isSafe childTrue = true ∧
+        ∀ index,
+          (localStep strategy.commitment index (strategy.localResponse index)).isSafe childTrue =
+            true := by
+  constructor
+  · intro hSafe
+    exact ⟨hSafe .global, fun index => hSafe (.opening index)⟩
+  · rintro ⟨hGlobal, hLocal⟩ challenge
+    cases challenge with
+    | global => exact hGlobal
+    | opening index => exact hLocal index
+
+end SeparatedResponseStrategy
+
 /--
 One fixed proof survives every challenge without rejection or a false child.
 This proposition states the semantic contract before finite enumeration.