The three honest residuals recorded this morning are now CLOSED (details: docs/analysis/MULTISTAGE_EXTRACTION.md, docs/analysis/D4_BINDING_CLOSURE.md, BENCHMARKS §2l):

1. The multi-stage LaBRADOR extraction — the degree-law unwind (lattice-widthfold::extraction): the open analysis is now an executable, fail-closed ledger of five machine-checked laws (E1 per-stage floor+grinding, E2 the affine degree law / composed degree 2L, E3 the unwind norm law 2·β_{L+1} < q/2, E4 the grinding ledger, E5 the extractor-feasibility cap 2^L ≤ 2^16) — ENFORCED inside assert_sound_chain at prove AND verify time, so no chain can ship without its extraction posture. The ledger separates the knowledge gap (the rewind abort — 2^0.6–2^3.2 bits on shipped schedules) from the binding security (the MSIS floor — 161–841 bits): the former is a rewinding-completeness quantity, NOT the forgery security; conflating them is the analysis error the document exists to prevent. The three-layer honesty (arithmetic / modeled / assumed) is stated explicitly per field.
2. The D4 binding closure (lattice-akita::salsa_binding): the byte-witness-to-commitment authenticated opening is CLOSED via the compact-fold composition — the width-collapse chain PROVES the level-1 F̄·v = t equation ((W0) — never assumed, so the level-1 key's own MSIS comfort zone is irrelevant), carries the functional claim ((W0')/(W3)), and rests the binding on the per-stage estimator-gated [A₂ | −T] instances. Pinned by the wrong-commitment tamper test; composed into the v2 pipeline as Stage5Mode::Bound (the swapped-commitment rejection at Stage 5). The D1 norm proof remains the β₁ = 255 gate's shortness certificate. The r-column split scales past the Lemma-4 cap (exactly 2,048 values/commitment at ring dim 16/Q_32) with per-column keys/D1/chains and the μ-weighted ψ-decomposition — the per-column keys derive from a PUBLIC domain (the reference posture; production requires a setup ceremony — recorded in the analysis doc's §4).
3. The known-open items after this landing (unchanged in kind, now measured): the Q_32 norm ceiling (the unwind slack 2^6.6 at the β₁ = 2^15+ rows — the Modulus-50 class is the route); zero-knowledge for the fold/response layers (Wave 8.6); the estimator remains a model, not a theorem; FS rewinding soundness and transcript collision resistance remain standard assumptions.

Three posture changes this session:

