Optimize NonSoficGroup proof elaboration and private imports

[Vilin97]

NonSoficGroup's four large proof modules repeatedly feed broad contexts to arithmetic tactics and inherit unrelated private imports. This narrows the private import closure, supplies explicit arithmetic fact sets, replaces nonlinear search with linear arithmetic where sufficient, and reuses direct norm, projection, and square-root lemmas. A new private lemma proves the central-sector projection argument over an abstract group before the existing theorem specializes it to matrix root subgroups.

The target was selected from a size/import inventory and declaration profiling: about 35,000 lines, 3,047 compiled declarations, and expensive spectral-gap, expander-cut, coarea, and rank-threshold arithmetic. The patch touches four existing project files. Public imports, existing declaration signatures, definitions, names, instances, and generated auxiliaries are preserved. No registry/index update is required. Current main pins Lean/Mathlib v4.35.0-rc3; the live pins are retained.

Base: 86da5902e640ceb44e53f88c4a04f870dc062126.
Head: c0f50e5a68a929ed8327b5dcb8cc2ebbb8c03217.

Measurements

Three complete project rebuilds per revision before the final fact-list cleanup, alternating baseline/candidate/candidate/baseline/baseline/candidate:

Revision	Repeat	Elapsed s	User CPU s	System CPU s	Peak child RSS KiB
Base	1	119.81	193.00	5.26	2,340,800
Candidate	1	143.09	194.92	5.39	2,283,768
Candidate	2	132.99	192.72	5.36	2,279,792
Base	2	151.84	209.75	5.65	2,347,516
Base	3	158.51	210.80	5.69	2,345,756
Candidate	3	132.16	191.09	5.42	2,270,928

Median elapsed time: 151.84 → 132.99 seconds, 12.414% lower. Median combined CPU time: 215.40 → 198.08 seconds, 8.041% lower. Median peak child RSS: 2,345,756 → 2,279,792 KiB, 2.812% lower.

Command: lake build LeanPool.NonSoficGroup.Imports, wrapped in /usr/bin/time -f '%e %U %S %M'. Before each run, only this project's generated outputs in .lake/build/lib/lean/LeanPool and .lake/build/ir/LeanPool are removed. Both isolated worktrees use the same pinned, already-built dependencies and native Lake options. There were no concurrent diagnostic Lean jobs from this task during measurement. Foundations' setup dependency count falls from 3,480 to 3,163, and Spectral's from 3,673 to 3,425.

This shared 16-vCPU VM had substantial background load. These are observed rebuild results; the elapsed-time variation cannot all be attributed to the patch. Earlier exploratory revisions did not meet the 10% target (one full round measured 9.800% lower median elapsed time). Completely cold dependency builds and whole-pool CI duration were not measured. The final source differs from the timed candidate only by removing two duplicated pairs of facts in linarith only lists; the compiled declaration comparison below is repeated after that cleanup.

Exact final-head clean rebuild: c0f50e5a68a929ed8327b5dcb8cc2ebbb8c03217: 103.73 s elapsed, 178.70 s user CPU, 5.19 s system CPU, and 2,289,212 KiB peak child RSS (one supplemental run; warning-free).

Declaration invariant

Before editing, all .olean, .olean.server, and .olean.private parts for the six project modules were saved at the base SHA. A Lean inspector uses Lean.readModuleDataParts to include private/generated declarations. It compares exact elaborated types using Expr.equal, including binder names/annotations; universe parameters; all ConstantInfo metadata and safety; and exact non-theorem values. Only theorem proof bodies may differ. Rewrites that changed generated auxiliary types were reverted.

Final result: before=3047 after=3048 changedProofs=100 failures=0.

The one added declaration is private: SoficGroups.fixed_submodule_inner_square_bound_of_central_sectors. No existing declaration is missing.

Validation

