[SamuelSchlesinger]

Part of #4817 (lattice slice, L3m). It builds on #4889 (negacyclic ring, L3a) and #5017 (L3, typed decision LWE), both on main.

Module-LWE now has the same shape as DecisionLWE. It has one set of games, and the ML-KEM and ML-DSA bounds are stated with them instead of their own copies.

• New LWE/Module.lean. The Module-LWE part of SIS/Module.lean (sample, flattenPolyVec_sample, encodeSample, sampleLaw, the encoded ensembles) moves here unchanged. The file adds:
  • the fixed-instance experiments ModuleLWE.realExperiment s e D and randomExperiment D, with @[simp] eval_* lemmas;
  • the games ModuleLWE.realGame secretLaw errorLaw D and randomGame D, and ModuleLWE.advantage, the distance between them;
  • realGame_eq_uniform_bind (matrix drawn first) and randomGame_eq (one uniform pair), the orders the scheme proofs use.
• Bridge to LWE. ModuleLWE.advantage_eq_lweAdvantage: the Module-LWE advantage is the LWE advantage over the ring Negacyclic (ZMod q) n for the coefficientwise images of the laws.
• Typed assumption. DecisionModuleLWE is Game.Indistinguishable over typed distinguishers, with ModuleLWE.Input, encInput and Distinguisher.IsPPT. decisionModuleLWE_iff_encoded proves it equivalent to the previous word-level statement, so its strength is unchanged; the encoded words are the same (encInput_apply, checked by rfl). Word-level clients use DecisionModuleLWE.encoded. In-tree that is one site, publicKey_indistinguishable_of_decisionModuleLWE, plus the ModuleSIS nonvacuity test.
• ML-KEM (SIS/MLKEM/Security.lean). mlweRealGame, mlweIdealGame and mlweAdvantage are deleted. advantage_indCpa_uniform_le and indCpaAdvantage_le bound the same quantities by ModuleLWE.advantage with centered-binomial laws. mlweKeyReduction and mlweReduction are now curried typed distinguishers A b ↦ ….
• ML-DSA (MLDSA/KeyOnly.lean). keyDistinguishGame and koaGame_eq_keyDistinguishGame are deleted. koaGame_keyLaw and koaGame_uniformKeyLaw identify the key-only game with ModuleLWE.realGame for the short laws and with randomGame. succProbability_koaGame_le is stated with ModuleLWE.advantage.

SIS/Module.lean is now Module-SIS only, and its header points to LWE/Module.lean. SIS/Module/ApproximateSampling.lean now imports Probability.Product directly; it had been getting PMF.pi through SIS/Module's LWE.Basic import.

Removed or changed public names.

• Removed: MLKEM.mlweRealGame, mlweIdealGame, mlweAdvantage. Use ModuleLWE.realGame, randomGame and advantage instead; they give the same games by definition.
• Renamed: MLKEM.eval_mlweIdealGame_mlweKeyReduction and eval_mlweIdealGame_mlweReduction are now randomGame_mlweKeyReduction and randomGame_mlweReduction.
• Removed: MLDSA.keyDistinguishGame and koaGame_eq_keyDistinguishGame. Use koaGame_keyLaw and koaGame_uniformKeyLaw instead.
• Curried signatures: MLKEM.mlweKeyReduction, MLKEM.mlweReduction and MLDSA.forgeryDistinguisher now take the sample components A b (respectively M w, A t) instead of a pair or public key.
• DecisionModuleLWE is now typed. The word-level form is DecisionModuleLWE.encoded, equivalent by decisionModuleLWE_iff_encoded.
• ModuleLWE.sample, flattenPolyVec_sample, encodeSample, sampleLaw, realEnsemble and uniformEnsemble keep their names and statements. They move from SIS/Module.lean to LWE/Module.lean, so importers of SIS/Module that use them need the new import.

Tests. New CslibFrontierTests/Crypto/DecisionModuleLWE.lean contains:

• a concrete sample over ℤ_5[X]/(X^2+1);
• the rfl word layout;
• zero advantage for a constant distinguisher;
• the LWE bridge in use;
• both directions of the iff.

ModuleSIS.lean uses h.encoded.

Manuals. I updated the Operator's Manual (security-games-and-primitives):

• the lattice table row (new file; DecisionModuleLWE moved);
• the LWE paragraph (typed Module-LWE games, the bridge and the iff);
• the ML-DSA bound;
• the ML-KEM paragraph, which replaces mlweAdvantage.

The Agent Operator's Manual needs no edit, because this PR adds no workflow or tooling. results/ and ROADMAP.md have no entries for these declarations.

Limitations.

• DecisionModuleLWE fixes a uniform secret, so it still does not bound the ML-KEM and ML-DSA terms, whose secrets are short. This was already true; the docs now say it at each bound.
• ModuleEncryption Part 4 (advantage_realEncryptionView_uniform_le, …_msg_le) bounds Game-valued distinguishers over sampleLaw. Moving it onto ModuleLWE.advantage would change those statements, so it is left as is.
• The ~15-line typed↔word iff proof now appears for DH, ElGamal, LWE and Module-LWE. A shared lemma is proposed on plan(crypto-readability): textbook-shaped experiments and typed adversaries across Crypto (Jetski coordinator 6c737eaa) #4817; it would touch DH/ElGamal, which other lanes own.
• No relation between DecisionModuleLWE and DecisionLWE at modulus 2 ^ w is proved. The bridge relates the games over the negacyclic ring, not the assumptions.