1. The recursive width-collapse staging (lattice-widthfold::chain): the Sound profile's binding is now a CHAIN of per-stage [A₂ | −T] instances, every one estimator-gated at ≥ 128 classical bits PLUS the 32-bit replay-grinding allowance (CHAIN_GRINDING_BITS — the per-stage challenge spaces |C_ℓ| = (2A₂+1)^{r₂} admit replay grinding; the chain charges the total against every stage's floor, fail-closed). The honest residual — the full multi-stage LaBRADOR extraction (the degree-law unwind across stages to the level-1 response) — remains the open analysis, documented in the module; the conservative shipping posture is the per-stage floor + the (W0) target threading (each stage's public target is the previous stage's committed T combination). The measured boundary table (--example chain_coverage) replaces the single-stage n̄ ≤ 16 ceiling with the staged coverage (n̄ ≤ 4096 at the byte gate; the Q_32 norm headroom is the binding constraint beyond — the Modulus-50 class is the honest fix, not more stages).
2. SALSA D4 (the Akita/zkVM response-layer swap): the byte-packed D1 chain certifies the byte-witness's norm (the Ajtai commitment's security precondition) with the Lemma-4 no-wraparound gate; the ψ-functional carrier binds the response INTRA-layer (the claims → the carrier → f(r_sc) → the byte-witness's MLE → D1's terminal). The byte-witness-to-commitment Ajtai binding (the authenticated opening at the challenge) remains the documented gap at the pipeline2 layer — the binding-complete polylog route is the compact-mode fold (the Sound profile), which now extends to the benchmark streams via (1).
3. The Cyclo §7 bridge's compact terminal: the decider's (D1) verify_opening is replaced by the fold's (W0) commitment check; the lift's norm precondition ∥z'∥∞ < k enters as the fold's β₁ (the estimator's bound accounting) rather than the clear decider's explicit per-element gate — the honest deviation recorded in cyclo.md's ledger (the folded response's (W4) gate is direct; the parts' norm story rides the (W2) extraction discipline).

The LZX workspace is a lattice-based post-quantum zkVM kernel implementation (15+ crates, pure std, zero external dependencies). This document states the security claims, the capability discipline, and the reporting process required by the implementation audit.

A proof produced by this codebase carries exactly the capabilities granted by lattice-zk::privacy_spec::CapabilitySet — never more:

A proof is never "zk" merely because its PCS is lattice-based. The Akita evaluation path (prove_evaluation) opens the committed witness in the clear; genuine zero knowledge flows only through the lattice-zk layer (blinded sumcheck + ABDLOP linear proofs).

• The ZK constructions are implemented and KAT-tested at kernel-scale parameters (vectors ≤ 2^4 entries, m ≤ 200 commitment slots). Production parameters (and the associated smoothing/regression analysis for the Ajtai hiding argument) require the external review of gate G8 before the ZeroKnowledge capability is granted for production-sized statements.
• The rejection-sampling margin in ZkLinearProof must satisfy norm_bound ≫ (n/2)·|s|; parameter sets violating this degrade HVZK statistically (see zk_linear.rs tests for the enforced margins).

1. LinearProof Fiat-Shamir malleability (wave 3): the challenge was derived from the statement only — the masking commitment w was not absorbed first. Post-hoc forgery: choose any short z', set w' := A·z' − c·t. Fixed by absorbing (w, images) before the challenge; regression-tested in lattice-commitment and lattice-zk.
2. Degenerate short-secret sampling (wave 3): sample_small_secret requested 8 + 4·i XOF bytes per ring element, silently zero-filling most coefficients — collapsed masking entropy across every Lyubashevsky-style proof. Fixed with a full rejection budget per element.
3. Envelope allocation bomb (wave 3): the section-count × section-size caps allowed ~1 GiB allocation before validation; now a total-bytes cap (MAX_TOTAL_SECTION_BYTES) is enforced before any section allocation.
4. Four RV64 conformance bugs (wave 3, found by the differential corpus): unaligned LD/SD word-straddle semantics, SRLI/SRAI shamt ≥ 32 funct6 decoding, SLLIW/SRLIW/SRAIW decoding as 64-bit shifts, LUI/AUIPC missing sign extension.

• No panics on untrusted bytes: fuzz-tested entry points (envelope::from_bytes, AjtaiCommitment::from_bytes) with structured bombs and 4 000 random mutations.
• All length/offset arithmetic is checked; allocation caps are enforced before allocation.
• QROM attestations are verified before transcript replay or expensive arithmetic.

• Private masking randomness comes only from lattice_zk::entropy (OS /dev/urandom or explicitly-labeled test seeds). Transcript-derived randomness is public by construction and structurally cannot seed a SecretSeed.
• Seed reuse across proofs is a nonce collision — detected by NonceLedger at proof time.

Security issues follow the audit's gate G6 process:

1. Reproduce with a minimized test (the workspace's deterministic transcripts and KAT seeds make reproduction exact).
2. Classify against the threat model (audit §10.1: malicious prover / malicious proof bytes / malicious program / side channel / supply chain / quantum adversary).
3. Fix + regression test + capability re-review (the affected capability token is suspended until the fix lands).
4. Record the post-mortem in this file.

• Zero external crates; cargo metadata must show no registry dependencies. Builds use a pinned stable toolchain; release artifacts must record the toolchain digest (gate G8 checklist).

1. The bits-bundle vacuous-gate fix (a security defect, not just size): the old packing put 31 bits per coefficient against q = 3·2^30+1 (q/2 ≈ 2^30.6) — the balanced-representative norm claim was ambiguous mod q. The compact mode's 1-byte-per-coefficient packing bounds every committed coefficient by 255, restoring the norm gate's meaning.
2. The two-characteristic discipline: the legs' claims are Goldilocks values; the commitments live in R_q. No homomorphism connects the fields (verified live during implementation — the F_q carrier's evaluation diverges from the lifted Goldilocks claim), so the compact design keeps the carrier over Goldilocks and closes the fold with SCALAR challenges: the integer fold never wraps mod q (the gate bounds r·A·255 < q/2), so the Goldilocks evaluation functional commutes exactly through the fold. Cross-field claim lifting is forbidden by construction.
3. Soundness chain: legs → carrier (Goldilocks sumcheck) → w = f(r_sc) → the MLE interpolation over columns pins the ũ's → the commuting functional pins ũ to the response v → the Ajtai fold F̄·v = Σ d_j·y_j pins v to the commitments → MSIS on [F̄ | −y₁..−y_r] at the relaxed bound (2× the gate) with the mixed-moduli constraint lattice. Extraction needs no ring divisions (Q_32 splits completely — division by challenge differences is unsound there).
4. Fail-closed gates: per-coefficient norm gate (< q/2, checked on prove and verify); the r-alignment precondition (r ≤ every factor length); the response codec's strict decode; the values-only claims queue must drain exactly (reordered or missing claims rejected); commitment/width/factor-length shape checks.
5. Challenge family: scalar d_j ∈ [−2^12, 2^12] drawn after the ũ absorption; the response is a deterministic function of the committed columns (no prover adaptation surface). The forgery resistance reduces to the CVP hardness of the constraint lattice at the honest-gap regime — the parameter knobs (k, r, the gate) are documented in DESIGN_50KB.md for estimator-driven tightening.
6. Tamper coverage (test-pinned): wrong final registers, wrong program digest, wrong claim value, reordered claims, tampered carrier terminal, tampered ũ, tampered response bits, tampered commitment bytes, wrong seed, tampered widths — all rejected.

lattice-sis-estimator/examples/fold_security_table.rs runs the ADPS16 estimator on the compact fold's actual instances (q = 3·2^30+1, ring N = 64, m = (n̄ + r)·64, the relaxed 2× bound; scalar convention per scalar_sis_from_ring). The pre-estimator assertion in note 5 above ("the lattice covering radius at the chosen (k, n̄) far above the gate") does not survive the run:

The finding: the single-level fold at the benchmark response lengths (n̄ in the hundreds) buys the 27 KB size, not the MSIS binding — m/n in the tens puts every instance in the combinatorial regime regardless of the gate. The knobs (k↑, r↓, A↓, the statistical gate) do not close the gap at these lengths: reaching 128 bits at n̄ ≥ 8 requires k ≥ 16, whose commitments (r·k·64·4 bytes) alone exceed the 50 KB budget.

The sound posture (the roadmap's own Stage 5.2, now estimator- mandated): the second-level fold (lattice-zkvm/src/second_fold.rs, landed) — the LaBRADOR-decider amortization: the level-1 responses of r bundles sharing the column key fold into ONE short response bound by a fresh Ajtai key at the estimator's sound row (κ = 4, n̄ ∈ {2, 4}, r = 4, A = 2^8 → 329+ classical bits, re-verified FAIL-CLOSED at construction by the estimator-gated profile). Every check is exact and linear — the public-target fold F̄·z = Σ γ_i·t_i, the short-key binding A₂·z = Σ γ_i·T_i, the commuting functional Φ(z) = Σ γ_i·u_i — with no garbage terms.

The LaBRADOR tail — LANDED (2026-10-04, the width fold): the width-reducing fold (lattice-zkvm/src/width_fold.rs) implements the quadratic-garbage construction the honest finding mandates: the wide level-1 response splits into r₂ parts whose link images p_i and cross terms G_ij = F̄_{(i)}·s_j are committed BEFORE the challenges (the symmetrized quadratic form Σ_{i,j} γ_i γ_j G_ij with G_ii = p_i), the folded z ∈ R^w binds through the short instance [A₂ | −T] at (w, r₂, κ, A₂) = (8, 2, 8, 2^2–2^4) (206–1,855 classical bits over the real level-1 gates — the width_fold_table example's verdict), and the functional layer rides the same pre- challenge discipline (the g_ij = ψ^{(i)}(s_j) superposition fix — the per-slice (W3) identities). The Sound compact profile (compact.rs::CompactProfile::Sound + memproof.rs:: prove_memory_argument_sound) consumes it live: the level-1 response is never transmitted, so the level-1 [F̄ | −y] instance never arises — the binding of the whole opening is [A₂ | −T], fail-closed by the estimator-gated profile at prove AND verify (the posture marker re-derivation). The single-stage coverage ends at n̄ ≤ 16 (β₁ ≤ 2^20 at A₁ = 2^4); beyond it the profile refuses rather than shipping a broken binding (the recursive staging and the Modulus-50 class are the documented follow-ups). The measured honest price at the test scale: 129.7 KB vs the compact mode's ~60 KB (BENCHMARKS §2j) — the quadratic garbage's cost, the estimator-mandated trade.

The table itself regenerates with: cargo run --release -p lattice-sis-estimator --example fold_security_table (and the width fold's own regime: cargo run --release -p lattice-sis-estimator --example width_fold_table).

blockfold.rs replaces the compact mode's r per-column Ajtai commitments y_j = F̄·w_j (the column-uniform key) with ONE packed block commitment y = F·vec(W) under the wide seeded key F ∈ R_q^{k×m}, m = r·n̄^pad, and replaces the linear fold check F̄·v = Σ_j d_j·y_j with the fused binding sumcheck:

• the verifier derives ρ ∈ Z_q^k, h ∈ R^{n̄}, β ∈ R, computes g := Σ_l ρ_l·F[l] (one streamed key pass) and c_y := Σ_l ρ_l·y_l, and checks ⟨β, Σ_p c_p·w_p⟩ = ⟨β, c_y + ⟨h, v⟩⟩ by a degree-2 sumcheck over the m-entry cube, with the public C̃ factor and the prover's terminal ring element ŵ: ⟨β, C̃(τ)·ŵ⟩ = final claim;
• the binding chain: carrier w ← interpolation ← ũ_j ← functional commute Φ(v) = Σ d_j·ũ_j ← the h-half pins v ← the W-side round messages + ŵ ← the g-half pins y (⟨g, W⟩ = ⟨ρ, y⟩).

Why the linear check had to go: a single linear Ajtai commitment cannot be checked against the folded short response by any linear relation — ⟨ρ, y⟩ = ⟨Fᵀρ, W⟩ and ⟨μ, v⟩ = ⟨d⊗μ, W⟩ span generically-transversal subspaces, so the per-column granularity of the old check was load-bearing; removing it REQUIRES a sumcheck to carry the binding. This is exactly Akita's fused Eq-160 pattern — the "outer layer" gap the research consensus documented.

The block-geometry MSIS table — RUN (2026-10-06): cargo run --release -p lattice-sis-estimator --example block_geometry_table (both norms, the Akita exact-ℓ2 discipline). The verdict, at the benchmark bundle shapes (m_ring = r·n̄^pad ∈ [2048, 4096]):

• the byte-bound homogeneous instance (two W-side openings of one y — the block's distinctive preimage, coefficients ≤ 255, r/A-INDEPENDENT): k=2 → 31.8 bits (broken), k=4 → 98.1, k=8 → 253 classical bits; the exact-ℓ2 6σ path agrees;
• the conservative composed reading ([F | −y] with the gate regime 2·r·A·255): k=16 reaches 128 classical bits, stable across every bundle shape — the ladder is SECURITY_K = 16 (shipped);
• the honest comparison: at equal k the block-byte instance BEATS the compact's gate instance (31.8 vs 11.7 at k=2; 253 vs 61 at k=8) — the byte bound more than pays for the wide instance's extra attack freedom (the earlier "strengthens the m/n regime" intuition had the mechanism backwards; the outcome holds);
• the streamed key expansion (below) makes the k-ladder memory-free on the verification side — the security knob costs O(m) verifier state, not O(k·m).

The honest gaps (recorded, not hidden):

1. The composite extractor (sumcheck rewinding over (ρ, h, β, τ) composed with the Ajtai relation, terminating in MSIS on the wide [F | −y] with the byte-bounded preimage and the norm-gated response difference) is argued at the engineering level, not a written formal reduction. The estimator table for the block geometry IS now run (above); the residual is the formal reduction write-up.
2. The degree-2 sumcheck's soundness over Z_q (q prime, ≈ 2^31.6) gives ~31 bits per round × log₂m rounds — the binding is information-theoretically strong at the cube sizes in play, but the two-round rewinding schedule (the standard strong extractability argument for linear-PCS-style sumchecks) is not written out.
3. CLOSED (2026-10-06): the verifier's key passes are STREAMED (streamed_c_array) — each key column regenerates from the seed with the SAME flat l-major indexing AjtaiPublicKey::from_seed uses, g_p accumulates in place, and the public C-array fuses into the one pass: O(m + n̄ + k) verifier state (bit-identical to the materialized route, pinned by a dedicated test). This is Akita's setup-offloading discipline in the seeded-key regime — the strictly simpler case, since the key is transcript-derived and public (no commitment of the setup matrix needed).

The per-column compact mode (compact.rs) is UNCHANGED and remains the default; the block mode (prove_memory_argument_block) is the committed-optimization path selected by the benchmark harness.