perf(FormalLearningTheory): simplify growth and minimax proofs

[Vilin97]

FormalLearningTheory's logarithmic, growth-function, finite-support and minimax bounds repeatedly send large proof contexts to broad arithmetic and simplification tactics. This replaces those searches with explicit order and set arguments, preserving the existing mathematical API. The median clean project build falls from 123.423 s to 100.239 s (18.78% faster) across three eligible pairs.

The proof changes are confined to four files:

• Rademacher: restrict arithmetic to its supporting facts, scale square-root inequalities directly, and use Boolean equivalence when identifying restrictions.
• Symmetrization: compose product inequalities using monotonicity and explicit power identities, including the sample-size lower bound.
• FiniteSupportUC: use direct complement-measure, union-membership and witness arguments instead of simplifying the entire context.
• ApproxMinimax: derive the logarithmic potential inequality without a redundant sign split, then combine explicit scaled bounds.

The measured head is f915b2acaaae30d0717013d28f556b30ba334d0f. The exact base is 2fc3a737eb236f260197b4ef2e296d5f076ca728, re-fetched and verified against current main before commit. Lean remains 4.35.0-rc3; the pinned Mathlib checkout is c55e6e786f49471c72fbddbec5415808896aec1e. No existing statement, definition, instance, notation, import, attribute or public name was edited. No gates or configuration changed.

Before editing, a Lean environment exporter imported every project module with importAll := true and loadExts := false, then enumerated module-owned constants, including private and generated declarations. The manifest records exact expression graphs for elaborated types and definition values, universe parameters, kinds, safety flags, inductive/constructor/recursor information and ownership. All 2,611 pre-existing module/declaration records (2,604 distinct names) are preserved. Existing definition values match exactly after removing expression metadata. The only raw type differences are hygienic bound-variable counters in analytical_log_sqrt_bound._proof_1_8 and growth_exp_le_delta_large_v._proof_1_2; their types are alpha-equivalent. The separate canonical export erases binder macro scopes and confirms every existing record is identical. Lean generated one additional private theorem auxiliary, finite_support_vc_approx._simp_1_5. There are no missing or renamed declarations and no changed semantic types or values.

Each timed run deletes only this project's artifacts under .lake/build/lib/lean/LeanPool/FormalLearningTheory* and .lake/build/ir/LeanPool/FormalLearningTheory*, retaining the same pinned dependency artifacts, then runs /usr/bin/time -v lake --wfail build LeanPool.FormalLearningTheory.Imports. Wall time is measured around that command with Python's monotonic clock. Every run compiled all 57 project modules. Source snapshots alternate in balanced order; the source was frozen throughout the included samples.

Pair	Base wall (s)	Optimized wall (s)	Reduction
2	123.423	106.450	13.75%
3	123.984	100.239	19.15%
4	100.690	83.352	17.22%

Median maximum process RSS: 1,780,232 KiB → 1,761,932 KiB. RSS is the maximum reported process size, not aggregate concurrent-build memory; no 10% RAM reduction is claimed. The VM is shared, so the timings show observed improvements under this workload and do not predict a specific CI runner. An initial pair overlapped a supplementary local validation job and was excluded as a pair before being used; the table contains its replacement.

Validation passed:

lake --wfail build LeanPool.FormalLearningTheory.Imports
lake exe runLinter --no-build LeanPool.FormalLearningTheory.Imports
lake exe lint-style LeanPool.FormalLearningTheory.Imports
lake exe mk_all --module --check
(cd python && python3 -m lean_pool.quality --repo .. --static-only)

The repository quality checker's selected-project card/declaration checks, axiom allowlist audit and whole-project option/backdoor environment audit also passed through a scoped scratch driver. A final manifest comparison and frozen-source hash check were run after the timing rebuilds. lake shake --force --keep-public inspected the import closure; the proof-only patch leaves imports unchanged. Full protected CI and independent review remain required. Auto-merge is not enabled.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No blocking issue was found in the reviewed proof changes.

Summary

Replaces broad proof searches with explicit inequalities, set arguments, and Boolean cases across four existing modules.

• Finite-support bounds use explicit measure and witness steps.
• Rademacher bounds use direct restriction and inequality steps.
• Growth bounds combine their factors with direct inequalities.
• The minimax potential bound uses direct logarithm inequalities.

_{Reviews (1) · Last reviewed commit: "perf(FormalLearningTheory): simplify gro..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "At f915b2a, the FormalLearningTheory refactor replaces broad arithmetic and simplification calls with explicit monotonicity, complement-measure and witness arguments. The minimax logarithmic-potential step removes an unnecessary split on the sign of v by scaling the log bound directly; the growth-function steps expose the nonnegative factors used by each inequality. Existing statements and imports are unchanged in the complete four-file diff. The author's reported 18.78% median wall-time reduction is advisory; I did not rerun benchmarks or independently reproduce the compiled declaration manifest.",
"assessment": {
"scope": "arithmetic and finite-support proof refactor",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The explicit inequality chains and smaller proof contexts improve maintainability without weakening the existing arguments."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: f915b2acaaae30d0717013d28f556b30ba334d0f

Verdict: ✅ approve

The four-file tactic rewrite replaces broad simplification and arithmetic searches with explicit set arguments, Boolean equivalence, monotonicity lemmas, and restricted arithmetic facts. It retains intermediate bounds and reusable helpers while removing the redundant minimax sign split, making proof dependencies easier to follow and debug. Local elaboration was blocked by missing imported-module artifacts; the reported timing improvement was not independently verified.

Aspect	Value
Scope	tactic rewrite
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The rewrites preserve useful proof structure and reduce dependence on ambient hypotheses and simp sets, with no actionable maintenance regression found.

---

Tokens: 1,272,574 in / 5,581 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $5.1740 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.