refactor(Hachi/CWSS): cwss packages with escape

ArkLib.lean

@@ -3,32 +3,32 @@ import ArkLib.Commitments.Functional.Basic
 import ArkLib.Commitments.Functional.Hachi
 import ArkLib.Commitments.Functional.Hachi.Commitment
 import ArkLib.Commitments.Functional.Hachi.Composition
-import ArkLib.Commitments.Functional.Hachi.Escape
 import ArkLib.Commitments.Functional.Hachi.EvalSplit
-import ArkLib.Commitments.Functional.Hachi.Gadget
 import ArkLib.Commitments.Functional.Hachi.Gadget.Basic
+import ArkLib.Commitments.Functional.Hachi.Gadget.Core
 import ArkLib.Commitments.Functional.Hachi.Gadget.Norms
-import ArkLib.Commitments.Functional.Hachi.InnerOuter
 import ArkLib.Commitments.Functional.Hachi.InnerOuter.Arithmetic
+import ArkLib.Commitments.Functional.Hachi.InnerOuter.Basic
 import ArkLib.Commitments.Functional.Hachi.InnerOuter.Correctness
 import ArkLib.Commitments.Functional.Hachi.InnerOuter.Scheme
 import ArkLib.Commitments.Functional.Hachi.InnerOuter.Security
-import ArkLib.Commitments.Functional.Hachi.QuadEval
+import ArkLib.Commitments.Functional.Hachi.QuadEval.Basic
 import ArkLib.Commitments.Functional.Hachi.QuadEval.Bridge
 import ArkLib.Commitments.Functional.Hachi.QuadEval.Gadgets
 import ArkLib.Commitments.Functional.Hachi.QuadEval.Reduction
 import ArkLib.Commitments.Functional.Hachi.QuadEval.Soundness
+import ArkLib.Commitments.Functional.Hachi.Recursion.Basic
 import ArkLib.Commitments.Functional.Hachi.Recursion.PartialEval
 import ArkLib.Commitments.Functional.Hachi.Recursion.TraceHandoff
 import ArkLib.Commitments.Functional.Hachi.Recursion.ZBatchBridge
-import ArkLib.Commitments.Functional.Hachi.RingSwitch
+import ArkLib.Commitments.Functional.Hachi.RingSwitch.Basic
 import ArkLib.Commitments.Functional.Hachi.RingSwitch.Reduction
 import ArkLib.Commitments.Functional.Hachi.RingSwitch.Rlin
-import ArkLib.Commitments.Functional.Hachi.Sumcheck
+import ArkLib.Commitments.Functional.Hachi.Sumcheck.Basic
 import ArkLib.Commitments.Functional.Hachi.Sumcheck.Bridge
 import ArkLib.Commitments.Functional.Hachi.Sumcheck.FinalEval
 import ArkLib.Commitments.Functional.Hachi.Sumcheck.Rounds
-import ArkLib.Commitments.Functional.Hachi.ZeroCheck
+import ArkLib.Commitments.Functional.Hachi.ZeroCheck.Basic
 import ArkLib.Commitments.Functional.Hachi.ZeroCheck.Batch
 import ArkLib.Commitments.Functional.Hachi.ZeroCheck.Constraints
 import ArkLib.Commitments.Functional.Hachi.ZeroCheck.Reduction

ArkLib/Commitments/Functional/Hachi.lean

@@ -24,11 +24,11 @@ subprotocols and the completeness layer — the honest-prover `opening` (`hachi.
 
 ## Folder structure
 
-The folder `Hachi/` is organized by paper section, each subfolder carrying an umbrella `.lean`
-re-export next to it (as this file does for the whole folder):
+The folder `Hachi/` is organized by paper section. Each subfolder carries a `Basic.lean`
+umbrella re-export inside the folder (as this file does for the whole Hachi development):
 
 * `Gadget/` (§2.1) — the base-`b` Ajtai gadget matrix `G` and its digit-decomposition inverse
-  `G⁻¹` (`Basic`), with centered `ℓ∞` / `ℓ₂²` norm bounds for both directions (`Norms`).
+  `G⁻¹` (`Core`), with centered `ℓ∞` / `ℓ₂²` norm bounds for both directions (`Norms`).
 * `EvalSplit.lean` (§4, Eq. (12)) — multilinear evaluation as the vector–matrix–vector product
   `mb(xl) ⬝ᵥ (toMatrix p *ᵥ mb(xh))`; kept top-level because the future §3 packing head reuses
   it over the subfield.
@@ -38,10 +38,13 @@ re-export next to it (as this file does for the whole folder):
 * `QuadEval/` (§4.2, Figure 3) — the quadratic polynomial-evaluation reduction: gadget algebra
   (`Gadgets`), protocol data and relations (`Reduction`), Hachi Lemma 8 coordinate-wise special
   soundness (`Soundness`), and the zero-round polynomial-level bridge (`Bridge`).
-* `Composition.lean` — the CWSS composition home: the finished core
-  `evalChain = bridgePackage ▷ quadEvalPackage` with its certificate
-  `eval_coordinateWiseSpecialSound`; every further subprotocol lands as one more `CWSSPackage`
-  `▷`-appended there.
+* `RingSwitch/`, `ZeroCheck/`, and `Sumcheck/` (§4.3) — the lift, corrected zero-check, and
+  guarded sumcheck stages of the opening chain.
+* `Recursion/` (§4.5) — the partial-evaluation, packing, and trace-handoff adapters that close
+  one iteration at the next ring's plain `QuadEval.relIn` relation.
+* `Composition.lean` — the CWSS composition home: `evalChain = bridgePackage ▷
+  quadEvalPackage`, followed by the opening subprotocols. Packages expose one plain `relIn` /
+  `relOut` flow while a parallel escape set grows backwards at Figure 4 and `QuadEval`.
 * `Commitment.lean` — Hachi as a `Commitment.Scheme`: the multilinear eval-oracle interface and
   the honest `keygen` / `commit` (the opening `Proof` is a documented `sorry` pending the
   remaining subprotocols).

ArkLib/Commitments/Functional/Hachi/Commitment.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024-2026 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tobias Rothmann
 -/
-import ArkLib.Commitments.Functional.Hachi.QuadEval
+import ArkLib.Commitments.Functional.Hachi.QuadEval.Basic
 import ArkLib.Commitments.Functional.Basic
 
 /-!