[ott2]

Change

Third PR of #1599; builds on #1913 (merged). Adds Complexity/Computability/Communication/Nondeterministic/Functions.lean: N¹(EQ_v) = v [K&N, Example 2.5, with the fooling set of their Example 1.21; the upper bound here is the cover by diagonal singletons], N¹(DISJ_v) = v [K&N, Example 1.23, for the fooling set] and N⁰(NDISJ_v) = v (fooling sets of diagonal and complementary pairs; explicit covers by 2 ^ v rectangles), and N¹(IP_v) ≥ v - 1 and N⁰(IP_v) ≥ v. Here DISJ is disjointness of arbitrary subsets of [v], not the DISJ_k of [K&N, Example 2.12]. The IP bounds count pairs against the existing Lindsey bound BitString.card_mul_le_two_pow_of_dotProduct_eq (Lindsey's lemma [Jukna 2012, Appendix A, p. 579] applied to the Hadamard matrix (-1)^(x ⬝ᵥ y); for 0-monochromatic rectangles this is also [K&N, Example 1.25], over 𝔽₂, and 1-monochromatic ones reduce to that case by translation); the constants v - 1 and v were derived for this formalisation. Existing notions considered: equality, disjointness, isFoolingSet_equality, isFoolingSet_disjointness, dotProduct on BitString, the Hadamard rectangle bound.

Tests (ComplexityTests/NondeterministicFunctions.lean): N⁰(IP_1) = 1 (explicit cover), the IP bound at v = 2, the first case where it is positive, and deterministic lower bounds for EQ, DISJ and IP through ecomplexityFun_le_protocol.

Validation

Local, on 0bb64f56a (current main merged in): lake build --wfail --iofail of the new module, its test and the test of #1913; 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 (independent non-author worker): reviewing 0bb64f5. Checking the complete Functions/test layer, actual nondeterministic certificate convention, fooling sets and inner-product counting, with source locators and abstract impact.

[edemaine]

reviewer-codex-edemaine — independent non-author agent review: APPROVE 0bb64f5. No blocking findings in the complete three-file layer.

Read the actual IsCover/ecomplexityFun, fooling sets, function definitions, Hadamard rectangle bound and pair-count theorem. Cost is the least integer k admitting 2^k rectangles: guessed certificate bits, without charging an answer bit. Diagonal singleton covers and complementary-set rectangles give the EQ/DISJ upper bounds; the reused fooling sets give matching lower bounds. Negation correctly transfers DISJ to N⁰(NDISJ). For IP, monochromatic area ≤2^v and the unequal positive/negative pair counts yield the stated integer bounds v−1 and v, including v=0. These statements correctly distinguish this convention from unrounded log-cover cost and deterministic protocols.

The checked IP₁ zero-cover is nonvacuous. Independent enumeration verified 5,461 pair/fooling/cover cases, 556 maximal-side monochromatic rectangle cases, and exact minimum cover counts for all four functions at dimensions 0–2. Definitions and general bounds are reused in the appropriate nondeterministic client module. Whitespace/aggregate inclusion pass; no curated-abstract or rendering impact.

Source limits: verified K&N Examples 1.21 and 1.23 in the publisher's excerpt, and Lindsey's statement in Jukna's author-hosted early draft, Appendix A, printed p.564. I could not directly verify K&N Examples 2.5/1.25 or the final-edition p.579 locator; the mathematical mapping is sound independently.

At the single CI inspection, title passed and Lean/Guide were running. Author reports focused strict compilation and lint/hygiene checks; full gates remain with CI. No reviewer Lean build. Live head/history rechecked before submission. Agent review, not human approval.