fix[Hachi]: reconcile openCore with branch's batchPackage API after main merge

The merge of main brought in the Verified-zkEVM#650 skeleton's Composition.lean (which
calls batchPackage with hq2 : 2*b ≤ q+1 and hb : b-1 ≤ bound) but kept this
branch's sorry-free Batch.lean, whose batchPackage instead takes
hn : n₀ ≤ 2^m₁ (shortness asserted directly in relBatched rather than
derived from H₀ ≡ 0). The two disagreed, breaking the build.

Adapt openCore/openingChain/hachi_iteration_coordinateWiseSpecialSound back
to the hn API and restore the explicit (b := b) in the theorem (b is no
longer pinned by a hypothesis). Also drop mem_relLiftE_of_relBatchedE from
the module header's sorry inventory: it is now proved sorry-free
(#print axioms: propext, Classical.choice, Quot.sound only).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: ErVinuelas

ArkLib/Commitments/Functional/Hachi/Composition.lean

@@ -100,9 +100,8 @@ seam a home for the `w̃`-commitment's weak-binding break (design G1; `E` abstra
 `coordinateWiseSpecialSound_of_mkWitness_scalar` (`ScalarRound.lean`, consumed only by future
 proofs). *Escape threading* (F2.0): `quadEval_coordinateWiseSpecialSound_withEscape`.
 *Per-link math*: the F2 index bookkeeping (`rlinStmt`/`unstack`/`mem_relOutE_of_relRlinE`),
-Lemma 9 (`lift_coordinateWiseSpecialSound`), the F5 encodings (`Constraints.lean`), the
-un-batching (`mem_relLiftE_of_relBatchedE`), corrected Lemma 10
-(`zeroCheck_coordinateWiseSpecialSound`), the sum-to-point bridge, Lemma 11
+Lemma 9 (`lift_coordinateWiseSpecialSound`), the F5 encodings (`Constraints.lean`), corrected
+Lemma 10 (`zeroCheck_coordinateWiseSpecialSound`), the sum-to-point bridge, Lemma 11
 (`round_coordinateWiseSpecialSound`), F8 (`finalEval_coordinateWiseSpecialSound` + the
 `finalCheck` encoding), G2 (`partialEval_coordinateWiseSpecialSound` + its encoding defs), G3
 (`handoff_coordinateWiseSpecialSound` + `traceCheck`/`toNextQuadEvalStatement`/`hatEval`).
@@ -234,7 +233,7 @@ noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
     (φF : ZMod q →+* F)
-    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1) (hb : b - 1 ≤ γ) :
+    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hn : n₀ ≤ 2 ^ m₁) :
     CWSSPackage init impl
       (PolyEvalStatement 𝓜(q, α) innerRows messageDigits outerRows innerDigits dRows m r)
       (QuadEvalWitness 𝓜(q, α) innerRows (2 ^ m) messageDigits (2 ^ r) innerDigits ⊕ E)
@@ -250,7 +249,7 @@ noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT
   evalChainE (b := b) (γ := γ) init impl hq5 hκ hτ K.esc ▷
     rlinPackage (zDigits := zDigits) 𝓜(q, α) init impl (b : ZMod q) ω γ K.esc ▷
     liftPackage 𝓜(q, α) γ ρBound K φF init impl hd ▷
-    batchPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b hq2 hb ▷
+    batchPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b hn ▷
     zeroCheckPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b ▷
     sumcheckBridgePackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b
 
@@ -272,7 +271,7 @@ noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (Sta
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
     (φF : ZMod q →+* F)
-    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1) (hb : b - 1 ≤ γ)
+    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hn : n₀ ≤ 2 ^ m₁)
     (zpow : Fin (2 ^ κ) → F)
     (Φ' : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ']
     {innerRows' messageDigits' outerRows' innerDigits' dRows' m' r' : ℕ}
@@ -300,7 +299,7 @@ noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (Sta
           roundsSpec F b (mLow + κ)) ++ₚ pSpecFinalEval F).Challenge i) :=
     ProtocolSpec.instSampleableTypeChallengeAppend (h₁ := i₁)
       (h₂ := instSampleableTypeChallengePSpecFinalEval)
-  (((openCore (m₀ := mLow + κ) (m₁ := m₁) init impl hq5 hκ hτ K φF hd hq2 hb).toGuarded.append
+  (((openCore (m₀ := mLow + κ) (m₁ := m₁) init impl hq5 hκ hτ K φF hd hn).toGuarded.append
       (roundsChain 𝓜(q, α) (mLow + κ) m₁ γ ρBound b init impl K φF (mLow + κ))
       (roundsChain_relIn 𝓜(q, α) (mLow + κ) m₁ γ ρBound b init impl K φF
         (mLow + κ)).symm).append
@@ -322,24 +321,24 @@ theorem hachi_iteration_coordinateWiseSpecialSound (init : ProbComp σ)
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
     (φF : ZMod q →+* F)
-    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1) (hb : b - 1 ≤ γ)
+    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hn : n₀ ≤ 2 ^ m₁)
     (zpow : Fin (2 ^ κ) → F)
     (Φ' : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ']
     {innerRows' messageDigits' outerRows' innerDigits' dRows' m' r' : ℕ}
     (pp' : Hachi.PublicParamsD Φ' innerRows' (2 ^ m') messageDigits' outerRows' (2 ^ r')
       innerDigits' dRows')
     (reinterpretCom : K.TCom → Commitment Φ' outerRows')
     (base' : ZMod q) (βSq' γ' κ' : ℕ) :
-    ((openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ
-        hτ K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq'
+    ((openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) (b := b) init impl hq5 hκ
+        hτ K φF hd hn zpow Φ' pp' reinterpretCom base' βSq'
         γ' κ')).verifier.coordinateWiseSpecialSound init impl
-      (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ hτ
-        K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq' γ' κ').struct
+      (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) (b := b) init impl
+        hq5 hκ hτ K φF hd hn zpow Φ' pp' reinterpretCom base' βSq' γ' κ').struct
       (relPolyEvalE 𝓜(q, α) (b : ZMod q)
         (quadEvalBetaSq γ b zDigits ((𝓜(q, α)).φ.natDegree) m messageDigits) γ (2 * ω) K.esc)
       (relInE Φ' base' βSq' γ' κ' K.esc) :=
-  (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ hτ
-    K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq' γ' κ').isCWSS
+  (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) (b := b) init impl hq5 hκ hτ
+    K φF hd hn zpow Φ' pp' reinterpretCom base' βSq' γ' κ').isCWSS
 
 end OpeningChain