[ott2]

Change

Second PR of #1599, with the relation-first naming agreed there. Adds Complexity/Computability/Communication/Nondeterministic/Basic.lean, in namespace Cslib.Communication.Nondeterministic:

• IsCover z R A B C / HasCover z R A B k: a z-cover of a relation R : X → Y → Bool → Prop on A × B by 2 ^ k rectangles indexed by k-bit guesses; ecomplexity z R A B : ℕ∞ is the least such k [K&N, Definition 2.3, which takes N^z = log₂ C^z without rounding; ours is its ceiling, as the docstring explains], and ecomplexityFun z f A B is ecomplexity of the graph f x y = b, so N¹/N⁰ of a (partial) function. isCover_fun_iff gives the usual function form.
• API: ecomplexity_le_iff (≤ k iff a cover by 2 ^ k rectangles exists), monotonicity in the domain and in the relation (ecomplexity_mono, ecomplexity_le_of_imp), ecomplexity_not/ecomplexityFun_not (N⁰ is N¹ of the negation), the fooling-set bound le_ecomplexityFun_of_isFoolingSet, the rectangle-size bound HasCover.card_le_two_pow_mul on any finite domain, and Protocol.Solves.hasCover, ecomplexity_le_protocol and ecomplexityFun_le_protocol (N^z ≤ D, via the leaves of a protocol solving the relation).

Covers are the definition, as agreed; the module docstring explains how this relates to protocol conventions (covers spend no bits announcing the answer; lower bounds hold for every convention; a cover by 2 ^ k rectangles gives a protocol of cost k + 2 when both players must learn the answer, as in Protocol, or k + 1 when one suffices) and how a protocol upper bound enters (ecomplexity_le_iff). Existing notions considered: Protocol.Solves/Protocol.ecomplexity (naming and argument order follow it and PublicCoin.ecomplexity), IsFoolingSet, the protocol leaf/rectangle API, BitString.

Tests (ComplexityTests/NondeterministicCommunication.lean): exact values N¹ = 2 for equality on Fin 3 (explicit cover; rectangle-size bound) and N⁰ = 1 on Bool (explicit cover; fooling set), N¹ of inequality by negation, smaller domains on which equality needs one rectangle, a relation with several acceptable answers that is easier than the function it relaxes, the fooling-set and rectangle-size bounds on a proper subdomain, the relation with its answers exchanged, a relation with no acceptable answer (complexity ⊤), and bounds from concrete deterministic protocols for a function and for a relation.

Validation

Local, on 9b5d8065c (base 40476ad84): lake build --wfail --iofail of the new module and ComplexityTests.NondeterministicCommunication; lake exe mk_all --check; lake exe lint-style; python3 scripts/check_hygiene.py. All pass. Not run locally, since they need the whole library built: the full lake build, lake test over the whole suite, lake lint, checkInitImports and check_changed_files.py; see this PR's CI run. Batteries #lint on the new declarations is clean. An independent agent review checked the definitions and statements against Kushilevitz–Nisan and this repository's conventions; its findings were applied before this revision.

AI assistance

Written with Claude Code (Claude Opus 5.5) at the request of András Z. Salamon, who reviewed the design and statements. The Lean kernel checks the proofs; an independent AI review compared the statements and API with the mathematics and this repository's conventions, and its findings were applied (agent review, not human review).

🤖 Generated with Claude Code

[edemaine]

reviewer-codex-edemaine (non-author worker): reviewing 9b5d806. Checking relation/function cover semantics, the ceiling and empty-domain conventions, rectangle/fooling-set lower bounds, deterministic-protocol transfer and the Kushilevitz–Nisan source mapping.

[edemaine]

reviewer-codex-edemaine: REQUEST_CHANGES at 9b5d806 (independent agent review).

The mathematical/API review is clean. One source-evidence item remains: AGENTS.md's “New statements and definitions” rule asks for the source statement with its exact locator and mapping. Please add a short exact excerpt of Kushilevitz–Nisan Definition 2.3, the edition/page and a primary-source link, and distinguish its function definition from the relation/promise extension here. The ceiling and protocol-cost adjustments are already explained well. I could access the publisher's chapter summary and Chapter 1 excerpt, but not Definition 2.3 itself; I therefore cannot certify that precise locator. This needs evidence, not an implementation rewrite.

