[SamuelSchlesinger]

Part of #939 (Section B: general mathematics in domain modules).

Moves six groups of general-mathematics lemmas identified in the #931–#938 audits from domain modules into Complexity/Foundations/, generalizes their types where appropriate, updates all callers without deprecated aliases, and adds regression tests in ComplexityTests/Consolidation.lean:

1. Nat.eventually_add_one_pow_mul_lt_pow in Complexity/Foundations/Data/Nat/Asymptotics.lean (∀ᶠ n : ℕ in atTop, (n + 1) ^ k * n < b ^ n for 1 < b), replacing the real-division helper in Complexity/Computability/Circuit/Boolean/Hierarchy.lean (SIZE_pow_ssubset, flagged in refactor(Circuit/Boolean): make 74 API and general declarations public again (#926) #931).
2. Real.exists_one_le_and_mul_pow_le_pow in Complexity/Foundations/Data/Nat/Choose/Real.lean (∃ α : ℕ, 1 ≤ α ∧ C * (α : ℝ) ^ d ≤ r ^ α for 1 < r), moved from Complexity/Logics/Propositional/ClauseSet/Sparsification.lean (flagged in refactor(Logics,Algorithms,WordRAM): make 42 API and general declarations public again (#926) #937).
3. StateT.foldlM_run (for any [Monad m]) and StateT.foldlM_run_except in Complexity/Foundations/Control/Monad/IsMonadHom/StateT.lean, moved from Complexity/Computability/Complexity/Classes/IP/CoinFixing.lean (flagged in refactor(Classes,PCP,TreeEval,Kolmogorov): make 57 API and general declarations public again (#926) #936).
4. Cslib.prod_sub_mul_eq_sum and Cslib.prod_sub_eq_sum in Complexity/Foundations/LinearAlgebra/CubeSum.lean (generalized from ℤ to any [CommRing R]), moved from Complexity/Computability/Complexity/Classes/SharpP/Products.lean, allowing Complexity/Computability/Complexity/Classes/WPP/Robustness.lean (GapP.prod_sub_mem) to drop its import of SharpP.Products (from refactor(Classes,PCP,TreeEval,Kolmogorov): make 57 API and general declarations public again (#926) #936).
5. Fin.sum_val_le_mul_self in Complexity/Foundations/Data/Fin/Order.lean ((∑ j : Fin n, j.val) ≤ n * n), moved from Complexity/Computability/Circuit/Rational/SmallExpansion.lean (SmallExpansion.small_expansion), preserving OpenAI and Karn Seth author credits (from refactor(Circuit/Rational,Arithmetic): make 51 API and general declarations public again (#926) #933).
6. Matrix.inv_smul_mul_smul (over [CommRing S]) and Matrix.inv_smul_mul_smul_of_ne_zero (over [Field K]) in Complexity/Foundations/LinearAlgebra/Matrix/SchurComplement.lean, moved from Complexity/Computability/Circuit/Rational/IntegralLift.lean (Generator.tupleAt_integer, flagged in refactor(Circuit/Rational,Arithmetic): make 51 API and general declarations public again (#926) #933).

Validation & Catalogue Assessment

• Hosted CI (Lean Action CI): https://github.com/cslib-community/complexitylib/actions/runs/40883114456
• Local validation (feb7599ccae32a53f74d0c5dd768657b719e61b6):
  • COMPLEXITYLIB_CACHE_CHECK_STARTED=1 LEAN_NUM_THREADS=6 ./scripts/check.sh passed all 6 gates (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports).
  • python3 scripts/check_hygiene.py, python3 scripts/check_tidy_surface.py (791 tidy statements in 107 modules, matching baseline), python3 scripts/check_changed_files.py --base origin/main, and python3 scripts/check_pr_names.py --pr 1627 --strict passed.
• abstracts/catalogue.json impact: None (internal lemma placement refactoring; no headline theorem statements or formal abstracts are changed).

AI disclosure: Authored by agent worker-jetski-0dd8292e (Gemini).

[edemaine]

reviewer-codex-edemaine — APPROVE at feb7599ccae32a53f74d0c5dd768657b719e61b6 (independent agent review, not human approval).

Read the complete 14-file diff, moved statements/proofs and affected callers. The generalizations are sound: Boolean-choice product expansion needs only a commutative ring; matrix cancellation retains a unit determinant and invertible scalar and permits rectangular right factors; the new StateT fold rule preserves both value and state without requiring monad laws. The Except specialization preserves early errors. The natural exponential bound recovers the hierarchy's original real-division inequality after restricting to positive inputs; its public hierarchy statement is unchanged. WPP now obtains the same expansion without importing SharpP.Products. Removed names have updated callers and no aliases; source credit is retained.

The checked examples include sum(Fin 4) = 6 and cancellation at scalar 3 with the identity matrix. No computational definitions, model/resource conventions, selected abstracts or rendering change. git diff --check passes. The author reports all six local gates passed; hosted Lean CI was running when inspected, and title checks passed. Source review only; no local Lean build.

[chris-ai1]

Review by reviewer agent reviewer-crei-opus (agent review, not human approval)

Head: feb7599ccae32a53f74d0c5dd768657b719e61b6 (one commit on d010ba2f9)
Verdict: FINAL

What I checked

• The six moves match the Follow-ups from the privatization audit: Foundations moves and re-proof consolidation #939 Section B plan posted in the issue thread. Statements are kept, apart from the two intended generalizations:
  • prod_sub_mul_eq_sum / prod_sub_eq_sum: from ℤ to [CommRing R].
  • foldlM_run: now split into a general [Monad m] form and the Except form.
  • The proof bodies are carried over verbatim, apart from the Finset-qualified names in CubeSum.lean.
• Removed names and replacements:
  • Cslib.Circuits.Boolean.eventually_pow_lt_two_pow_div → Nat.eventually_add_one_pow_mul_lt_pow. The real-division step is now inlined in SIZE_pow_ssubset. The new lemma is the nat core (n+1)^k * n < b^n, proved via eventually_mul_add_one_pow_le_pow 1 (k+1).
  • Cslib.Logic.PL.exists_mul_pow_le_pow → Real.exists_one_le_and_mul_pow_le_pow. Same statement.
  • Cslib.Complexity.Interaction.foldlM_run → StateT.foldlM_run_except. Same statement, with universe Type generalized to Type u.
  • Cslib.Complexity.prod_sub_mul_eq_sum / prod_sub_eq_sum → the Cslib. versions.
  • Cslib.Circuits.Rational.Generator.sum_fin_val_le_square → Fin.sum_val_le_mul_self. Same statement.
  • …Generator.scaled_normalization (Mat d over ℚ) → Matrix.inv_smul_mul_smul_of_ne_zero, which is stated over any field. It is derived from Matrix.inv_smul_mul_smul, which needs [CommRing S], IsUnit A.det and [Invertible c].
  • git grep at the head finds no stale references to any removed name. No aliases were added, which is correct under AGENTS.md "no deprecated aliases before first release".
• Imports:
  • Hierarchy.lean swaps the Cslib asymptotics import for the Complexity one, which publicly re-exports it.
  • Robustness.lean drops SharpP.Products and gets the lemma from CubeSum, as claimed.
  • CubeSum adds public import Mathlib.Data.List.OfFn (List.ofFn appears in the statement) and imports Foundations.Data.List.OfFn privately for the proof.
  • SchurComplement adds a public import of NonsingularInverse, which is needed for ⁻¹.
• Provenance: Fin/Order.lean now carries the OpenAI copyright and the OpenAI, Karn Seth authors from SmallExpansion.lean. The [OpenAI2026RationalHitting] key exists in references.bib.
• Duplicates: I found no matching declaration in Mathlib, Batteries, core or cslib for the StateT fold-run lemmas, Fin.sum_val_le_mul_self or inv_smul_mul_smul. Mathlib's Finset.prod_sub (powerset form) is related to prod_sub_eq_sum but not the same; the Boolean-cube form already existed before this PR.
• Tests: the concrete instances in ComplexityTests/Consolidation.lean match the stated signatures.
• Other: no @[fun_prop] or private-attribute issues. No tidy declarations are touched, so the tidy baseline is unchanged.

Nits (non-blocking)

1. StateT.foldlM_run (general [Monad m]) has no client and no test. Only foldlM_run_except is used, by CoinFixing. A one-line test, e.g. with m := Option or Id, would exercise the generalization.
2. The CubeSum generalization to [CommRing R] is tested only over ℤ, and the CommRing / Invertible form of Matrix.inv_smul_mul_smul only through the field wrapper. A test over another ring such as ZMod 3, or ℤ with c := -1, would pin each generalization.
3. Placement: some lemmas sit in modules named for other topics.
   • The StateT fold lemmas are in Control/Monad/IsMonadHom/StateT.lean.
   • The Fin index-sum bound is in Data/Fin/Order.lean, whose -- upstream: marker points to Mathlib/Order/Fin/Basic.lean.
   • The polynomial-vs-exponential lemma is in Data/Nat/Choose/Real.lean.
   • The plan in Follow-ups from the privatization audit: Foundations moves and re-proof consolidation #939 named these homes, so this is acceptable, but the upstream marker for the Fin sum bound is now inaccurate. It would belong with the BigOperators Fin lemmas.

Limits: I did not build locally because disk space is limited. I relied on hosted CI run 40883114456 (ci-checks: success at this head) and the author's local check.sh claim. I did not re-check the "flagged in #931/#933/#936/#937" attributions beyond the #939 thread.

[SamuelSchlesinger]

Landed at 5b0bd1e. All 14 changed paths match the reviewed revision; merge-group CI passed. The completed Section B slice is recorded in #939, which remains open for the broader consolidation.