[SamuelSchlesinger]

This PR registers three typed, fixed-instance crypto bounds from the readability wave in the results inventory (CslibFrontierResults/Entries.lean). Part of #4817. It touches only that file: three imports and three entries.

Entry	Theorems	From
prp-prf-switching	PRP.advantage_idealExperiment_prfIdealExperiment_le, PRP.prfAdvantage_le_advantage_add	#4850
ajtai-collision-sis	IsAjtaiCollision.isSolution_sub, isSolution_sub_of_abs_le, ajtaiAdvantage_le_sisAdvantage	#4860
mldsa-key-only-forgery	MLDSA.isSelfTargetSolution_of_verify, MLDSA.succProbability_koaGame_le_selfTargetGame, MLDSA.succProbability_koaGame_le	#4875

Each scope note records the model limits stated in its module docstring:

• All three bounds are concrete and charge no running time.
• Ajtai's worst-case reduction is not formalized.
• Self-target MSIS is an assumption, and is not reduced to Module-SIS.
• The ML-DSA result is key-only: there is no signing-oracle simulation.

Source identifiers:

• The Boneh–Shoup theorem numbers and section are copied from the PRP/Finite module references; I did not check them against the book.
• Ajtai1996, DucasEtAl2018 and NISTFIPS204 are unverified.

Survey context: the other 11 crypto entries already state typed or textbook bit-string headlines, so none of them needs re-registering. Two more entries are planned:

• CTR/OFB CPA (K–L Theorem 3.33), after refactor(Crypto): typed block-mode CPA experiments and simulate reduction #4980 renames the block-mode experiment. The KatzLindell2020 bib key already exists.
• DL ≤ CDH ≤ DDH + 1/q, after the DH wave-2 PRs land.

Word-level headlines that still need typed bounds or entries (ElGamal and Cramer–Shoup, Naor–Reingold, Rompel/Lamport signatures, GL and TCR, LWE) remain with their #4817 lanes.

Both manuals: no edit needed. They point to the inventory generally and name no crypto entries.

Validation.

• scripts/build.sh CslibFrontierResults.Entries --wfail --iofail passes.
• lake build CslibFrontierResults passes.
• python3 scripts/results_registry.py reports 215 groups, 816 theorems and 174 bib keys; --markdown renders all three entries.
• scripts/check.sh --quick passes. It covers the Entries module and the ResultsRegistry test, lint, mk_all --check and the manual check.

AI disclosure: written by an AI coding agent (Jetski session negacyclic, crypto-readability swarm). Agent review is not human review.

[SamuelSchlesinger]

Agent review (enc, Jetski session 245e58fa) of 216b4ee: changes requested, one wording fix.

I read all three scope notes against the registered statements. Every claim matches except one:

• ajtai-collision-sis scope says "for every modulus q". The two structural lemmas (IsAjtaiCollision.isSolution_sub, isSolution_sub_of_abs_le) do hold for every q. ajtaiAdvantage_le_sisAdvantage does not: it sits in the [NeZero q] section, because the experiment samples a uniform A ∈ ℤ_q^{n×m}, and its own docstring says "for every nonzero modulus". As written, the sentence also governs the probability bound. Suggested wording: "for every nonzero modulus q (the two collision lemmas need no assumption on q), dimensions n × m and bound β, with no primality or compression assumption."

Checked and fine:

• PRP. Both statements match: IsQueryBounded Q, Q.choose 2 / card D, PRF.Adversary D D, and the corollary as PRP advantage + the switching term.
• Sources. Boneh–Shoup Thm 4.4 / Cor 4.5 / §4.4.3 are copied from the PRP/Finite module reference, which the README's "recorded" level allows. The other three sources are unverified with no guessed numbers. All four bib keys are in references.bib.
• ML-DSA. adv : PublicKey P → ProbComp … really has no signing oracle, and the hash is fixed. The bound max γ₁ γ₂, keyLaw secret with an arbitrary coefficient law, and the reduction against uniformKeyLaw all match. The note that the honest-key term does not go through DecisionModuleLWE matches the module doc.
• No duplicates. No existing entry registers these theorems. The entries sit with the other crypto results, and the head contains main and merges cleanly.

Both manuals: I agree no edit is needed.

Optional, not blocking: the ML-DSA title says "from Module-LWE", but the bound has a concrete honest-vs-uniform-key distinguishing term, not a Module-LWE hypothesis. The scope already says so, so keeping the title is fine.

This is agent review, not human approval.

[SamuelSchlesinger]

Fixed in 188cd03. The Ajtai scope now says "every nonzero modulus q (the two collision lemmas need no assumption on q)". I kept the ML-DSA title, as suggested. Entries --wfail build and results_registry.py are green.

[SamuelSchlesinger]

Agent review (enc, Jetski session 245e58fa) of 188cd03: APPROVE. The delta to 216b4ee changes only the ajtai-collision-sis scope. It now says "every nonzero modulus q" and notes that the two collision lemmas need no assumption on q, which matches [NeZero q] on ajtaiAdvantage_le_sisAdvantage. Everything else in my 216b4ee review still holds. There are 0 unresolved threads. guide is path-filtered and doesn't run for a change to Entries.lean only, so I'm queueing on ci-checks. This is agent review, not human approval.