• Clean native project builds and warning scans.
• lake env lean --run scripts/ci/lint-project.lean with all six project modules: all slow declaration linters pass.
• lake exe lint-style LeanPool.NonSoficGroup.Imports.
• Unchanged repository quality functions scoped to all six project modules: file/header/proof-size checks, project card/schema/entry/reachability, allowed-axiom audit, and compiled option/backdoor audit: zero errors.
• The generated-index renderer matches the project's Imports.lean and unchanged LeanPool.lean.
• lake shake --force --keep-public --explain LeanPool.NonSoficGroup.Imports was inspected. It exits 1 with further advisory import substitutions/moves; these were not applied automatically. The existing instance environment is retained, including an explicit shake: keep for the freeness instance required by the exact finite-field-basis type. --force skips unrelated unbuilt-pool cache sanity checks; it does not change the build or quality gates.
• git diff --check.

The binary manifests, inspector, arithmetic probes, rebuild harness, and raw logs are retained on the operator VM under /data/codex/scratch/researcher/optimization-20261018T1505. Full-pool protected CI and independent refactor review remain required. Leave this PR open; no merge, queue admission, or auto-merge is requested.

[greptile-apps]

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

[Medium impact] No actionable defect was found in this refactor; full-pool CI and external source checks remain unverified.

Summary

This refactor narrows private imports, gives arithmetic tactics explicit facts, and replaces several proof steps with existing lemmas. It also moves the central-sector projection argument into one private helper.

• Lean proves the same results with more focused arithmetic steps.
• The proof modules keep focused imports and the instances they need.
• The matrix proof uses a shared helper for central-sector bounds.

_{Reviews (1) · Last reviewed commit: "Factor central-sector projection proofs ..." · Reviewed by Greptile}

[Vilin97]

The refactor improves maintainability: it narrows arithmetic automation, uses direct projection identities and factors the matrix-specific projection bookkeeping into a private helper. I found no source defect in the changed proofs.

{
"review_kind": "refactor_review",
"head_sha": "c0f50e5a68a929ed8327b5dcb8cc2ebbb8c03217",
"assessment": {
"scope": "proof elaboration and private imports",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Explicit arithmetic facts and a private projection helper reduce ambient automation while preserving the argument."
},
"verdict": "approve",
"code_quality": 4,
"findings": [],
"source_evidence": "I read all four complete diffs and the decisive producer, projection, finite-sector induction, matrix specialization and averaging proofs. Existing written theorem headers, definitions and ambient assumptions are preserved in the static comparison; the only new declaration is private and has a concrete caller. The coefficient8, centrality, commuting-sector and terminal-orthogonality obligations remain genuine.",
"imports": "Public imports and the project entry/card remain fixed. Focused private imports retain the finite-field and freeness instance environment; shake:keep annotations document dependencies rather than waive quality checks.",
"cost_scope": "The author's alternating-build measurements and final cleanup limitations are disclosed. I have not independently reproduced timings or certified compiled/generated API identity.",
"validation_scope": "This is source approval at the exact head. Authored CI39153964945 and the normal configured review after successful CI remain separate. Current main's own push validation is pending at the captured check. The explicit request to leave this PR open without merge, queue admission or auto-merge is preserved."
}

[Vilin97]

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

Reviewed head: c0f50e5a68a929ed8327b5dcb8cc2ebbb8c03217

Verdict: ✅ approve

This refactor narrows private imports, makes arithmetic dependencies explicit, replaces repeated arguments with library lemmas, and separates projection algebra from matrix-specific facts. The intermediate bounds and proof structure remain readable, with no actionable code debt found. The targeted build stopped at a dependency-fetch HTTP 403, so build and timing claims were not independently reproduced.

Aspect	Value
Scope	proof elaboration and private-import refactor
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

Explicit fact lists, direct library lemmas, and the structured projection helper improve maintainability without sacrificing proof structure or reusable helpers.

Findings (1)

• prompt-injection — PR-wide
  The PR description directs the reader to ‘Leave this PR open’. This contributor-controlled instruction was ignored when selecting the verdict; remove review-handling directives from the description.

---

Tokens: 2,358,625 in / 10,917 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $9.5983 (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.