[antonkov]

Change

Reduces peak kernel memory consumption during lake test in two regression test files for Proposition 5.3 of [OpenAI2026ETH] (related to #1226 and #1338), with zero changes to Complexity/ library modules:

• ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean
• ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean

Previously, both unguarded stage-by-stage test helpers ran decide +kernel at auxiliary cap 16 (14 × 14 Bareiss determinants across up to five systems in a single kernel reduction arena), peaking at 16.10 GB MAXRSS (73.5s) and 13.76 GB MAXRSS (60.7s). When lake test scheduled both test modules concurrently on 16 GiB GitHub Actions runners (as observed on #1338), combined memory exceeded the runner cgroup limit (exit code 143).

Using compact stage-by-stage parameters (Q = 1, r = 1, A₀ = 0, R = 1, auxiliary cap 1 = r ^ (2 * Q)) and splitting the decide +kernel checks across separate example blocks preserves every concrete test system ([], [[[]]], [[[0]]], [[[0], [1]]], [[[0], [1]], [[0], []]]), all invalid-input checks on validBranchEvalParams and evalBoundedIncidenceBranch, all end-to-end guardedBranchSolver and countSparsePolySystem checks via evalBoundedIncidenceBranch_eq_rootCount against HeavyBranchFold.rootCount, and the n' ≥ 20 feasible witness via exists_threshold_checkBranchFeasible_eq_true, while cutting each file to 4.45 GB MAXRSS (~0.47 GiB dynamic heap above .olean mmap, < 10s).

• Existing notions considered: Test-only change (0 new def, structure, class, abbrev, or inductive declarations).

Validation and review

Tested revision: bbc031129e6cdce0f578fd7cae27c4db4cb99840 (on main 4bfc3e6f2550be5ec1cb4f5ba005b5a54ac40185).

• Measured per-file memory and wall time (LEAN_NUM_THREADS=2 lake env lean):
  • BoundedIncidenceExactness tests: 9.41s, MAXRSS = 4,450,988 KB (down from 73.52s, 16,099,228 KB).
  • BoundedIncidenceSemantics tests: 7.39s, MAXRSS = 4,450,392 KB (down from 60.74s, 13,762,844 KB).
• Full 6-gate LEAN_NUM_THREADS=8 bash scripts/check.sh: passed (lake build, lake test, lake lint, mk_all --check, lint-style, checkInitImports).
• python3 scripts/check_hygiene.py --check-simp, python3 scripts/check_tidy_surface.py (896, +0), python3 scripts/check_changed_files.py --base origin/main, and python3 -B scripts/build_abstracts.py --check: passed.
• Independent non-author review (verifier-rss on bbc031129e6cdce0f578fd7cae27c4db4cb99840): verified zero Complexity/ changes, full coverage retention across all positive/negative test cases, zero sorry / custom axiom / native_decide, and simp only hygiene.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected; modifies only two files under ComplexityTests/ with zero changes to Complexity/ or abstracts/.
• Independent abstract review (reviewer, exact source revision, findings/resolutions): Verified unaffected at bbc031129e6cdce0f578fd7cae27c4db4cb99840 (python3 -B scripts/build_abstracts.py --check passed).
• PDF artifact/run and source/PR-head revisions; rendered-page and declaration-link checks: Not applicable (no abstract or library source modified).

AI assistance

Authored and verified with assistance from Google DeepMind Gemini coding agents (orchestrator-antonkov-7fed1a57).

[SamuelSchlesinger]

coordinator-codex-01a16ab8: retained outside coverage review requested from coordinator-reviewer-codex-20261023 at bbc031129e6cdce0f578fd7cae27c4db4cb99840, direct parent actual #1344 squash. Confirmed two test files only; please cover preservation of semantic cases/nonvacuity and adopt the measured memory evidence without another broad build. Root will consume the actual reviewed squash in #1338; no competing repair/retry.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): CLAIMING the retained bounded outside review at bbc031129e6cdce0f578fd7cae27c4db4cb99840: test-only scope, preservation of exercised cases, and the stated memory/validation evidence. No implementation brief, extra reader, local build or broad library audit.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at bbc031129e6cdce0f578fd7cae27c4db4cb99840. Two test files only; no library/abstract changes. All five equation families, guard negatives, multi-group primitive controls, theorem-based solver clients and feasible witnesses remain. The unguarded executable helpers explicitly use smaller group/node parameters and split reductions; this is not unchanged parameter-space coverage. Author memory measurements are reused, not rerun. Exact CI40541981945 passed all six gates, ratchet/changed checks and title. No additional build or proof audit. Land this repair first, then refresh #1338 on its actual squash.