[SamuelSchlesinger]

Addresses Item A.1 from #939:

• Consolidate the elementary factorial-power comparison bound Nat.pow_self_le_three_pow_mul_factorial (n ^ n ≤ 3 ^ n * n!) into Complexity.Foundations.Data.Nat.Factorial as an addition to upstream Cslib.Foundations.Data.Nat.Factorial.
• Eliminate the duplicate private copies in Complexity/Computability/Circuit/Boolean/ShallowSymmetric/Covering.lean and Complexity/Computability/MCSP/Shannon.lean.
• Remove now-unneeded Mathlib.Analysis.Complex.ExponentialBounds imports from both call sites.

Validation

• lake build --wfail --iofail (ok)
• lake exe mk_all --check (ok)
• lake test --wfail --iofail (ok)
• lake lint (ok)
• lake exe lint-style (ok)
• lake exe checkInitImports (ok)
• python3 scripts/check_hygiene.py (ok)
• python3 scripts/check_tidy_surface.py (1301 statements in 225 modules, matching baseline)
• python3 scripts/check_docs.py --config-only (consistent)

AI-assisted: Jetski (worker-jetski-b5844be2).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-02 (agent review) at bf4ab81.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at bf4ab81 (agent review, not human approval)

Nat.pow_self_le_three_pow_mul_factorial (n : ℕ) : n ^ n ≤ 3 ^ n * n.factorial has the same statement as both deleted copies (Covering.lean's k ^ k ≤ 3 ^ k * k.factorial and Shannon.lean's s ^ s ≤ 3 ^ s * s.factorial), and its proof is the Covering.lean proof verbatim, with the variable renamed. No aliases are added, and all three call sites use the new name. The removed Mathlib.Analysis.{SpecialFunctions.Exponential,Complex.ExponentialBounds} imports were plain imports used only by the deleted proofs, and the new module imports them itself. Hosted ci-checks passed on this head. The module is small, imported only by its two consumers (and Complexity.lean), mirrors cslib's Cslib/Foundations/Data/Nat/Factorial.lean with a correct upstream marker, and keeps the original authors. I found no Mathlib lemma with this statement. Stirling.le_factorial_stirling implies it but would not shorten the proof.

Restack needed (no change to this verdict's content): since #931 merged, ShallowSymmetric.pow_self_le_three_pow_mul_factorial is public on main, so Covering.lean conflicts. Resolve it by deleting the now-public copy as well. Nothing in the library, tests, abstracts, guide or docs uses that name outside Covering.lean, so no alias or other client update is needed. The PR does not touch ComplexityTests.lean (#916).

[SamuelSchlesinger]

Restacked onto latest main (51d90c3f) at 2ecc2c4:

• Deleted the now-public copy in Covering.lean to resolve the merge conflict with refactor(Circuit/Boolean): make 74 API and general declarations public again (#926) #931.
• Updated Covering.lean call sites to use Nat.pow_self_le_three_pow_mul_factorial.
• Validated mk_all --check, lint-style, and check_docs.py --config-only.

Ready for merge.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at 2ecc2c4 (agent review, not human approval)

Delta review of the restack. Per git range-diff, the only change from my reviewed bf4ab81 is the one I asked for: the deleted Covering.lean copy is now the public ShallowSymmetric.pow_self_le_three_pow_mul_factorial that #931 published, and it is removed with no alias. A repository-wide git grep finds no remaining use of the old name anywhere (library, tests, abstracts, guide or docs). The three call sites use Nat.pow_self_le_three_pow_mul_factorial. The PR now merges cleanly with main, and hosted ci-checks passed on this head. My earlier statement and import checks still hold.