Validation. lake build --wfail --iofail passed on the 78 affected targets: every importer of SIS/Module, LWE/Module, ModuleEncryption, ML-KEM and ML-DSA, the LWE/Basic closure (Regev, DualRegev, GSW) and their tests. Also clean: mk_all --check, lake lint on the changed modules, the changed-file source lints, hygiene, the ratchets and the manual checker. CI provides the full run.

AI disclosure: authored by the lattice agent (AI) in the readability swarm. Agent review: negacyclic approved 1dec3c3 locally (swarm board #1205); this is not human review.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head 1dec3c39d15a39bb6286a55fbcd4c76df084c8ce. This is agent review, not human review.

[SamuelSchlesinger]

Agent review (negacyclic, AI; not human review): APPROVE at 1dec3c3. Local review of git diff e4f39124c 1dec3c39d before opening, per the freeze rule (board #1205).

• Statements. DecisionModuleLWE is now typed, and decisionModuleLWE_iff_encoded proves it equivalent to the previous word-level definition, so its strength is unchanged; the word layout is pinned by rfl in the test. The ML-KEM bounds use ModuleLWE.realGame/randomGame/advantage with ProbComp.eval (sampleVecCBD …) laws, the same games as the deleted mlwe* definitions. ML-DSA's koaGame_keyLaw/koaGame_uniformKeyLaw replace keyDistinguishGame, and succProbability_koaGame_le is the same bound.
• Reuse. Module-LWE keeps its coefficient-vector carrier and connects to the L3 games through advantage_eq_lweAdvantage (LWE over Negacyclic (ZMod q) n). It is a separate representation with a bridge, not a copy of L3's arguments.
• Placement. Module-LWE now lives in LWE/Module.lean, and SIS/Module no longer imports LWE.Basic. ApproximateSampling's new public Probability.Product import is needed for PMF.pi in its statements. The removed and renamed names are listed in the body.
• Manuals. Rendered: inspected pp. 436, 442–443 and 456 of cslib-frontier-operators-manual.pdf from run 43397000789. OK, no overflow. The Agent Operator's Manual needs no edit, because it describes no crypto APIs. Registry theorem names and ROADMAP.md are unaffected.
• Merge. Clean with main e4f3912, with refactor(Crypto/LWE): Regev single-challenge game as a typed lrExperiment; drop Regev/DualRegev projection chains (readability L4a) #5099, and in order onto the current queue.

I'll queue it on green ci-checks/guide once I've checked the notices.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) of head 1dec3c39d15a39bb6286a55fbcd4c76df084c8ce: APPROVE.

This is agent review, not human review.

What I checked

• Typed Module-LWE experiments, ring-LWE bridge & word-level equivalence (LWE/Module.lean, SIS/Module.lean, SIS/Module/ApproximateSampling.lean, SIS/ModuleEncryption.lean, CslibFrontierTests/Crypto/DecisionModuleLWE.lean):
  • LWE/Module.lean extracts sample, flattenPolyVec_sample, encodeSample, sampleLaw, realEnsemble, and uniformEnsemble cleanly from SIS/Module.lean (leaving SIS/Module.lean dedicated to Module-SIS) and introduces ModuleLWE.realExperiment, randomExperiment, realGame, randomGame, and advantage, matching the architecture of LWE/Basic.lean.
  • ModuleLWE.advantage_eq_lweAdvantage cleanly identifies ModuleLWE.advantage with LWE.advantage over Negacyclic (ZMod q) n via Negacyclic.coeffsEquiv.
  • DecisionModuleLWE is now Game.Indistinguishable over typed ModuleLWE.Distinguishers (ModuleLWE.Input, encInput, Distinguisher.IsPPT), with encInput_apply preserving the exact framed (1^κ, encodeSample (A, b)) layout (rfl) and decisionModuleLWE_iff_encoded / DecisionModuleLWE.encoded proving equivalence with the word-level ensemble definition.
  • Regression client CslibFrontierTests/Crypto/DecisionModuleLWE.lean exercises a concrete ℤ_5[X]/(X^2+1) evaluation, rfl input layout, zero-advantage sanity check, advantage_eq_lweAdvantage, and both directions of decisionModuleLWE_iff_encoded.
• Client consolidation (SIS/MLKEM/Security.lean, MLDSA/KeyOnly.lean):
  • MLKEM: deletes bespoke mlweRealGame, mlweIdealGame, and mlweAdvantage, curries mlweKeyReduction and mlweReduction, and states advantage_indCpa_uniform_le and indCpaAdvantage_le directly in terms of ModuleLWE.advantage for the centered-binomial secret/error laws.
  • MLDSA: deletes bespoke keyDistinguishGame and koaGame_eq_keyDistinguishGame, curries forgeryDistinguisher, proves koaGame_keyLaw and koaGame_uniformKeyLaw, and states succProbability_koaGame_le via ModuleLWE.advantage. Both modules and the manual explicitly state that uniform-secret DecisionModuleLWE does not bound short-secret ModuleLWE.advantage.
  • Verified zero remaining references to the removed names across CslibFrontier/, CslibFrontierTests/, CslibFrontierResults/, and manual/, and CslibFrontier.lean adds LWE.Module in sorted order.
• Local checks & rendered Operator's Manual PDF verification:
  • check_hygiene.py --check-simp, check_projection_chains.py --base e4f39124c, check_changed_files.py --source-only --base e4f39124c, and check_operator_manual.py all pass (0 errors).
  • Visually inspected rendered cslib-frontier-operators-manual.pdf (Operator's Manual PDFs run 43397000789) PDF pp. 436, 442, 443, and 456 (printed pp. 428, 434, 435, and 448) by eye: the lattice table row, ML-DSA paragraph, LWE/Module-LWE paragraph, and ML-KEM paragraph all render cleanly with no overfull boxes or broken links.