# Repo Map

This repo is easiest to navigate by subtree, not by individual file name.
Many developments are paper-scoped and spread across several modules.

## Main Surfaces

```text
ArkLib/
  Data/               foundational math, coding theory, polynomials, probability, etc.
  Interaction/        typed prover, verifier, and reduction foundations
    Core/             rebuilt interaction core on PolyFun trees (staged migration)
  Relation/           claims, witness relations, and oracle data families
  OracleReduction/    core IOR abstractions and security theory
  Commitments/        commitments and opening arguments
  AGM/                algebraic group model representations
  ProofSystem/        protocol families and higher-level proofs
  ToMathlib/          local additions not upstreamed to Mathlib
  ToCompPoly/         local additions not upstreamed to CompPoly
ArkLibTest/           compile-time tests, acceptance cases, and runtime checks
blueprint/src/        blueprint sources and references.bib
docs/kb/             persistent paper, concept, audit, and query knowledge base
docs/wiki/            reference pages and conventions
docs/design/          interaction-layer design chapters and status
scripts/              repo utilities
home_page/            site assets and assembled website root
```

## Conceptual Layering

- `ArkLib/Interaction/` is the interaction layer, which is meant to replace the legacy layer
  ([README](../../README.md#two-layers)). Its `Reduction.lean` module
  is independent of oracle, probability, and legacy protocol semantics.
  `CompositionSoundness.lean` adds an exact append execution law and quantitative
  soundness under lawful distribution semantics, with an explicit admissibility-error variant.
  It quantifies over ordinary whole-tree prover strategies and uses the existing paired runner.
- `ArkLib/Interaction/Core/` is the rebuilt interaction core. It is being introduced in stages
  beside the existing interaction modules, which stay frozen until their clients move; Core
  imports none of them. Protocols are PolyFun `FreeM` trees whose roles come from the
  `plainSig` and `oracleSig` lenses (`Signature.lean`); `Protocol.lean` owns paths, views and
  nodes. `Reduction.lean` defines provers, verifiers, reductions and the public-coin sampler;
  `OracleVerifier.lean` adds oracle verifiers with routed input and message oracles;
  `Execution.lean` runs a verifier against an arbitrary prover and keeps rejection as a returned
  verdict. `Composition.lean` appends verifiers, provers and oracle routes. `Security/` holds
  completeness and soundness over adversary models, classical straight-line and transcript-only
  extraction, and round-by-round soundness and knowledge on cursor prefixes. Its acceptance
  tests live in `ArkLibTest/Interaction/Core/`.
- The descriptions below cover the frozen interaction modules outside `Core/`.
- `ArkLib/Interaction/Oracle/` refines generic type trees with public/oracle positions, keeps
  structural `BranchPath` separate from concrete `ExecutionPath` messages, and adds position-typed
  role/interface decorations plus the minimal decorated `Oracle.Protocol` bundle.
- `ProofSystem/Sumcheck/Interaction/Protocol.lean` defines the full interaction-layer sum-check tree,
  restricted verifier, and direct execution through `executeStrategiesCore`. Prover memory lives
  in ordinary strategy continuations. `ProtocolSoundness.lean` proves the final output oracle relation bound;
  `MultivariateSoundness.lean` supplies the one-round polynomial projection bound.
  `ProtocolCompleteness.lean` defines the honest strategy and proves support-level and
  probability-one completeness.
- `Interaction/Oracle/CoreRun.lean` offers `executeStrategiesCore` for ready prover strategies.
  `executeCore` runs reduction setup and delegates to that entry point. Both retain the actual
  input behavior, path and outputs for closing; `executeCore_eq_execute` preserves the existing
  execution law for reduction clients. `Access.lean` supplies the common virtual-view preservation
  law when a new message extends the available oracle signature.
- `Interaction/Oracle/Composition.lean` supplies a separate sequential execution combinator.
  Its explicit interface handoffs are not a substitute for a direct strategy execution theorem.
- `Interaction/Oracle/Security/` holds interaction-layer security. `RoundByRound.lean` defines
  ordinary round-by-round soundness on execution prefixes; `Soundness.lean` bounds the actual executor by the
  sum of the local challenge errors (`count * error` in the uniform case). `Knowledge.lean` defines
  witness-indexed knowledge certificates (`RoundExtractor`, `KnowledgeCertificate`);
  `KnowledgeAppend.lean` and `KnowledgeComposition.lean` compose them along dependent append.
  The `StateRestoration*.lean` modules prove state-restoration knowledge soundness for fixed-round
  public-coin protocols with bound `(Q + rounds.length) * error`, with variants for oracle outputs
  (`StateRestorationOracle`), pre-sampled private coins (`StateRestorationCoins`) and per-round
  errors (`StateRestorationBudget`). The measured forms are described under measured extraction
  below. `ProofSystem/Sumcheck/Interaction/RoundByRound.lean` is the interaction-layer Sumcheck client.
- `ArkLib/OracleReduction/` remains the conceptual center of the legacy reduction and security
  layer while protocol clients migrate. `FiatShamir/Basic.lean` owns the transform;
  `FiatShamir/Completeness.lean` adds fixed-table perfect completeness and shared lazy
  random-oracle completeness.
  Generic transcript projection and reconstruction equations live in `ProtocolSpec/Basic.lean`;
  round and optional-run factorization lemmas live in `Execution.lean`.
- `ArkLib/Relation/Basic.lean` is the neutral owner of claims, witness relations with an
  admissibility boundary, and oracle data families; it depends on no protocol tree. Likewise
  `ProofSystem/Sumcheck/Spec/PolynomialInterface.lean` owns the sum-check polynomial's
  evaluation-query interface, shared by the specification and the computational handler.
- `ArkLib/Data/`, `ArkLib/ToMathlib/`, and `ArkLib/ToCompPoly/` support the
  core with reusable definitions and lemmas.
- `ArkLib/Commitments/` and `ArkLib/ProofSystem/` build on top of those foundations.
- When changing a protocol subtree, read the local subtree plus one layer of imports toward
  `Data/` or `OracleReduction/` before making architectural edits.

## Where To Start By Task

- Extending foundational math or coding theory: start in `ArkLib/Data/`.
- Changing typed interaction or dependent reduction foundations: start in `ArkLib/Interaction/`.
  New interaction-layer work goes in `ArkLib/Interaction/Core/`; the modules beside it are frozen
  during the staged migration.
- Changing legacy reduction or security abstractions: start in `ArkLib/OracleReduction/`.
- Working on protocol statements or proofs: start in `ArkLib/ProofSystem/`.
- Updating commitment interfaces or concrete schemes: start in `ArkLib/Commitments/`
  (`Ordinary/` for plain commit-and-open schemes whose definition comes from the VCV-io
  `CommitmentScheme`, `Functional/` for commit-plus-oracle-evaluation schemes defined by
  ArkLib's own `Commitment.Scheme` in `ArkLib/Commitments/Functional/Basic.lean`).
- Moving reusable helper lemmas that ideally belong upstream: start in `ArkLib/ToMathlib/`,
  or `ArkLib/ToCompPoly/`, depending on the upstream project. Generic VCVio additions go upstream
  directly; ArkLib imports their public owner modules.
- Updating theory docs, references, or long-form exposition: start in `blueprint/src/`.
- Updating repository-local paper summaries, audits, or reference context: start in `docs/kb/`.

## Navigation Notes

- `ProofSystem/Spartan/` keeps its polynomial mathematics independent of both interaction layers.
  `Algebra/Layout.lean` embeds arbitrary R1CS sizes and recovers witnesses by restriction;
  `Context.lean` owns the retained public records. `Algebra/Identities.lean` defines the virtual
  polynomials, `Algebra/Computable.lean` constructs them with CompPoly, and
  `Algebra/Realization.lean` connects finite-table evaluation to their semantics. The
  `ZeroCheck/`, `Evaluation/` and `Batching/` folders pair each stage's `Relation.lean` with its
  `Reduction.lean`. `Sumcheck/First.lean` and `Sumcheck/Second.lean` lift the general Sumcheck
  protocol through executable virtual-polynomial lenses, preserving the original oracle tables and
  proving stage completeness and fixed-prefix errors `3 / |R|` and `2 / |R|`.
  The first verifier's query-bound theorem excludes evaluation of its virtual input polynomial.
  `WitnessAttachment.lean` sends the padded original witness, forwards scalar matrix queries,
  and extracts by restricting the actual sent table; its input relation is the original R1CS
  relation. It instantiates the shared `SendSingleWitness.Adapter` of
  `ProofSystem/Component/SendWitness.lean`. `Sumcheck/VirtualOracle.lean` evaluates the virtual
  polynomials by queries to the retained matrix and witness oracles, and `Terminal.lean` is the
  final oracle verifier. `Protocol.lean` composes the seven stages into `Spartan.oracleReduction`
  and proves `Spartan.perfectCompleteness` for the original R1CS relation. `Security.lean` proves
  `Spartan.knowledgeSoundness` with error `Spartan.totalError ℓ_m ℓ_n |R|`, which is
  `(4 * ℓ_m + 2 * ℓ_n + 1) / |R|` (`Error.lean`), through the executable
  `Spartan.straightlineExtractor`. `Basic.lean` imports `Security.lean`.
- `ProofSystem/Sumcheck/Impl/OracleProver.lean` provides the executable legacy honest prover,
  with exact refinement to `Spec.oracleReduction.prover` and preservation of the input polynomial
  oracle. `Impl/Representation.lean` and `Impl/Projection.lean` connect finite coefficient
  computations to the mathematical polynomial representations.
- Plonk's finite mathematics is independent of both execution layers.
  `ProofSystem/ConstraintSystem/Plonk.lean` owns gates, the prefix/private relation, and the
  wiring permutation whose cycles are exactly the variable fibers. Its generic cycle construction
  lives in `Data/Equiv/FiberCycle.lean`. `ProofSystem/Plonk/` groups each protocol stage into a
  subfolder (`Relation`, `Encoding`, `Accumulator`, `GrandProduct`, `Batch`, `Quotient`,
  `Assembly`), with `SendWitness.lean` at the top; it instantiates the shared
  `SendSingleWitness.Adapter` of `ProofSystem/Component/SendWitness.lean`.
  `Plonk/Relation/Basic.lean` connects variable and
  occurrence assignments, with public-occurrence coverage for reconstruction.
  `Plonk/Relation/Prepared.lean` prepends public equality rows, decodes private witnesses, and
  separates their baked-in constants into cleared selectors and an explicit public-input term.
  `Plonk/Encoding/Domain.lean` supplies injective evaluation nodes and disjoint coset labels.
  `Plonk/Encoding/Basic.lean` identifies occurrence columns with degree-bounded polynomials,
  proves the prepared gate and copy relation equivalence, and reconstructs private witnesses.
  `Plonk/Encoding/Computable.lean` refines the encoding through CompPoly coefficient arrays.
  `Plonk/Relation/PermutationFingerprint.lean` characterizes copy constraints by labeled product
  fingerprints, and `Plonk/Accumulator/` defines the cyclic numerator and denominator accumulators.
  `Plonk/Assembly/Reduction.lean` composes the wire reveal, grand product, batch and quotient zero
  test into one oracle reduction: `Plonk.Assembly.oracleReduction_completeness` has completeness
  error `3n / |F|` and `Plonk.Assembly.oracleVerifier_knowledgeSoundnessWith` has knowledge error
  `(7n - 3) / |F|`. `Plonk/Assembly/CircuitExtraction.lean` extracts the original circuit witness
  with error `(7(ℓ + n) - 3) / |F|` (`Plonk.Assembly.Circuit.oracleVerifier_knowledgeSoundnessWith`).
  Concrete cycle, satisfaction, and decoder checks live in
  `ArkLibTest/ProofSystem/Plonk/Relation.lean`;
  `ArkLibTest/ProofSystem/Plonk/Encoding.lean` checks order-four encoding over a prime field,
  including rejected gates, inconsistent copies, and incorrect public inputs.

- `ProofSystem/Plonk/GrandProduct/` formalizes the Plonk permutation grand product:
  a univariate accumulator `Z` over the multiplicative evaluation domain with `Z(1) = 1` and
  `Z(ωx) * Q(x) = Z(x) * N(x)`. `Data.lean` defines its executable polynomials and
  residuals; `Reduction.lean` defines the oracle reduction; `Completeness.lean` and `Security.lean`
  prove its completeness and round-by-round knowledge bounds.
  `ProofSystem/Plonk/Batch/` batches the three residuals through `GeneratorBatch` with
  `powerBatchGenerator F 3`, one uniform field challenge, and knowledge error `2 / |F|`.
  `ProofSystem/Plonk/Quotient/` checks the resulting residual through the quotient zero test.
  The multilinear (GKR-style) grand-product argument is a different protocol and is not
  formalized here.

- `ProofSystem/Component/GeneratorBatch.lean` batches polynomial zero tests with a single
  seed from a zero-evading generator. It provides the virtual evaluation oracle, extractor,
  guarded form, perfect completeness, and round-by-round knowledge certificates. Its output
  relation is the input relation of `Component/QuotientZeroTest.lean`; the quotient stage
  performs the acceptance check. Power, affine, and multilinear weights are instances of this
  same component, selected by the generator parameter.
  Weighted polynomial arithmetic and the vanishing-to-dot-product probability bound live in
  `Data/Polynomial/GeneratorBatch.lean`; its “Power weights” section also owns
  `Polynomial.powerBatch` and its algebra lemmas for coding-theory consumers. Generator
  zero-evasion bounds for powers, affine coordinates, and multilinear tensors live in
  `Data/CodingTheory/ProximityGenerator/ZeroEvading.lean`. `MultilinearBasic.lean` owns the
  shared tensor definitions so this theory does not depend on Reed–Solomon agreement results.

- `ProofSystem/Fri/FoldingSoundness.lean` and `QuerySoundness.lean` contain the algebraic
  soundness arguments; `ErrorBounds.lean` instantiates existing numerical MCA bounds.
  `Fri/Spec/Soundness.lean` proves ordinary and round-by-round soundness of the executable
  oracle reduction; `VerifierExecution.lean` identifies its exact acceptance event and
  `InputRelation.lean` owns the input word and strict proximity language and connects them
  to the closed-ball input relation. It is independent of adaptive soundness; the
  bad-event and adaptive bounds import these input definitions.
  `Fri/Spec/Completeness.lean` proves perfect completeness and clipped noisy-input completeness
  of the complete reduction, with an exact final witness and radius-zero output relation.
  `HonestExecution.lean` describes the retained original word and exact subsequent polynomial
  folds. `HonestFolding.lean` and `HonestFinalFolding.lean` prove the actual honest prover runs
  and full output-history agreement. `LocalCompleteness.lean` connects those histories to the
  executable query checks, where only the first block can contain input errors.
  `QueryCompleteness.lean` counts corrupted first-fold blocks and bounds independent uniform
  queries, including the sharper bound for the supplied word and polynomial witness.
  `Spec/Extraction/Program.lean` owns the named straightline extractor: it scans retained arbitrary
  words and interpolates a bounded prefix of accepting positions. Its public result erases the
  same instruction program whose word and field operations are counted. `Spec/ExtractionCorrectness`
  proves exact returned-witness recovery; `Spec/KnowledgeSoundness` proves all-input knowledge
  soundness with this extractor and the existing error. `Spec/MeasuredKnowledgeSoundness` adds
  the program's operation-count vector through `knowledgeSoundnessWithResources`.
  `Spec/Extraction/` owns the immutable access backend, generated domain points, driver, and
  resource proofs; reusable measured
  polynomial operations live in `ToCompPoly/Univariate/Arithmetic*.lean`. Raw coefficient-array
  size facts come from `CompPoly.Univariate.Raw.Size`; canonical-polynomial bounds remain in
  `ToCompPoly/Univariate/Size.lean`. These size facts count stored coefficients, not execution cost.
  Compiled small cases run
  with `lake exe fri-extractor-runtime`; classic trust checks live in
  `ArkLibTest/ProofSystem/Fri/Extraction.lean`.
  `RoundConsistency.lean` connects local checks to word folding. Generic persistent-event
  state functions, adaptive accumulation, and the acceptance-to-soundness bridge live in
  `OracleReduction/Security/{BadEvents,Accumulation,Acceptance}.lean`. These proofs use that
  direct acceptance-to-soundness bridge rather than the general implication and composition
  theorems; see the [FRI audit](../kb/audits/fri-soundness.md).
- `ProofSystem/Stir/` holds the STIR [ACFY24stir] building blocks: `Combine`, `Quotienting`,
  `OutOfDomSmpl`, `ProximityBound` and `ProximityGap`. `MainThm.lean` records the Section 5
  parameters and relations; its module docstring states the construction and soundness targets
  that are not yet formalized.

- `ArkLib.lean` is a generated umbrella import file, not a hand-maintained module index.
- Across the PolyFun/VCVio boundary, import generic polynomial-functor and handler structure from
  PolyFun and oracle/probability specializations from VCVio. Dependency internals are not an ArkLib
  proof surface: if an ordinary import is missing a usable law, upstream that law rather than reaching through the module boundary.
- `ArkLib/Commitments/` splits into two families by *what an opening proves*:
  - `Ordinary/` — standard commitments that only **commit and open** (reveal the committed
    message). These reuse the VCV-io `CommitmentScheme` definition rather than redefining it;
    the concrete schemes are `SimpleRO` (a random-oracle commitment, `Ordinary/SimpleRO.lean`)
    and the simple Ajtai lattice commitment (`Ordinary/Ajtai/Simple/`, with `Scheme`,
    `Correctness`, and `Security` modules).
  - `Functional/` — *functional* commitments that **commit and then prove oracle evaluations**
    of the committed data (an opening proves `oracle data query = response`, not the data
    itself). These have their own, unrelated definition in
    `ArkLib/Commitments/Functional/Basic.lean` (`Commitment.Scheme`, plus correctness and the
    experiments `Commitment.bindingExperiment`, `Commitment.functionBindingExperiment`,
    `Commitment.extractabilityExperiment` and `Commitment.extractability`). KZG and Hachi are the
    concrete functional schemes.
- KZG commitment-scheme modules live under `ArkLib/Commitments/Functional/KZG/`: `Basic` for the
  construction and scheme instance, `Algebra` for the powers-of-τ SRS and prime-order group
  lemmas, `Sampling` for setup sampling helpers, `HardnessAssumptions` for t-SDH and ARSDH games
  over explicit adversary classes, `Correctness` for correctness proofs, `Binding` for evaluation
  binding, and `FunctionBinding/` for function binding. Binding is stated as reductions:
  `KZG.CommitmentScheme.binding_reduces_to_tSdh` bounds an adversary's binding advantage by the
  t-SDH success of its reduction, and `KZG.CommitmentScheme.function_binding_reduces_to_arsdh`
  does the same for function binding and ARSDH. Shared CPolynomial/Polynomial division bridge
  lemmas live under `ArkLib/ToCompPoly/`.
- `ArkLib/AGM/Basic.lean` defines algebraic group representations (`GroupRepresentation`): the
  scalars an algebraic adversary reports for each group element it outputs.
- `ArkLib/Commitments/Functional/BitZ/` holds the supporting algebra and probability bounds of
  BitZ: `ExponentLift` for the bit inner product in an exponent, `Round1` for the honest-message
  coefficient bound and fixed-witness fingerprinting error, `Round2` for the deterministic
  tensor implication, and `OutOfDomain` for the multilinear-list collision bound. There is no
  `Commitment.Scheme` instance or composed protocol security theorem yet. The
  [BitZ paper page](../kb/papers/BGKLSW26.md) maps statements to the paper and records the remaining
  protocol obligations.
  Binary-encoding bounds and injectivity live under `Data/Nat/BitSum`; other generic helpers are
  under `Data/Matrix/DotProduct` and
  `ToMathlib/MvPolynomial/CoeffBound`. `Data/MvPolynomial/PrimeFingerprint` contains counting
  bounds; `PrimeFingerprintProbability` adds the two-stage native sampler.
  `Data/MvPolynomial/LinearMvExtension` owns `powAlgHom` coefficient recovery and injectivity.
  Acceptance clients live under `ArkLibTest/Commitments/Functional/BitZ/`, including a CompPoly
  evaluation-table application, and `ArkLibTest/Data/MvPolynomial/PrimeFingerprintProbability`.
- Hachi commitment-scheme modules live under `ArkLib/Commitments/Functional/Hachi/` and formalize
  the Greyhound [NS24] / Hachi [NOZ26] *inner-outer* Ajtai lattice commitment over a cyclotomic
  ring `Rq Φ`. The folder is organized by paper section;
  every subfolder carries its umbrella as `Basic.lean` inside that subfolder.
  `ArkLib/Commitments/Functional/Hachi/Basic.lean` is the folder-level landing page, with the full
  folder map in its module docstring. Layout:
  - `Gadget/` (§2.1) — `Gadget/Core` is the base-`b` gadget matrix `G` and its norm-reducing digit
    decomposition `G⁻¹`; `Gadget/Norms` is the centered `ℓ₂²`/`ℓ∞` shortness bounds for both
    directions the honest case and Lemma 8 need. `Gadget/Basic.lean` re-exports both.
    **Two decompositions coexist and must not be confused.** `DigitDecomposition` is the
    *full-input* one: its reconstruction law holds for every residue, without restricting digit
    range. Restricting the digits to a base-`b` box of size `b` requires `q ≤ b ^ digits` to cover
    `ZMod q`; the concrete construction uses `δ = ⌈log_b q⌉`. That is right for the message
    and inner steps, whose coefficients are arbitrary residues. `BoundedDigitDecomposition base
    digits bound` is the *short-input* one: a total, executable digit map whose reconstruction law
    is conditional on `|x| ≤ bound`, realized by `boundedBalancedZmodDigitDecomposition` on the
    balanced interval `[-⌊b/2⌋·S, (b-1-⌊b/2⌋)·S]`, `S = digitOnesValue b digits`. It exists for
    Hachi's folded witness `z = Σᵢ cᵢ sᵢ`, whose digit count `τ` is set by the deterministic bound
    `‖z‖∞ ≤ 2ʳ·ω·⌊b/2⌋` and **not** by `q`: at the `ℓ = 30` parameters, where `τ = 5`
    (see `Params.lean`), one has `16⁵ < q`, so five balanced digits cannot cover every residue,
    yet `τ = 5` is perfectly correct. `gadgetDecomposeFun` (a bare per-coefficient digit map) is
    the shared computational core of both, so the layout and norm bookkeeping is proved once.
  - `TraceHead/` (§3.1) — the one-message, zero-challenge scalar-to-ring trace head. `Coefficients`
    packs monomial coefficients over the fixed subring, proves the read-back directly, and
    identifies the packing, through `CMlPolynomial.equivMvPolynomialDeg1`, with the shared
    `PackingData.packedMLE` of a monomial-coefficient `ClaimLayout`
    (`traceHeadLayout`, one opening coordinate); `Coordinates` indexes `psi` by the monomials
    and turns the trace check into a coefficient inner product, `Protocol` is the aborting verifier
    with its `CheckedObservation` read-back and coordinate-wise special soundness into
    `relPolyEval`, `Completeness` proves perfect completeness (also at the message-bounded
    relations), and `Commitment` covers the honest committer. The fixed subring is used as a ring;
    nothing here depends on its field identification. The importable library module
    `TraceHead/Conformance.lean` states the accepting condition through the shared `sliceRel`
    (`trace_head_conforms`); concrete fixtures remain in
    `ArkLibTest/ProofSystem/RingSwitching/Conformance/Hachi.lean`.
  - `EvalSplit.lean` (§4, Eq. (12)) — the matrix split underlying the evaluation argument:
    multilinear evaluation `eval p (xl ++ xh)` factors as the vector–matrix–vector product
    `mb(xl) ⬝ᵥ (toMatrix p *ᵥ mb(xh))` (`evalSplit_eq_eval`), with the inverse reshape
    `toPolynomial` and the bridge lemma `splitForm_monomialBasis_eq_eval` consumed by
    `QuadEval/Bridge`. Kept top-level rather than inside `QuadEval/`, since it is a statement about
    the polynomial layer alone.
  - `InnerOuter/` (§4.1) — the scheme itself: `Scheme` (the inner/outer commit composition and its
    *weak opening*, following [NOZ26, §4.1]), `Correctness` (perfect correctness for lawful
    gadget decompositions), `Security` (the weak-binding reduction to Module-SIS via
    `verify_weak`), and `Arithmetic` (pins the modulus to the power-of-two cyclotomic
    `X^{2^α}+1`, which the security proofs genuinely require). `InnerOuter/Basic.lean`
    re-exports the scheme, its correctness, and its weak-binding reduction.
  - `QuadEval/` (§4.2, "Polynomial Evaluation as Quadratic Equation", Figure 3) — Hachi's
    polynomial-evaluation reduction, which proves `f(x) = y` by expressing the evaluation as the
    quadratic form `bᵀ M a` and folding the `2ʳ` carrier blocks under the challenge vector (hence
    the name `QuadEval`); it is Hachi's multilinear/inner-outer lift of Greyhound's [NS24, §3.1]
    folding protocol. `QuadEval/Gadgets` holds the gadget algebra (`PublicParamsD`, the
    honest-prover carrier/short commitment `v = D ŵ`, the `J`-decomposition of `z`, and the
    `tensorG`/`tensorG1` challenge combinations). `QuadEval/Reduction` is the 2-round protocol with
    its types, plain `relOut` (Eq. (20) + range balls), plain `relIn` (eval-consistent weak
    opening), and the `QuadEvalSISBreak`/`quadEvalSISSet` **break vocabulary** for MSIS(B/D)
    outcomes — key-tied: breaks are validated against the fixed key parameter `pp`, which (like
    the relations' key) is never statement data.
    `QuadEval/Soundness` is the subtract-and-divide extraction `buildWitness`, split into the plain
    assembler `quadEvalMkWitness` and the **escape event** `quadEvalEscLocal`, and **Lemma 8**
    (coordinate-wise special soundness) as the single
    `quadEval_coordinateWiseSpecialSoundWithEscape` (named-extractor, *plain* input and output
    relations, escape as a disjunct of the conclusion; `sorryAx`-free) feeding the package,
    the composable `quadEvalPackage`, and the reduction's derived norm constants
    `quadEvalZL2SqBound` = `B_z` / `quadEvalBetaSq` = `4·B_z` (the generic tree plumbing lives in
    `Security/CoordinateWiseSpecialSoundness/SingleRound`; the supporting norm growth is in
    `Data/Lattices/CyclotomicRing/NormBounds/Basic` and `Gadget/Norms`; the executable division
    the extraction divides by is `Data/Lattices/CyclotomicRing/Inverse`). `QuadEval/Bridge` is the
    **polynomial-level bridge**: a zero-round `ReduceClaim` head (`bridgeVerifier`) reinterpreting a
    `CMlPolynomial`-level `PolyEvalStatement` as a `QuadEvalStatement` via the monomial tensor bases
    (`toQuadEvalStatement`), the pulled-back input relation `relPolyEval`, and its CWSS
    `bridge_coordinateWiseSpecialSoundWith`. That link is proved in **both** directions too: the
    computable protocol object `bridgeReduction` (verifier `= bridgeVerifier` by
    `bridgeReduction_verifier`), the converse relation step `mem_relIn_of_relPolyEval` — which makes
    `relPolyEval` exactly the pull-back of `relIn` — and `bridgeReduction_perfectCompleteness`
    (error `0`, straight from the generic `ReduceClaim.reduction_completeness`: a zero-round
    `ReduceClaim` head draws no challenge and performs no check, so all of its content is that
    relation equivalence). `QuadEval/Completeness` is the **honest direction**, in
    two readings that must not be conflated. *Ball-relaxed*
    (`quadEvalReduction_perfectCompleteness`, concretely `…_boundedBalancedDigits`)
    reaches ArkLib's `relOut`, whose c6 is the symmetric ball, **not** Eq. (20)'s box `S_b` — the
    containment
    `paperRelOut ⊆ relOut` transports *soundness* to the paper's verifier and is useless in the
    honest direction. *Paper-exact* (`…_paperRelOut`, `…_balancedDigits`) reaches `paperRelOut`
    itself, using the balanced digits `balancedZmodDigitDecomposition` whose range *is* `S_b`
    (`balancedZmodDigit_valMinAbs_mem`), from the box-carrying input relation `relInBox`;
    `…_relOut_of_balancedDigits` then derives the relaxed conclusion, making the containment's
    direction explicit. Shared linear content: `honestRows_of_relIn` (rows c1–c5 at every challenge
    vector — hence error `0`). The certificate is tied to the same verifier by
    `quadEvalPackage_verifier_eq_quadEvalReduction_verifier`.
    `QuadEval/Basic.lean` re-exports the reduction, its soundness, its completeness,
    and the bridge.
  - §4.3 (Hachi's sumcheck-based opening, Figures 4–7) is split into one flat folder per paper
    subprotocol figure (peers of `QuadEval/`), each file exporting a CWSS package
    in the weakest kind it honestly lives in: plain `CWSSPackage`/`GCWSSPackage` for the reshaping
    and guarded-check links, `EscapeCWSSPackage`/`EscapeGCWSSPackage` (plain relations plus an
    escape *event*) for the links whose extraction can break an assumption. The nine-link
    iteration's soundness side is **complete and axiom-clean**, with a **computable**
    composed extractor — as is the closing `EndPiece/`. The honest nonrecursive chain is in
    `Correctness.lean`; its composed completeness uses the proved guarded append completeness.
  - `RingSwitch/` (§4.3 entry, Figure 4 / Lemma 9) — the HMZ25 **ring-switching lift** reducing
    `R^lin` to a claim about the committed lifted witness evaluated at a random `α`.
    `RingSwitch/Rlin` is the zero-round Eq. (20) → `R^lin` adapter (a plain `CWSSPackage`, pure
    statement reshaping, **proven**); `RingSwitch/Reduction` is the **cyclotomic instance** of the
    generic `Lift` switch (`ProofSystem/RingSwitching/Lift/`): `cyclotomicPresentation` +
    `IsPresentation` laws (discharged from `Data/Lattices/CyclotomicRing/QuotientLift.lean`), the
    generic `checkAt`, and the generic interpolation/descent engine, assembled through the
    committed-scalar shell (`k = 2d`, abstract `w̃`-commitment `LiftCom` with its short-collision
    set `LiftCom.Collision`; the weak-binding escape event is `CommittedScalar.escEvent`, so this
    link is an `EscapeCWSSPackage`; **proven** Lemma 9 CWSS). `RingSwitch/Completeness` is the
    honest direction of **both** links, proven and axiom-clean and now **unconditional**:
    `rlinReduction_perfectCompleteness_image` lands in the *image* seam `relRlinImage` (the pairs
    that came from the adapter: `p = (rlinStmt X, stack w)` with `(X, w) ∈ relOut`), and
    `liftReduction_perfectCompleteness_image` consumes exactly that, discharging **both** halves of
    `liftShort`: the `z`-bound from seam membership, the quotient bound from the digit encoding
    (`rhoDigitsShort_of_digitBaseOk`), which needs no hypothesis on the witness. Nothing is
    assumed. Why the honest side uses a different relation
    than soundness: `relRlin` forgets the matrix provenance, the value of `s.bound`, and hence the
    protocol-level `z`-bound — and `∀ s, bound ≤ s.bound` is *false* for positive `bound`
    (`s.bound = 0` is a legal statement), so the condition must be carried by the seam. The seam
    refines `relRlin` (`mem_relRlin_of_mem_relRlinImage`), so no relation is weakened.
    `RingSwitch/RhoDigits` is [NOZ26] §4.3's **hidden gadget decomposition** of the quotient:
    `rhoDigits` splits each quotient row into `δ = clog_b q` balanced base-`b` digits, with the
    reconstruction identity `rhoDigits_reconstruct` / `rhoDigits_evalAt` and the unconditional
    per-digit bound `rhoDigits_valMinAbs_natAbs_le` (`⌊b/2⌋`, for *any* quotient). This is what
    `liftMessage` commits — a vector of width `μ + n·δ`, not `μ + n` — and what makes
    `LiftCom.Collision` a genuine Module-SIS instance: `moduleSIS_relation_of_mem_Collision`
    proves a short collision satisfies `ModuleSIS.relation` for the Ajtai key at radius `2·bound`,
    its nonzero conjunct coming from `liftMessage_injective` (the digits reconstruct the
    quotient, so the committed vector determines the opening).
    `RingSwitch/QuotientNorms` is the bound on the **raw** quotient: for `φ = X^d + 1` division
    *selects* coefficients (`Polynomial.coeff_divByMonic_X_pow_add_one`, in
    `ToMathlib/Polynomial/DivByXPowAddOne`), so it inherits any coefficient bound on the row sum —
    `μ · 2d · βM · βz`, with **no wraparound hypothesis**. For the Hachi chain the only honest `βM`
    is `q/2` (the `R^lin` matrix carries the Ajtai key and gadget powers), so an *undecomposed*
    quotient can only be bounded by `q/2` (`rhoShort_half`); that is precisely why the digit
    encoding is necessary rather than decorative, and `HonestChain.lean` records the parameter
    collapse it removes.
    `RingSwitch/Basic.lean` re-exports the folder. (The §3 packing reduction is a distinct
    algebraic construction —
    `ProofSystem/RingSwitching/Packing/` — which does not use the committed-scalar seam; the two
    constructions share the ring-switching folder's top-level verifier skeletons and transport
    algebra.)
  - `ZeroCheck/` (§4.3, Figure 5 / **corrected** Lemma 10) — reduces the batched identities
    `H₀ ≡ 0 ∧ H_α ≡ 0` to random-point evaluations. `ZeroCheck/Constraints` is the **shared**
    encoding (Eqs. (21)–(23): the table `w̃`, `H₀`/`H_α`, the sumcheck polynomials, degree pins,
    per-round seam `nestedRoundRel`), consumed by both this zero-check and `Sumcheck/`;
    `ZeroCheck/Batch` is the per-row/range ⇄ `H₀/H_α ≡ 0` batching bridge (proven **both ways** —
    `mem_relLift_of_relBatched` and `mem_relBatched_of_relLift` — and the place
    `liftShort` is *derived* from `H₀ ≡ 0` rather than assumed); `ZeroCheck/Reduction` is the
    corrected Lemma 10 (`m₀ + m₁` scalar challenge rounds with `k = 2` each, extracted through the
    nested evaluation tree of `ArkLib/Data/MvPolynomial/NestedEvaluationTree.lean` — Mathlib-level,
    `k`-ary, individual degree `< k` — with the computable view in
    `ArkLib/ToCompPoly/Multilinear/NestedEvaluationTree.lean`; its named
    `nestedZeroCheckExtractor` is an executable all-left lookup into
    `ChallengeTree.LeafWitnesses`, with no runtime relation search; the weak-binding failure mode
    is the escape event `nestedZeroCheckEsc`, whose hardness target is `LiftCom.Collision`). Its
    module docstring carries the counterexample and the repair; the full analysis is
    `docs/kb/audits/noz26-zero-check-lemma10.md`. `ZeroCheck/Completeness` is the honest direction
    (`nestedZeroCheckReduction_perfectCompleteness`, proven and axiom-clean, with error exactly
    zero — `relBatched` asserts the identities, so nothing about the challenge distribution is
    used). It also carries `batchReduction_perfectCompleteness`, the batching bridge's honest
    direction, so both links of this folder are certified in both directions.
    `ZeroCheck/Basic.lean` re-exports the folder.
  - `Sumcheck/` (§4.3, Figure 6 / Lemma 11 + Figure 7 tail) — the sumcheck loop finishing the
    opening, **proven and axiom-clean throughout** (rows 7–9). `Sumcheck/Bridge` reshapes the
    zero-check's point claims into the initial hypercube sums; `Sumcheck/RoundPoly` is the
    round-polynomial layer (cube split, the partial sum as a univariate with its evaluation and
    degree lemmas — proof-side in Mathlib's `Polynomial`, plus the computable `computableRoundPoly`
    the prover sends and the transfer lemma tying the two together); `Sumcheck/Rounds` is the
    `m₀`-round guarded paired sumcheck (Lemma 11, loop by recursion over `▷ᵍ`) with a computable
    extractor that reads the supplied branch openings; `Sumcheck/FinalEval` is the guarded reveal
    of `w̃(a)` (Figure 7 tail) landing on the short-opening evaluation claim `relWEvalClaim`,
    whose computable extractor reads the unique leaf opening; `Sumcheck/Completeness` is the
    honest side — `honestComputeG`, one round's perfect completeness (axiom-clean), the `m₀`-fold
    honest chain sharing its verifier with `roundsChain`, and
    `bridge ▷ rounds ▷ final evaluation`. `Sumcheck/Basic.lean`
    re-exports the folder and records why this round layer is *not* built on the generic
    `ProofSystem/Sumcheck/` modes (their rejection convention is incompatible with tree-based
    extraction, and neither carries a soundness certificate to inherit). The folded honest
    completeness statements use proved guarded composition and suffix completeness from every
    shared oracle state; their axiom dependencies are standard only.
  - `EndPiece/` (§4.3, closing) — the **terminal link** of the opening: the prover sends the
    reduced witness `w̃` and the guarded verifier checks `relWEvalClaim` against it directly
    (recompute the commitment, evaluate the table MLE at the sumcheck point), leaving nothing to
    reduce. Escape-free — it re-reads data just sent, so no hardness assumption is consulted — and
    **`sorry`-free and axiom-clean**: extraction is the identity on the transcript message
    (`endPieceWitness`), and CWSS closes through the challenge-free bridge plus guarded
    acceptance. Certified in both directions about the same verifier: `endPieceReduction` /
    `endPieceReduction_perfectCompleteness` is the honest side, and the full reflection lemma
    `endPieceCheck_eq_true_iff` is shared with the nonrecursive scheme's terminal verdict
    (`Correctness.lean`), so the closing link has one decision procedure.
    `EndPiece/Basic.lean` re-exports `EndPiece/Reduction.lean`.
  - The recursive opening (§4.5) is not formalized; `docs/kb/audits/noz26-recursion-z-packing.md`
    records why.
  - `Composition.lean` — the **CWSS composition home**: `iteration` chains all nine subprotocol
    links (rows 1–9 of the header's seam table) into one evaluation iteration, and
    `hachi_iteration_coordinateWiseSpecialSoundWithEscape` states its composed named-extractor CWSS
    certificate (`sorry`-free and axiom-clean). `eval_coordinateWiseSpecialSoundWithEscape` states
    the same for the rows 1–2 front alone — the paper's Figure 3 reduction. `roundsChain` re-pins
    the sumcheck loop's relation seams definitionally, so the guarded tail composes with the
    universal `▷` rather than with explicit appends at named seam lemmas. `endPiece` (imported
    from `EndPiece/`, `sorry`-free and axiom-clean) closes a run of iterations, and `evaluation`
    is `iteration ▷ endPiece` — the complete opening argument, with no sorried factor left.
    Escape events compose along the chain by `ChallengeTree.EscapeEvent.append`, so only relation
    seams have to match.
  - `Commitment.lean` — **Hachi as a `Commitment.Scheme`**: the eval `OracleInterface`, honest
    `keygen`/`commit` (the paper's **balanced** base-`b` gadget decomposition at width
    `δ = ⌈log_b q⌉`, digits in Eq. (20)'s box `S_b` — `[-8, 7]` at `b = 16`), used by
    `hachiNonrecursive`; the unsigned `zmodDigitDecomposition` survives only
    as the building block the balanced digits are shifted from (`Gadget/Core`), and
    `InnerOuter.perfectlyCorrect` is likewise stated at the balanced digits. The file also carries
    the **honest-committer facts** the honest chain needs: `verifiedOpening_honestOpening` (the
    committer's output is a `WeakBinding.VerifiedOpening` — it lives here, not in
    `InnerOuter/Correctness`, because `InnerOuter/Security` imports that file),
    `vecInSb_honestInnerDecomp_balanced`, and `mem_relInBox_of_honestBalanced` /
    `mem_relInBox_of_commit`: the honest opening satisfies paper-exact `QuadEval`'s input relation
    `relInBox`, given Eq. (15) evaluation consistency — the second one at the actual output of
    `commit`. Weak-opening validity, evaluation consistency and box membership stay separate
    conjuncts. The **nonrecursive** scheme `hachiNonrecursive` in `Correctness.lean` is where the
    same committer is packaged with a complete opening and perfect correctness is proved.
  - `HonestChain.lean` — the honest side's **parameter interface** and prefix composition:
    `HonestRangeParams` (digit base `b`, Eq. (20) ball radius `γ`, zero-check range base `bZero` —
    which is also the base of the quotient's hidden gadget decomposition — with the box→ball
    condition, the batching bridge's *honest-direction* inequality, and the digit-base
    admissibility triple `DigitBaseOk q γ bZero`, plus the witness
    `HonestRangeParams.ofPinnedDigitBase` at `γ = b − 1`, `bZero = b`, which also meets the
    pull-back orientation and so realizes the two-sided regime), one named corollary per seam,
    and `completePrefixReduction` — the appended bridge ▷ QuadEval ▷ `R^lin` ▷ lift ▷ batching ▷
    zero-check protocol. Its completeness uses proved pure-verifier composition, and the
    extension through sumcheck uses guarded composition. Each suffix is complete from every
    shared oracle state, so both composed results have standard-only axiom dependencies.
    `ZeroCheck/Constraints` represents the quotient by base-`bZero` digits (`rhoDigits`),
    each bounded by `⌊bZero/2⌋`. The batching bridge requires `bound ≤ bZero − 1`;
    `HonestRangeParams.pinned_of_soundness_orientations` gives `γ = bZero − 1 < q/2`
    when both pull-back orientations hold.
  - `Correctness.lean` — **the complete nonrecursive opening and its perfect correctness**. The
    chain is closed without the §4.5 recursion adapters by a `SendWitness`-style **terminal
    reveal-and-check**: the prover sends the final `LiftedWitness`, the verifier decides the whole
    `relWEvalClaim` predicate on it by returning `endPieceCheck` — the very check the guarded
    `EndPiece/` verifier guards on, with reflection lemma `endPieceCheck_eq_true_iff`, both
    axiom-clean — as its Boolean verdict (`terminalVerifier_verify_eq_endPieceCheck`). A zero-round
    **input adapter** (`commitInputReduction`, honest lemma
    `mem_relPolyEvalMsgShort_of_relCommitInput`, with `mem_relPolyEval_of_relCommitInput` as its
    forgetful corollary) converts the commitment API's claim into `relPolyEvalMsgShort` for the
    balanced committer — `relPolyEval` plus the `ℓ∞` bound `⌊b/2⌋` on the committer's message
    decomposition, the one extra invariant the honest-`z` shortness bound consumes. Adapter ▷
    chain-through-sumcheck ▷ terminal compose into `hachiNonrecursiveOpening`, packaged with
    `commit` as the scheme `hachiNonrecursive`, and
    `hachiNonrecursive_perfectCorrectness` proves `Commitment.perfectCorrectness` via the generic
    bridge `Commitment.perfectCorrectness_of_opening_perfectCompleteness`
    (`Commitments/Functional/Basic.lean`, axiom-clean, using
    `OptionT.prEvent_mk_bind_eq_one_of_support`). The composed opening/correctness theorems use proved
    guarded composition and have standard-only axiom dependencies, as do their individual links,
    adapter, terminal step, and correctness bridge. The unfinished recursive opening was retired
    ([#1411](https://github.com/Verified-zkEVM/ArkLib/pull/1411)).
    **`τ` is an independent parameter here.** `hachiNonrecursiveOpening` / `hachiNonrecursive` /
    their correctness theorems take the folded-witness digit count `τ` and its bound `zBound` as
    section variables, constrained only by `hcap : zBound ≤ balancedDigitCapacity P.b τ`,
    `hzb : 2ʳ·ω·⌊b/2⌋ ≤ zBound` and `0 < τ`; the message and inner digit counts stay `δ`. `μ₀`
    (`rlinCols`), the lift key width and the sumcheck table width all depend on `τ`, so a
    correctness statement and the soundness-side `quadEvalBetaSq` cannot silently disagree about
    it. No `q ≤ P.b ^ τ` hypothesis exists on this path (it is false at the `ℓ = 30` parameters).
  - `Concrete.lean` — the same scheme at the concrete Ajtai lift commitment `D · (z ‖ ρ)`
    (`nonrecursiveLiftCom`), where every honest field is computable; it carries the same `τ` /
    `zBound` parameters. `scripts/HachiRuntime.lean` (the `hachi-runtime` executable) runs it at
    toy parameters with `τ = 1 < δ = 2`, so the bounded `z` decomposition is exercised, and checks
    the bounded digit function directly at the production digit parameters `b = 16` and `τ = 5`.
  - `Params.lean` — the [NOZ26] Figure 9 `ℓ = 30` parameters (`q = 4294967197` — primality proved
    by `norm_num`'s Pratt certificate — `b = 16`, `δ = 8`, `r = m = 10`, `ω = 16`, `α = 10`,
    `d = 1024`) **at `τ = 5`** rather than Figure 9's tabulated `τ = 4`. The `τ` divergence is
    deliberate and is the one place this profile departs from Figure 9's table — but it is *not* a
    departure from the paper's own prescription: §4.4 fixes `τ` as the smallest integer with
    `b^τ > β` for `β := 2ʳ·ω·b = 262144`, and `16⁴ = 65536`, so §4.4's rule yields `5`. The same
    holds under the sharper `‖z‖∞ ≤ 2ʳ·ω·⌊b/2⌋ = 131072` formalized here, for which five digits are
    minimal. Do not describe this as the exact Figure 9 profile, and do not describe `τ = 5` as
    conservative relative to the paper. The file carries the arithmetic the chain consumes at it:
    `q ≤ 16⁸` with `Nat.clog 16 q = 8`, the deliberate `16⁵ < q`, the balanced capacity `489335` of
    five base-`16` digits with the honest bound `131072` fitting inside it, and `μ₀ = 57344`.
    **`τ = 5` is minimal, not merely sufficient**: `tau_minimal` rules out every `t < 5`, since
    `balancedDigitCapacity 16 4 = 30583 < 131072` and capacity is monotone
    (`balancedDigitCapacity_mono`). That `30583` is exactly the `z` value [NOZ26] Figure 9
    tabulates alongside its `τ = 4`. This equality does not establish how that entry was derived.
    The paper does not prove `30583` as a deterministic bound or analyze Figure 3's abort when
    `‖z‖∞ > β`. A `τ = 4` profile needs a justified completeness bound for that abort;
    statistical analysis is one possible route. See
    [`../kb/papers/NOZ26.md`](../kb/papers/NOZ26.md), "Known Divergences From ArkLib". The file
    then instantiates the `τ = 5` `QuadEval` link
    with every hypothesis discharged, in **both** readings —
    `quadEvalLink_perfectCompleteness_atProfile` (ball-relaxed) and `…_paperRelOut` (Eq. (20)'s box
    `S₁₆` verbatim) — which is the machine-checked form of "no `q ≤ 16⁵` is required". Finally it
    pins the **two security directions to one `τ`**: `packageAtProfile` is Lemma 8's certificate at
    `zDigits = 5`, `packageAtProfile_relOut` equates its output relation with the completeness
    theorems' (a statement that cannot be written at two different `zDigits` — the
    `QuadEvalResponse` types would differ), and
    `relInMsgShort_atProfile_subset_packageAtProfile_relIn` lands the correctness input relation in
    the package's `relIn` at `βSq = betaSq`. The *scheme*-level substitution is not written out:
    every profile hypothesis it would need is already discharged here (`hμn` by
    `sumcheckWidthAtProfile` at `M = 25`), and the composed scheme's type carries
    `Nat.clog params.b 4294967197` inside `Fin (2¹⁰)`-indexed matrices and a 26-deep
    `ProtocolSpec` append tower, which exhausts the elaborator's `isDefEq` budget.
- Merkle trees live upstream in VCV-io under `VCVio/CryptoFoundations/MerkleTree/`: addressed
  perfect trees in `Addressed/` (namespaces `AddressedMerkleTree` and `PerfectMerkleTree`), the
  inductive tree in `Inductive/` (namespace `InductiveMerkleTree`), salted trees in `Salted/`
  (`SaltedMerkle`), hash forests in `HashForest/` (`MerkleHashForest`), leaf and node hashing in
  `Hashing/` (`MerkleTreeHashing`), and extraction in `Extractor.lean`, `Extractability.lean`,
  `BatchExtractability.lean` and `MultiExtractability/` (`MerkleTreeExtractor`,
  `MerkleTreeExtractability`, `MerkleTreeMultiExtractability`).
- Reed-Solomon code definitions live under the `ReedSolomon` namespace: the base RS code in
  `ArkLib/Data/CodingTheory/ReedSolomon.lean`, and the folded/interleaved/multiplicity/multilinear
  variants under `ArkLib/Data/CodingTheory/ReedSolomon/` (see
  [coding-theory-conventions.md](coding-theory-conventions.md)).
- **Two different "folds" coexist and must not be confused.** GR08 *alphabet-enlarging* folding —
  a codeword symbol packs `(f̂(x), f̂(xω), …, f̂(xω^{s-1}))`, the degree bound is unchanged, and the
  code lives in `ι → Fin s → F` — is `ArkLib/Data/CodingTheory/ReedSolomon/Folded.lean`. The
  FRI/STIR-style *split-and-fold*, where a challenge contracts the polynomial and the evaluation
  domain shrinks, is `ProximityGap/Folding.lean`, `Data/Polynomial/SplitFold.lean`, and
  `Data/Polynomial/FoldingPolynomial.lean`; the "folded RS code" there is a plain RS code on a
  subdomain, not an FRS code.
- The ABF26 generic coding-theory layer sits in `ArkLib/Data/CodingTheory/` under the
  `CodingTheory` namespace: `SubspaceDesign.lean` (`IsSubspaceDesign` and the folded-RS
  subspace-design theorem), `ExtensionCodes.lean` (extension-field presentations and extension
  codes), `Erasure.lean` (erasure-consistency uniqueness below minimum distance),
  `HammingBallVolume.lean`,
  `Basic/Entropy.lean` (`qEntropy`), `Basic/ParityCheck.lean` (codes cut out by parity checks and
  the counts of parity-check tuples). List-size bounds of Johnson type are in
  `JohnsonBound/Family.lean`, alongside the pre-existing `JohnsonBound/Basic.lean` machinery it
  consumes.
- List-size bounds that are *not* of Johnson type are under `ListDecodability/Bounds/`, with
  `ListDecodability/Bounds.lean` as the umbrella that imports them and carries the family overview,
  the quantification conventions and the shared reference list. The split is by scope, not by paper:
  `Bounds/Basic.lean` (the three counting identities everything rests on), `Bounds/Linear.lean`
  (bounds valid for every linear code — Elias volume and its entropy form, the rate–radius
  arithmetic, the generalized Singleton bound), `Bounds/RandomLinear.lean` (the random-linear-code
  bound, with the [GLMRSW22] proof in `Bounds/RandomLinear/`),
  `Bounds/LargeAlphabet.lean` (the exponential-alphabet barrier, over the four-file development in
  `Bounds/LargeAlphabet/`: statements and family counting, centres and incidence counting, the local
  neighbourhood bound and pigeonhole barrier, then sparse large-union families and the assembly),
  `Bounds/Interleaved.lean` ([GGR11]'s interleaved-code list-size bound),
  `Bounds/ReedSolomon.lean` (the Reed-Solomon separations and the random-evaluation-domain bound,
  with the subspace-polynomial witnesses in `Bounds/ReedSolomon/SubspaceWitness.lean`),
  `Bounds/SubspaceDesign.lean` ([CZ25]'s upper bound and the folded-RS and multiplicity-code
  corollaries) over `Bounds/AgreementHypergraph.lean` (the geometric agreement machinery that proof
  needs, which mentions no list size and is reusable), and `Bounds/KKH26.lean` plus
  `Bounds/KKH26Asymptotic.lean` (the concrete [KKH26] templates and ABF26 Theorem 3.15). The
  file/directory pair
  `ListDecodability.lean` + `ListDecodability/` follows the same shape as `ReedSolomon.lean` +
  `ReedSolomon/`: the file holds the definitions (`Lambda`, `listDecodable`), the directory holds
  results about them. A few deep bounds are externally sourced solicited proofs: they carry tagged
  `sorry` annotations and are listed in the `solicited` array of `scripts/axiom_baseline.json`
  ([#1352](https://github.com/Verified-zkEVM/ArkLib/issues/1352)); use the paper KB pages to inspect
  their sources. In-tree results include [CZ25]'s subspace-design theorem (and therefore the
  folded-Reed-Solomon and univariate-multiplicity capacity corollaries) and the [AGL23]
  large-alphabet barrier.
- ABF26's citation-heavy §4–§5 catalogue is separated from the core error definitions:
  `ProximityGap/CapacityBounds.lean` holds the numeric upper/lower bounds.
  `ProximityGap/CapacityBounds/SubspaceDesign.lean` shares the subspace-design pinning
  and affine-line MCA conversion used by the generic and folded Reed--Solomon bounds.
  `ProximityGap/LineDecoding.lean` holds the GG25-corrected interfaces corresponding to ABF26
  Definition 4.20 and Theorem 4.21, and
  `Connections/ListDecodingAndCA.lean` holds the four list-decoding/CA connections. Extensions
  that turn bounds into prize witnesses live below `ProximityGap/GrandChallenges/`, so the
  core `GrandChallenges.lean` grid and carrier API does not import the catalogue. The
  Johnson-range witness uses the bound proved via [DKT26], with the [BCHKS25] Theorem 4.6
  printed constant.
- The folded Wronskian (GK16 Definition 11) and its linear-independence criterion live in
  `ArkLib/Data/Polynomial/FoldedWronskian.lean`, not under `CodingTheory/`; its sibling
  `ArkLib/Data/Polynomial/ClassicalWronskian.lean` holds the ordinary Wronskian and the
  degree/derivative criterion behind the univariate-multiplicity half of ABF26 T2.18. Their
  generic determinant-divisibility and finite-field Kummer dependencies live in
  `ArkLib/ToMathlib/LinearAlgebra/Matrix/Determinant.lean` and
  `ArkLib/ToMathlib/FieldTheory/Kummer.lean`.
- **MDS lives in two shapes, and only one reaches module alphabets.** `LinearCode.IsMDS`
  (`Basic/LinearCode.lean`) is the `ℕ` Singleton-equality form and is stated only for
  `LinearCode ι F = Submodule F (ι → F)`; `LinearCode.IsMDS_iff_rate_distance` converts it to
  the `ℝ` rate-distance form `δ_min = 1 − ρ + 1/n` that ABF26 uses. Codes over a module
  alphabet `Fin s → F` (folded, interleaved, extension) **cannot** use the predicate and
  supply the rate-distance equation directly instead, at the alphabet-normalized rate
  `LinearCode.alphabetRate`: see `ReedSolomon.Interleaved.irs_rate_distance` (no divisibility
  needed) and `ReedSolomon.Folded.frs_rate_distance_of_dvd` (needs `s ∣ k`). Both feed the
  alphabet-generic `CodingTheory.mds_johnson_lambda_le_of_rate_distance`, whose module-alphabet
  consumers are `CodingTheory.irs_lambda_le_johnson_mds` and
  `CodingTheory.frs_lambda_le_johnson_mds` in `JohnsonBound/Family.lean`. Generalising the
  `IsMDS` *predicate* itself to `ModuleCode ι F A` is still open, and is **independent** of the
  module-alphabet `IsMCA` (which has landed): `IsMDSGenerator` constrains `C_G ⊆ F^|S|`, the
  generator's own code over the base field, so nothing on the MCA path needs it. Whoever does it
  should update this bullet and the corresponding row in
  [`../kb/audits/open-problems-list-decoding-and-correlated-agreement.md`](../kb/audits/open-problems-list-decoding-and-correlated-agreement.md).
- Finite-probability helpers live under the `Probability` namespace in
  `ArkLib/Data/Probability/Instances.lean` (see
  [probability-conventions.md](probability-conventions.md)); the collision bound for random
  functions is `ArkLib/Data/Probability/Combinatorial.lean`. Shannon entropy and Chernoff tails for
  real weights on finite types are `ArkLib/Data/Probability/FiniteEntropy.lean` and
  `ArkLib/Data/Probability/FiniteChernoff.lean`.
- Vandermonde matrix utilities shared across Reed-Solomon and proximity-gap developments live in
  `ArkLib/Data/Matrix/Vandermonde.lean`, not in the Reed-Solomon file.
- Trivariate polynomial utilities used by the BCIKS20 proximity-gap proofs
  (`evalAtX`, `evalAtY`, `evalAtZ`, the named degree projections, `D_Y`, `D_YZ`, and related
  notation) live in
  `ArkLib/Data/Polynomial/Trivariate.lean`, not in `ProximityGap/Basic.lean` or
  `ProximityGap/BCIKS20/ListDecoding/Guruswami.lean`. See
  [`polynomial-conventions.md`](polynomial-conventions.md) before applying generic bivariate
  operations to a trivariate value.
- **The reusable way into `perfectCompleteness` is `Reduction.perfectCompleteness_of_run_support`
  in `Security/Basic.lean`**, not the commented-out `perfectCompleteness_forall_challenge` sketch
  a few lines below it. It reduces perfect completeness to a support statement about the
  *unsimulated* `(Reduction.run …).run`: show every element of that support is a success whose
  output pair is in the output relation and whose two output statements agree, and the probability
  obligation is discharged (through VCVio's
  `OptionT.prEvent_mk_simulateQ_run'_eq_one_of_support`, which handles the sampled initial state and
  the oracle implementation uniformly). It applies to any reduction, of any length, over any
  `oSpec` — no determinism or single-round hypotheses. The worked example is Hachi's zero-check
  (`Commitments/Functional/Hachi/ZeroCheck/Completeness.lean`), where the per-link work reduces to
  a prover-state induction, an output lemma, a run-support lemma, and the relation lemma. Before
  hand-peeling `OptionT`/`liftM`/`simulateQ` layers for a new protocol, check whether this covers
  it. (`Commitments/Functional/KZG/Correctness.lean` applies the VCVio lemma directly.)
  The second worked example is `QuadEval` (`.../Hachi/QuadEval/Completeness.lean`), which adds the
  message-round case: there the run-support half is a closed-form computation of `Prover.run`
  (`prover_runToRound_last` / `prover_run_eq`) rather than an induction.
- **For a zero-round `ReduceClaim` link, do not use `perfectCompleteness_of_run_support` at all.**
  `ReduceClaim.reduction_completeness` (`ProofSystem/Component/ReduceClaim.lean`, proven) discharges
  the whole execution layer; its `hRel` is an **iff**
  (`(stmtIn, witIn) ∈ relIn ↔ (mapStmt stmtIn, mapWit stmtIn witIn) ∈ relOut`), so the only real
  obligation is the converse of the pull-back the soundness side already needed. Three links are
  done this way — `bridgeReduction_perfectCompleteness` (`QuadEval/Bridge.lean`),
  `rlinReduction_perfectCompleteness` (`RingSwitch/Completeness.lean`) and
  `batchReduction_perfectCompleteness` (`ZeroCheck/Completeness.lean`) — each in a few lines once
  the relation converse exists. Budget zero-round heads in hours, not days.
- **The two-round commit-then-challenge execution is owned generically** by
  `CoordinateWise.CommittedScalar.reduction_perfectCompleteness`
  (`Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean`): supply `computeW` plus the two
  facts `rel K checkAt` asks for that are not definitional — the challenge-local check at *every*
  challenge, and admissibility of the computed opening — and the run/probability layer is free.
  Commitment consistency is definitional, because the prover shell derives its round-0 message from
  `computeW`. Consumers: the generic ring-switching lift and, through it, Hachi's Figure 4. Any new
  link of that shape (`pSpecScalar`) should go through it rather than repeating `QuadEval`'s
  hand-unfolding.
- **Unfolding a fixed-length `Prover.runToRound` by hand: ascribe the round indices, do not rewrite
  them.** `Prover.runToRound_succ` is stated at `i.succ` with the recursive call at `i.castSucc`,
  but a concrete run starts from `Fin.last n`, and `Fin.last 2`, `Fin.succ 1`, `Fin.castSucc 1` and
  `(1 : Fin 3)` are equal only after `Fin.val`/`Nat.mod` arithmetic. Consequences, all hit while
  proving `QuadEval` completeness:
  - `rw` on the index itself (`show Fin.last 2 = Fin.succ 1 from rfl`) fails with "motive is not
    type correct", and `rw [Prover.runToRound_succ 1]` fails to match `runToRound (Fin.last 2)`.
  - The working shape is to *state* each unfolding as a `have` at the index that literally occurs
    (`Fin.last 2`, then `(1 : Fin 2).castSucc`, then `(0 : Fin 2).castSucc`) and prove it by the
    framework lemma — the `have`'s type ascription is checked at full transparency, so the indices
    reconcile there instead of inside `rw`. Chain them with `Eq.trans` / `rw`.
  - At index `castSucc 0` the `Unique (Transcript 0 pSpec)` instance is not found; write the empty
    transcript as `fun i => Fin.elim0 i` instead of `default`.
  - Pass the direction proof (`pSpec.dir 1 = .V_to_P`) as a *named hypothesis*, not `rfl`:
    `⟨1, rfl⟩` makes the surrounding term ill-typed at `instances` transparency, which silently
    stops both `rw` matching and `simp` congruence.
  - Once the rounds are unfolded, `simp [monad_norm, liftM, monadLift, MonadLift.monadLift]`
    followed by `rfl` closes the monadic bookkeeping; `FullTranscript.mk2` and
    `FullTranscript.mk2_eq_snoc_snoc` are the bridge between the `Transcript.concat` chain the
    prover builds and the two transcript slots the verifier reads.
- Transcript-tree infrastructure for special-soundness-style notions lives in
  `Security/TranscriptTree/`: `Basic` defines `ChallengeTree`, `LeafPath`,
  `ChallengeTreeShape`, `ChallengeTree.IsStructured`, `ChallengeTree.IsAccepting`,
  `Extractor.TreeBased`, and the shape-generic soundness core `Verifier.treeSpecialSound`. The
  extractor is **witness-only**: it consumes the tree *and* one candidate output witness per leaf
  (`ChallengeTree.LeafWitnesses`, honest when each answer certifies in `relOut` some statement the
  verifier can actually output there — `LeafWitnesses.IsValid`), and returns `Option WitIn`. The
  notion says extraction succeeds on every `S`-structured accepting tree at every valid witnessing;
  the unconditioned reading follows by closing the extractor at `ChallengeTree.canonWitnesses`
  (`treeSpecialSoundWith.mem_relIn_of_isAccepting`). `Basic` also defines the **escape layer**:
  `ChallengeTree.EscapeEvent` (a statement-indexed predicate on full challenge trees, with the
  trusted-spec contract in its docstring) and
  `Verifier.treeSpecialSoundWithEscape`, whose conclusion is `esc stmt tree ∨ extraction succeeds`;
  the plain notion is the never-firing event (`treeSpecialSoundWithEscape_false_iff`) and every plain
  certificate lifts losslessly (`treeSpecialSoundWith.withEscape`). `Composition`
  defines shape append, `appendSplit`, the generic structure-preservation/recombination lemmas
  for sequential protocol append, and `ChallengeTree.EscapeEvent.append` (composition of escape
  events along that split). The umbrella `Security/TranscriptTree.lean` re-exports both files.
  Both plain and coordinate-wise special soundness are instances of `Verifier.treeSpecialSound` for
  different shapes; neither special-soundness file imports the other.
- `Security/UnboundedExtraction.lean` records what `Verifier.knowledgeSoundness` means without
  an extractor cost bound: the classical selector `Extractor.Straightline.choose` makes it
  equivalent to `Verifier.relationSoundness` (`Verifier.knowledgeSoundness_iff_relationSoundness`).
  `knowledgeSoundnessWith` names an extractor without cost.
  `knowledgeSoundnessWithResources` adds declared instruction counts; complete execution bounds
  remain proposed in the [execution design](../design/03b-extractor-execution.md).
- Plain `(k)`-special soundness lives in `Security/SpecialSoundness.lean`. It is the instance of
  `Verifier.treeSpecialSound` for the pairwise-distinct shape `distinctShape k` (arity `kᵢ`, node
  predicate `Function.Injective`), with input/output relations like CWSS; it is the `ℓᵢ = 1`
  specialization of coordinate-wise special soundness. The bridge
  `coordinateWiseSpecialSound (ofSpecialSound k) ↔ specialSound k` lives in
  `Security/Implications.lean`.
- Round-by-round security lives in `Security/RoundByRound.lean` (state functions,
  `Extractor.RoundByRound`, and the notions `rbrSoundness` / `rbrKnowledgeSoundness`), on top of
  the probability glue in `Security/RbrGame.lean` (the challenge-first bounds over
  `simulateQ`/`OptionT` used by ToyProblem knowledge-soundness proofs). This is a **separate axis**
  from the
  transcript-tree notions below: its extractor type is `Extractor.RoundByRound` on transcripts,
  not `Extractor.TreeBased`, and it carries no escape-event layer.
  `Security/Implications.lean` identifies round-by-round knowledge soundness with soundness of the
  induced languages under unbounded extraction. Without
  input witnesses the identification holds for all relations and errors exactly when no input
  statement, full transcript and output witness exist together
  (`Verifier.forall_rbrSoundness_iff_rbrKnowledgeSoundness_iff`), because
  only then does a round-by-round extractor exist (`Extractor.RoundByRound.exists_nonempty_iff`);
  `ArkLibTest/OracleReduction/RoundByRoundCharacterization.lean` checks the separating example.
  `Security/Guarded.lean` defines guarded verifiers, independent of any security notion:
  `Verifier.IsGuardedWith`/`IsGuarded`, their data form `Verifier.GuardedForm` (check and verdict
  map as fields), `GuardedForm.append`, the seam run lemma `Verifier.append_run_guardedLeft`, and
  `Verifier.GuardedForm.ofQueryGuard`, the guarded form of a query-guard-return oracle
  verifier. `Security/GuardedRoundByRound.lean` adds what a round-by-round proof needs about a
  verifier that aborts on a failed check: the positive-probability lemma
  `Verifier.GuardedForm.check_and_of_prEvent_pos` and the message-then-challenge reducer
  `Verifier.rbrKnowledgeSoundnessWith_of_two_message`, which bounds the extraction-failure
  event `rbrExtractionFailureEvent` (defined in `RoundByRound.lean`) per fixed prefix. The run
  equation of a query-guard-return oracle verifier (one message query, then a guard and a
  verdict that may read the answer and the challenges),
  `OracleVerifier.toVerifier_verify_of_query_guard`, is in `OracleReduction/Basic.lean`.
  `Security/GuardedBridges.lean` derives ordinary knowledge soundness from round-by-round
  knowledge soundness of a guarded verifier, with the sum of the per-challenge errors
  (`Verifier.GuardedForm.knowledgeSoundness_of_rbrKnowledgeSoundness`,
  `OracleVerifier.knowledgeSoundness_of_rbrKnowledgeSoundness_of_guarded`); its straightline
  extractor folds the round-by-round extractor backward over the actual transcript.
  `Security/GuardedSoundness.lean` gives the corresponding soundness bridges
  (`Verifier.GuardedForm.soundness_of_rbrSoundness`,
  `OracleVerifier.soundness_of_rbrSoundness_of_guarded`).
- Measured extraction lives in `Security/Resources.lean`. Its game-independent core is
  `OracleComp.MeasuredProgram` in
  `VCVio.OracleComp.QueryTracking.MeasuredProgram`:
  an uncharged input view, an instruction program, deterministic handlers and declared charges.
  `Realizes` is output equality; `CostAtMost` bounds every permitted completed instruction path.
  `BudgetedProgram f` bundles both proofs, and `ofFun` realizes every function with zero budget.
  These facts do not certify host computation time or operational identity with arbitrary code.
  The legacy `RealizesExtractor` identifies the same extractor's monadic result with that run;
  `knowledgeSoundnessWithResources` adds its game and raw count profile `Kind → ℕ`.
  Native `Interaction/Oracle/Security/KnowledgeResources.lean` defines `RoundExtractor.stageMap`,
  per-node `MeasuredStages` and `BudgetAtMost`. Generic stages remain weighted; public
  `MeasuredKnowledgeCertificate Kind` and legacy count contracts require `[Finite Kind]` and
  standard profiles `Kind → ℕ`. Pricing coordinates is a separate justified valuation step.
  `KnowledgeResources/Composition.lean` composes named programs on a supplied typed path:
  `programAlong` returns the same `extractWitness`, and `programAlong_budget_le` bounds its
  budget by `path.length • bound` under a common local bound.
  `StateRestorationResources.lean` supplies the
  [role-specific resource contract](../design/03a-extractor-efficiency.md#state-restoration-resource-contract),
  including the all-witness identity to the game's `extractInputWitness`. The
  [common accounting boundary](../design/03a-extractor-efficiency.md#proof-and-accounting-boundary)
  applies to every count certificate, and the
  [native composition priorities](../design/05-roadmap.md#native-resource-composition) record
  the remaining client and resource-closure proofs.
  Acceptance clients are `ArkLibTest/OracleReduction/MeasuredExtraction.lean` and
  `ArkLibTest/Interaction/Oracle/Security/{StateRestorationBudget,MeasuredPathBudgets}.lean`.
  `VCVio.OracleComp.QueryTracking.DeterminedCost`
  turns the handler's recorded-cost bound into an all-path bound when every permitted response
  equals the handler's answer.
- Coordinate-wise special soundness ([FMN24]/[NOZ26]) lives in
  `Security/CoordinateWiseSpecialSoundness/`: `Basic` defines the `SS(S, ℓ, k)` combinatorics
  (`CoordEq`, `IsSpecialSoundFamily`), `CWSSStructure`, `CWSSStructure.toShape`, and both forms
  of the soundness notion — the **named-extractor form**
  `Verifier.coordinateWiseSpecialSoundWith` (the content-bearing statement; the extractor is an
  explicit parameter) and its existential closure `Verifier.coordinateWiseSpecialSound` (plumbing;
  it loses the algorithm, so advertised protocol statements use the named form) — plus their
  escape-threaded twins `…WithEscape` / `…Escape` and the lossless lift
  `coordinateWiseSpecialSoundWith.withEscape`; `Composition`
  transports CWSS structures across protocol append and proves binary append preservation
  via the generic transcript-tree split, in all forms (the composed extractor is the left
  factor's on the prefix tree, the composed event is `ChallengeTree.EscapeEvent.append`), and hosts
  the two directions of the pure-verifier acceptance bridge (`pure_accepting_of_mem` /
  `mem_of_pure_accepting`); `NoChallenge` supplies the empty-challenge base case. **Composition is
  binary only** — there is no n-ary CWSS `seqCompose`; chains are built by recursion over the binary
  append (`▷`), which keeps the composed extractor a nameable function. All CWSS packages
  (`CWSSPackage` and its guarded / escape-aware variants) carry their extraction algorithm as an
  explicit `extractor` field, with the `isCWSS` certificate stated at it — so a composed chain
  exposes an actual end-to-end extractor (`chain.extractor`). `NoChallenge` also provides
  `CWSSStructure.ofIsEmpty`, the concrete
  challenge-free structure used as the left factor when appending a zero-round `ReduceClaim` head
  (e.g. Hachi's `bridgeVerifier`). `SingleRound` is the generic single-challenge-round navigation
  layer (tree shape recovery `tree_shape`, the star-center machinery, the tree extractor
  `treeExtractor`, and the assemblies `coordinateWiseSpecialSoundWith_of_mkWitness` and its escape
  twin at the induced event `escEvent`) used by Hachi's polynomial-evaluation reduction `QuadEval`
  (Lemma 8). `ScalarRound` is its **proven** `(ℓ = 1, k)` scalar-challenge twin (`pSpecScalar`,
  `scalarStructure`, readers/shape recovery, the per-branch transcript kit,
  `treeExtractorScalar`, `escEventScalar(OfValid)`, and both assemblies
  `coordinateWiseSpecialSoundWith(Escape)_of_mkWitness_scalar`) for Hachi's Lemmas 9/11-shaped
  rounds and the DP24 batching wire format. `CommittedScalar` is the **proven** commit-then-
  scalar-challenge shell on top of `ScalarRound`: `BindingCommitment` (a commitment indexed by the
  shortness regime its binding is restricted to, with its short-collision set `Collision`), the
  anchored relation/verifier/prover, the plain assembler `mkWitness`, the binding-break escape
  event `escEvent`, the named `treeExtractor`, and its generic certificate + `EscapeCWSSPackage`;
  instantiated by the generic HMZ25 lift (`ProofSystem/RingSwitching/Lift/`) and through it by
  Hachi's ring switch. `Escape` is the **package lattice**: the escape-aware packages
  `EscapeCWSSPackage`/`EscapeGCWSSPackage` (ordinary relations and extractor, plus one `esc`
  **event** field), the lossless kind lifts `toEscape`/`toGuarded`, all mixed appends, and the
  universal `▷` elaborator dispatching over the 2×2 grid escape? × guarded?. Since escapes are
  events on `(statement, tree)`, composition matches only relation seams. `Guarded` is the
  **proven** runtime-rejection layer over the guarded verifiers of `Security/Guarded.lean`: the
  guarded package `GCWSSPackage` with its append `▷ᵍ`, the `Verifier.Outputs`-level guarded seam
  lemmas, and both guarded binary CWSS append theorems (plain and escape-threaded). The umbrella
  `CoordinateWiseSpecialSoundness.lean` re-exports the core files.
- Active areas are often grouped by paper or protocol family, for example
  `Data/CodingTheory/ProximityGap/BCIKS20/...` or `ProofSystem/Binius/...`.
- `ProofSystem/Binius/` holds the Binary Basefold protocol and its tensor-prefix frontend.
  `BinaryBasefold/Prelude/` and `Code` provide folding algebra and unique decoding;
  `Basic`, `OracleSpec`, `Spec` and `Relations` define protocol indices, messages and relations.
  `Soundness/` proves incremental folding and repeated-query bounds. `ReductionLogic` and
  `Steps/` connect those statements to oracle reductions; `CoreInteractionPhase/` composes the
  steps, `QueryPhase/` implements proximity queries and `General` composes the full protocol.
  `Commitment` owns the first-oracle interface, and `Opening` supplies multilinear opening with
  exact-encoding completeness and unique-radius round-by-round security. `FRIBinius/Prelude`
  instantiates the tensor profile; `FRIBinius/RingSwitch` composes the shared prefix reduction
  with Binary Basefold opening. See the [consumer guide](ring-switching-consumers.md).

- The ABF26 Section 6 toy IOP lives under `ProofSystem/ToyProblem/`. `Spec/` contains the
  domain-generic protocol and extraction theorems, `Impl/IRS.lean` supplies the computable
  interleaved Reed--Solomon extractor, `Impl/FRS.lean` contains neutral KoalaBear folded-RS
  reference points, and `Codegen.lean` enforces compiler-IR availability. The simplified IOR
  (`SimplifiedIOR`) is an `OracleReduction` with a query-by-query virtual output oracle and
  exact named interleaved-RS straightline and RBR extractors. The compiled small-parameter
  checks run with
  `lake exe toyproblem-runtime`; the security theorems themselves are parametric in the code, the
  radius, and the repetition count, so they apply at production sizes without evaluation. Turning
  such a theorem into a *numeric* error value additionally requires the MCA/CA capacity bounds in
  `Data/CodingTheory/ProximityGap/CapacityBounds`, all proven except ABF26 Theorem 4.16 (a
  solicited proof, [#1352](https://github.com/Verified-zkEVM/ArkLib/issues/1352)),
  deliberately outside the toy-problem import cone; no numeric error value is proven in-tree at
  any production shape.
- Batched FRI takes a proximity generator `G : S → Fin (m + 1) → F`. Its single
  uniformly sampled seed selects the coefficients of the virtual output word. Compose
  `BatchingRound.batchOracleReduction s d m G` directly with `Fri.Spec.reduction`, as
  `BatchedFri.Spec.batchedFRIreduction` does. The input relation carries degree-bounded
  polynomial witnesses agreeing with all input words on one common set of density at least
  `1 - δ`; the output relation is definitionally FRI's input relation.
  `BatchedFri/Security.lean` proves perfect completeness at every radius and ordinary and
  round-by-round soundness for any `ε` bounding `caError G C δ δ`.
  `BatchedFri/EndToEnd.lean` adds the FRI soundness error and proves composite perfect
  completeness at radius zero. Neither generic soundness theorem restricts the radius.
  Family corollaries instantiate these bounds:
  - `soundness_affineSpace` / `batchedFRI_soundness_affineSpace`: independent coefficients,
    error `errorBound`, for `0 < δ < 1 - √ρ`.
  - `soundness_powers` / `batchedFRI_soundness_powers`: powers `(1,r,…,r^m)`, error
    `m * errorBound`, in the same open Johnson regime.
  - `soundness_multilinear` / `batchedFRI_soundness_multilinear`: `2^t` words with monomial
    tensor coefficients, error `t * n / |F|`, for positive radius at most the relative
    unique-decoding radius. Here `n` is the code length. At `t = 2` the coefficient order
    is `[1, r₁, r₀, r₀*r₁]`. The additional `_multilinear_johnson` corollaries use
    `t * affineLineMcaJohnsonError` below the proved 1.5-Johnson radius
    `δ ≤ 1 - (1 - δ_min + η)^(1/3)`, with `δ_min = minDist(C)/n` and
    `0 < η < δ_min`. The numeric error is defined in `Multilinear.lean`.
  `Data/CodingTheory/ProximityGap/BCIKS20/GeneratorBounds.lean` supplies the first two numeric
  bounds. `Data/CodingTheory/ProximityGenerator/MultilinearBasic.lean` defines the executable
  tensor generator; `Multilinear.lean` proves the third bound using the additive tensor MCA
  theorem and the proved
  affine-line unique-decoding estimate. Its 1.5-Johnson alternative uses
  `linear_mcaError_le_one_point_five_johnson`; neither result uses the
  Reed–Solomon Johnson bound proved via [DKT26].
  `multilinearBatchGenerator` presents the same coefficients at index `Fin ((2^t - 1) + 1)`.
  Composite knowledge soundness remains out of scope because batching has no extractor.
  Executable examples, concrete soundness applications, and axiom checks are in
  `ArkLibTest/ProofSystem/BatchedFri.lean`.
- Binary sequential composition lives in `OracleReduction/Composition/Sequential/Append/`,
  exported by `Composition/Sequential/Append.lean`:
  - `Append/Basic.lean` — the `append` operations on provers, verifiers, and reductions, their
    oracle-protocol counterparts, and challenge-sampling transport across `++ₚ`.
  - `Append/StateFunction.lean` — composition of straightline and round-by-round extractors, and
    of verifier state functions. After the seam the composed state function uses `S₁ ∨ S₂`.
  - `Append/Execution.lean` — running appended provers / verifiers. `Prover.append_run_of_seam`
    permits effectful left output when the suffix is empty or opens with a message;
    `Prover.append_run` specializes it to pure left output for arbitrary suffix protocols.
  - `Append/Simulation.lean` — exact simulation of both explicitly routed challenge inclusions
    and appended prover execution, including the final shared oracle state.
  - `Append/Completeness.lean` — quantitative completeness from exact simulated factorization,
    with seam and purity corollaries and state-uniform suffix correctness.
  - `Append/OneMessage.lean` — the one-message specialization with effectful prover outputs.
  - `Append/RoundByRound.lean` — composition from round-by-round bounds under a pure first verifier.
  - `Append/GuardedRoundByRound.lean` — round-by-round knowledge soundness composes
    from round-by-round component bounds under a guarded first verifier, with the composed extractor
    and knowledge state function (`KnowledgeStateFunction.appendGuarded`) named; the components
    share only the intermediate relation.
  - `Append/ProverSplit.lean` — arbitrary prover restrictions retaining shared state at the seam.
  - `Append/OrdinaryComposition.lean` — prefix extraction and ordinary bad-event bounds.
  - `Append/Security.lean` — proved guarded ordinary soundness and pure-extractor knowledge
    soundness, with a guarded first verifier and a suffix bound valid from every deterministic
    shared oracle state.
  - `Append/NoAmbient.lean` — ordinary composition with one initialization and no ambient oracles.

  `Sequential/Completeness.lean` adds finite-chain completeness for pure outputs/verdicts;
  `Sequential/GuardedCompleteness.lean` handles deterministic rejecting verifiers.
  `Sequential/GuardedNary.lean` extends guarded completeness to finite chains;
  `Sequential/GuardedRoundByRound.lean` extends guarded round-by-round knowledge
  soundness to finite chains, requiring round-by-round bounds and guardedness for every component,
  with the `seqCompose` error reindexing proved;
  `Sequential/OracleCompleteness.lean` supplies binary and finite-chain oracle-reduction wrappers.
  `Sequential/GuardedNary.lean` also gives the guarded form of an appended or sequentially
  composed oracle verifier from its components' (`OracleVerifier.appendGuardedForm`,
  `OracleVerifier.seqComposeGuardedForm`). `OracleReduction/CastIdx.lean` moves an oracle verifier
  or reduction along equalities of the indices of its statement, oracle-statement and witness
  families (`OracleVerifier.castIdx`, `OracleReduction.castIdx`), with the
  round-by-round knowledge soundness, perfect completeness and guarded form moving along.
  `Sequential/NoAmbient.lean` proves output purity for empty ambient oracles and constructs guarded
  forms from explicit fallback maps. `LiftContext/Purity.lean` transports output purity and guarded
  forms through context lifting.
  See [sequential composition](sequential-composition.md) for theorem selection and hypotheses.
  `ArkLibTest/OracleReduction/Composition/Sequential/` contains acceptance examples, query-order
  and shared-state counterexamples, and axiom assertions, built by `lake test`.

  These proofs run on `HEq` transport, since transcripts and prover states are families indexed by
  the round number. The generic congruence lemmas for that (`heq_apply`, `heq_funext`, `heq_pi`,
  `heq_bind`, …) live in `ToMathlib/Logic/HEq.lean`, and the `ℕ`-indexed `HEq` computation rules for
  `Transcript.concat`, with the extensionality lemma `Transcript.heq_ext`, next to `concat` itself
  in `ProtocolSpec/Basic.lean` — put new ones there rather than re-deriving them privately per
  module.
- Virtual-output execution commutes through append, salt, cast, and executable lifting.
  Ordinary soundness and knowledge soundness compose through `Append/Security.lean` under a
  guarded first verifier and state-uniform suffix bounds, with pure extractors for knowledge
  soundness. Round-by-round knowledge soundness composes through
  `Append/GuardedRoundByRound.lean` from round-by-round component bounds and a guarded first
  verifier. `Sequential/GuardedRoundByRound.lean` requires round-by-round bounds and guardedness
  for every component of a finite chain. Completeness composition uses explicit shared-state
  hypotheses.
- Ring switching has two construction families, routed by
  `ProofSystem/RingSwitching/Basic.lean`. Packing groups independent coordinates; `Lift` replaces
  quotient equalities by polynomial equalities before evaluating them.
  `Packing/Coordinates`, `FiniteObservation`, `CheckedObservation`, `Polynomial`, `Relations`
  and `Multiplier` own the pure coordinate laws, polynomial round trips, derived slices and
  read-once matrix multiplier. `ClaimLayout` and `ClaimLayout/Quirky` supply certified prefix,
  suffix and Lagrange layouts. `BatchingRule` is operational sampling/weight data;
  `BatchingStrategy` adds a collision certificate. `Batching` and `DerivedBatching` provide fixed
  candidate-list bounds, charging only incorrect candidates. The list is fixed before the
  challenge and covers all compatible packed candidates.
  `PackedCommitment` contains oracle semantics, functionality and contextual evaluation relations;
  its separate `Honest` constructor certifies coverage. `Head` implements one encoded message and
  one batching challenge, retaining the original query and oracle collection. `ProductSumcheck/`
  owns the scalar rounds, residual relation, matrix terminal check and guarded composition on the
  same packed witness. `RingSwitch` composes them directly, with exact challenge-error sum
  `bat.error + 2m/card C`; it also closes any opening already typed at the contextual evaluation
  endpoint through `append_perfectCompleteness` and `append_rbrKnowledgeSoundness`.
  Completeness uses a commutative challenge ring; full security uses finite sampling, no zero
  divisors, functional compatibility and injective packing-to-challenge coefficient transport.
  The head's point-local collision law needs only equal component evaluations among compatible
  polynomials at the fixed query; its standalone RBR variant uses that premise at every query/oracle
  statement without polynomial uniqueness. Its separate fixed-list
  alternative does not provide full-tail list security or transport inherited source invariants.
  `TensorPrefix` is the equal-algebra prefix specialization: the transmitted carrier
  remains `P.A`, decoded by `P.columnEquiv`. Its original scalar check, row target, honest message,
  packed source, extractor and matrix terminal equations are proved against that single program.
  `Profile`, `Algebra`, `ProfileCoordinates`, `ProfileLayout`, `BatchingAlgebra` and `FinalAlgebra`
  retain the tensor-coordinate algebra. `Packing/Conformance` states pure prefix/carrier laws.
  `Binius/FRIBinius/Conformance` identifies source and exact first-oracle inputs;
  `Binius/FRIBinius/RingSwitch` composes the shared frontend with the Binary Basefold
  contextual opening. Completeness uses exact encodings, security unique-radius compatibility.
  `Packing/OpeningAdapter` transports a standard `MLIOPCS` to the contextual opening contract
  through a zero-round projection, preserving completeness and round-by-round security.
  `ArkLibTest/ProofSystem/RingSwitching/Packing/RingSwitch/{UnequalRankSuffix,Quirky}` instantiate full protocols
  with effective ranks four/three over different fields and exact error sum below one. Their
  transparent polynomial oracles are specification fixtures, not commitment schemes.
  Hachi's §3.1 trace head uses `PackingData.ofBaseOpening`, `packedMLE`, its own `ClaimLayout`
  and `CheckedObservation`, with its conformance to the shared layer in `TraceHead/Conformance`.
  It retains its own deterministic wire. Obligations for the reference Flock in the interaction
  layer are listed in the
  [consumer guide](ring-switching-consumers.md#flock-in-the-interaction-layer-and-acceptance).
  `Lift/` is the **generic HMZ25 lift** (large quotient ring →
  field, CWSS at `k = 2d`): `Presentation.lean` is its data layer (proof-free
  `Presentation R S` + `IsPresentation` laws over any monic modulus — not cyclotomic-specific
  — with the full lift algebra and interpolation engine proven over the laws), and
  `Reduction.lean` is the protocol layer over the committed-scalar shell
  (`OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean`), with the
  recovery obligation proven generically. Hachi's `Commitments/Functional/Hachi/RingSwitch/`
  is its cyclotomic instance, with law-discharge lemmas in
  `Data/Lattices/CyclotomicRing/QuotientLift.lean`. What the two families share lives at the
  folder top level — the check-then-update round-shape verifiers (`RoundVerifiers.lean`,
  over the `pSpecScalar` wire shape and the one-message `pSpecMessage` wire) and the
  embed-and-evaluate transport algebra (`Transport/Eval.lean`, `Transport/Coeffs.lean`) — plus the
  committed-scalar seam under `OracleReduction/`.
  Background: KB concept page `docs/kb/concepts/ring-switching.md`; blueprint section
  `proof_systems/ring_switching.tex`. Structured sum-check support lives in
  `ProofSystem/Sumcheck/Structured*` and `ProofSystem/Sumcheck/Domain.lean`; the round algebra
  (round-polynomial sums, the `d/|L|` collision bound) is in
  `Sumcheck/Structured/RoundLemmas.lean`, over the prefix-fixing algebra in
  `Data/MvPolynomial/RestrictDegree.lean` and the root bound
  `Probability.prob_polynomial_eval_eq_le`.
- Before assuming a file is authoritative, check whether it is source or derived output. See
  [`generated-files.md`](generated-files.md).

## Acceptance tests

`ArkLibTest/` mirrors production module paths for compile-time examples and regression tests.
`lake test` builds all test modules; the default validation wrapper runs it. Tests stay outside
the generated `ArkLib.lean` umbrella and production modules must not import them.
`ArkLibTest/Interaction/Core/` holds the rebuilt core's tests: `Plain.lean` (shapes, recorded
challenges and the public-coin sampler), `Oracle.lean` (query-only decisions and output
oracles), `Composition.lean` (routed composed oracle queries) and `Security.lean`
(classical-model and round-by-round security).