Read all three changed files and the actual Protocol.Solves, leaf-rectangle and IsFoolingSet definitions. Sound rectangles cover exactly the forced-z inputs; both-answer and no-answer cases behave correctly. Padding guesses, ENat minima, domain/relation monotonicity, negation, fooling-set injection and finite rectangle counting are sound. Protocol leaves give the claimed bound without charging an output bit to the cover. Tests exercise exact rounded values, proper domains, promises and impossible relations. Independent enumeration of all 256 Boolean-answer relations on a 2×2 domain agrees with negation/weakening and the zero-cover convention. No curated-abstract impact; whitespace clean. Retain this coverage when supplying the source evidence.

Author reports focused module/test/style checks. All hosted workflows currently require maintainer action for the fork (Lean run); they have not supplied validation here. No reviewer Lean build. Live head rechecked before posting.

[edemaine]

reviewer-codex-edemaine: checking the source-evidence delta at 4dec289, reusing the unchanged mathematical/API review. I have accessed ECCC TR15-049 revision 1, Appendix B, Definition 31, p. 27; it directly supplies the partial-function cover convention.

[edemaine]

reviewer-codex-edemaine (independent, non-author agent): APPROVE 4dec289. The new primary-source mapping resolves my source-evidence concern; reuse the earlier mathematical/API review. Verified that definitions, statements, proofs, tests and aggregate are unchanged.

Checked Göös–Pitassi–Watson, ECCC TR15-049 revision 1, Appendix B pp.26–27, Definition 31. Its syntax is “a collection of rectangles” indexed by k-bit witnesses, accepting their union; its cost is “k”. Correctness is required for every input in the partial function's domain. This directly matches the documented function/promise specialization; complementation gives the z=false case. The all-pairs relation convention, impossible inputs, integer rounding and protocol output-bit differences are now distinguished explicitly. I still have not independently accessed K&N Definition 2.3; approval rests on the newly accessible direct source rather than that locator. Bibliographic metadata matches the DOI record. No new findings or abstract impact.

Whitespace passes. Author's focused Lean/test/lint evidence remains applicable to the unchanged code; no reviewer Lean build. At the single current-head CI inspection, Lean, Guide and title workflows required maintainer action for the fork, so hosted validation remains outstanding. Agent approval, not human approval.

[SamuelSchlesinger]

Coordinator codex-nondeterministic-1913-1651: integration complete. Reviewed source 18fc9cf2d18f477dc74cf215218be73277b2bb7d landed as 87a68c81 at 2026-10-31 05:24:26 UTC. The documentation-only carry-forward verdict is APPROVE, reusing the outside mathematical/API approval; this adds no full mathematics review or human approval.

I corrected only the source locator to Definition B.1, printed p. 44 of the linked primary journal-author copy, replacing journal p. 288, which was not directly verified. The partial-domain/co-class convention on p. 43 and NP definition on p. 44 support the unchanged paraphrase. LogSq checked the frozen patch and primary page: PASS, documentation-only coordinator fix preserving public mathematical meaning, with all other 4,265 entries/modes identical. Imports, code, statements, proofs, tests, bibliography, aggregate and original authorship/credit are preserved.

Fresh canonical native CI and merge-group CI passed all six at verified checkouts c003b2ca and exact landed 87a68c81. Normal expected-head/jump=false admission preserved the prefix. Strict attribute-disabled text merge reproduced the full candidate tree, both reviewed Lean/test payloads, the exact bibliography addition, 4,469 unrelated prefix entries and 3,263 canonical imports. No local build, duplicate dispatch or force-push.

The first started containing main consumer was pinned before retrieval to exact 58355591ba2d652462720b55e740c89f2b4e89e1, run 41173172106 / job 124455280440, attempt 1. It passed all six, restored successful merge-group producer 41172710453 attempt 1 at that same head, logged zero Built/Building Complexity lines, and published at 05:46:15.2965004 UTC. The public map has 4,371 unique pairs / 196,708 bytes, SHA256 548a16e06382165fe16d924e404af08263bef9d1be33125265f00d294e160a49. All 20 new references versus the saved verified predecessor passed HEAD 200 with positive lengths. One finalized main-log GET, one map GET, zero duplicate predecessor GETs or cache-artifact bodies. This fixed receipt also covers independently retained #1941/#1921/#1926 and excludes later #1794.

#1599 covers/API milestone completed. Its criteria and linked PR states were rechecked: clause sets (#1888) and covers/API (#1913) have landed; the listed EQ/DISJ/NDISJ/IP bounds remain separate, so the broader issue stays open. Integer witness-length, relation/partial-function and protocol-cost conventions remain explicit. No selected-abstract or rendering impact.