perf(FiveEighthsTheorem): reduce counting-proof elaboration

[Vilin97]

FiveEighthsTheorem's finite-group counting proof repeatedly searches for nonempty instances and normalizes denominators that are already known to be nonzero. This revises five proof bodies, preserving the counting argument, all declarations, and the exported API. The main proof's measured elaboration work falls 48.35%; the observed median project-clean build falls 5.30%.

• Supply identity witnesses for the group and its center, and reuse one proof that the group cardinality is nonzero in three remaining field_simp calls.
• Replace three other field_simp calls with ring or the explicit mul_div_assoc / sub_div / div_self calculation; bound congruence descent and restrict the final linear arithmetic to the needed quarter-bound.
• Use the centralizer/center characterization directly instead of simp_all. Identify the centralizer predicate explicitly and replace grind with equality symmetry. as_aux_lemma preserves the existing compiler-generated proof helper.
• Use div_le_div_iff_of_pos_left for both reciprocal bounds, avoiding intermediate cross-products.

Base: af9bc17bdcf163f5c1b223e3b4551eb0efc22a42. Head: 14c832c664d1f143ea1c43d93bf37e110e54d53c. origin/main was fetched and verified immediately before the initial commit and again immediately before rebasing this same PR onto the current base. The pre-edit manifest and timings use 854da85a8bc6c9219c2c04ec9d43d4a49f43aef8; the only subsequent base changes are the unrelated Python registry-parser fix and its tests in #532. The selected project and Lean build inputs are byte-identical between these bases, and the manifest was also verified on the rebased base. Lean 4.34.0, Mathlib v4.34.0 (5ed2965256430c3649e86755f9576b54eca72435), and repository options are unchanged.

Selection and recovery. Reviewed previous optimization job logs, repository worktrees, remote PRs and comments, and announcement reports. The completed ABCExceptions / Zeta3Irrational cycles and existing Erdos367 PR were preserved. Work was performed in a fresh isolated worktree. Candidate builds/source inspection covered GoemansFlow (715 lines), PolyaEnumerationTheorem (935), and FiveEighthsTheorem (246). FiveEighthsTheorem had the largest individual theorem-body cost among the inspected profiles: about 17.69 million raw profiler heartbeats, versus 3.30 million in GoemansFlow and 7.18 million in Polya's Basic module. This is an evidence-based local selection, not a pool-wide ranking.

Invariant audit. A pre-edit Lean environment manifest recorded every project declaration, including private/generated declarations. It records the name, owning module, elaborated type, universe parameters, declaration kind, safety/partial flags, exported visibility, reducibility/inductive metadata, and all non-theorem values. Only theorem proof bodies are excluded.

Result: 45 → 45 declarations (30 theorems, 15 definitions); no additions, removals, or kernel-expression changes. The raw comparison identified five records with differences: compiler-generated bound-variable labels in three auxiliary theorem types, and source-position expression metadata in ncard_setOf_pair_eq_sum and its generated matcher (including the matcher's value). These were inspected individually. Removing only Expr.mdata and alpha-renaming bound-variable labels makes the manifests byte-identical, SHA-256 5235af878f0c3c6a34c2c3c31d3daaade56607e08c03afe24a67db052f8da75c. No constant names, universe parameters, binder kinds, free variables, or expression structure are normalized; no rewriting or definitional simplification is used. In particular, every non-theorem value matches under precisely this normalization. The separate repository textual statement comparison also reports zero statement changes, binder renames, additions, or removals across all 16 source declarations.

The module header, imports, notation, namespace structure, definitions, and statements are untouched. Some more aggressive proof rewrites were rejected because they removed generated helper declarations. No gates, waivers, or options were changed.

Controlled build measurements. Five builds per revision in separate base/head worktrees on the same Azure VM. Each trial deletes only .lake/build/lib/lean/LeanPool/FiveEighthsTheorem* and .lake/build/ir/LeanPool/FiveEighthsTheorem*, then runs lake build LeanPool.FiveEighthsTheorem. Mathlib dependencies stay cached; default Lake parallelism and repository settings are used. Python time.monotonic measures end-to-end wall time. Order alternates base/head and head/base. All ten builds succeed without warnings.

Revision	Trial 1 (s)	Trial 2 (s)	Trial 3 (s)	Trial 4 (s)	Trial 5 (s)	Median (s)
Base	3.499812	3.756657	3.168947	3.268211	3.061138	3.268211
Head	3.418241	3.413499	2.888252	3.095052	2.837971	3.095052

An initial three-build baseline was 3.035888, 3.145841, and 3.169827 seconds. The final alternating comparison above is the reported before/after result. Wall times are observations on a shared VM with warm dependencies, not cold-cache or CI guarantees.

Declaration-body measurements use lake env lean -DElab.async=false -Dtrace.profiler=true -Dtrace.profiler.useHeartbeats=true -Dtrace.profiler.threshold=100000 -DrelaxedAutoImplicit=false -DmaxSynthPendingDepth=3 LeanPool/FiveEighthsTheorem/Basic.lean in each worktree. These are raw profiler heartbeats, not divided maxHeartbeats units.

Proof body	Base	Head
card_div_card_eq_one_div_index	578,511	324,588
centralFraction_le_quarter	601,304	638,665
two_le_centralizer_index	286,682	238,232
centralizerFraction_le_half	545,563	582,900
commProb_le_five_eighths_of_finite	17,690,471	9,136,354

The two reciprocal-bound wrappers are slightly costlier in these profiles; their direct inequality application is a clarity change. The main counting proof accounts for the material reduction.

Validation completed:

• lake build LeanPool.FiveEighthsTheorem; warning scans of all final benchmark builds.
• lake exe runLinter LeanPool.FiveEighthsTheorem (including slow linters), lake exe lint-style LeanPool.FiveEighthsTheorem.
• lake exe mk_all --module --check: no generated-index changes required.
• python3 -m lean_pool.quality --repo <project-scope>: passed. The scope contains byte-identical copies of both project files, the unchanged project registry entry and repository configuration, a project-only generated root, and the same compiled project artifacts. This runs the existing source, size, card/declaration, axiom, and environment-backdoor checks without modifying the checker or any gate.
• Private-environment axiom audit: all 45 declarations pass. Independent dependency-closure audit: 10,742 constants visited, only Classical.choice, propext, and Quot.sound found.
• Raw and canonical environment-manifest comparisons, textual statement comparison, and git diff --check.
• lake shake --force --keep-public --explain LeanPool.FiveEighthsTheorem: inspected before/after. Every import remains necessary, including Linarith's compile-time dependency. No import removals were justified. --force skips shake's unrelated workspace cache prerequisite after the selected project is built; it bypasses no build or repository gate. The project import closure remains 2,987 modules, including project modules.

Remaining limitations: the full pool was not rebuilt or linted locally; CI is still required. The dependency closure is unchanged. No automatic merge was requested.

Reproduce the declaration invariant manifest

Save this inspector outside the content tree. Build the project at each revision, run lake env lean --run Manifest.lean manifest.jsonl, and compare the resulting JSONL files byte-for-byte. It deliberately preserves generated declarations and all non-theorem values. The only expression normalization erases kernel-irrelevant metadata and bound-variable labels.

import Lean

open Lean

deriving instance Repr for ReducibilityHints

def canonicalExpression : Expr → Expr
  | .mdata _ b => canonicalExpression b
  | .app f a => .app (canonicalExpression f) (canonicalExpression a)
  | .lam _ d b info => .lam Name.anonymous (canonicalExpression d) (canonicalExpression b) info
  | .forallE _ d b info =>
      .forallE Name.anonymous (canonicalExpression d) (canonicalExpression b) info
  | .letE _ t v b nondep => .letE Name.anonymous
      (canonicalExpression t) (canonicalExpression v) (canonicalExpression b) nondep
  | .proj name index b => .proj name index (canonicalExpression b)
  | e => e

def kind (c : ConstantInfo) : String :=
  match c with
  | .axiomInfo _ => "axiom"
  | .defnInfo _ => "definition"
  | .thmInfo _ => "theorem"
  | .opaqueInfo _ => "opaque"
  | .quotInfo _ => "quotient"
  | .inductInfo _ => "inductive"
  | .ctorInfo _ => "constructor"
  | .recInfo _ => "recursor"

def details (c : ConstantInfo) : String :=
  match c with
  | .defnInfo v => s!"{repr v.hints};{repr v.safety};{repr v.all}"
  | .thmInfo v => reprStr v.all
  | .opaqueInfo v => reprStr v.all
  | .inductInfo v =>
    s!"{v.numParams};{v.numIndices};{repr v.all};{repr v.ctors};{v.numNested};{v.isRec};{v.isReflexive}"
  | .ctorInfo v => s!"{repr v.induct};{v.cidx};{v.numParams};{v.numFields}"
  | .recInfo v =>
    s!"{repr v.all};{v.numParams};{v.numIndices};{v.numMotives};{v.numMinors};{v.k};" ++
      reprStr (v.rules.map fun r => (r.ctor, r.nfields, reprStr (canonicalExpression r.rhs)))
  | _ => ""

def main (args : List String) : IO Unit := do
  initSearchPath (← findSysroot)
  let env ← importModules #[{ module := `LeanPool.FiveEighthsTheorem }] {} (level := .private)
  let exported ← importModules #[{ module := `LeanPool.FiveEighthsTheorem }] {} (level := .exported)
  let mut declarations : Array (Name × Name) := #[]
  for (mod, data) in env.header.moduleNames.zip env.header.moduleData do
    if (`LeanPool.FiveEighthsTheorem).isPrefixOf mod then
      for name in data.constNames do
        declarations := declarations.push (name, mod)
  declarations := declarations.qsort fun a b => a.1.toString < b.1.toString
  let out ← IO.FS.Handle.mk (args.head!) .write
  for (name, mod) in declarations do
    let some c := env.find? name | throw <| IO.userError s!"missing {name}"
    let record := Json.mkObj [
      ("name", toJson name.toString), ("module", toJson mod.toString),
      ("kind", toJson (kind c)), ("universes", toJson (reprStr c.levelParams)),
      ("type", toJson (reprStr (canonicalExpression c.type))), ("unsafe", toJson c.isUnsafe),
      ("partial", toJson c.isPartial), ("exported", toJson (exported.contains name)),
      ("details", toJson (details c)),
      ("value", toJson (if c.isTheorem then "PROOF" else reprStr ((c.value? true).map canonicalExpression)))]
    out.putStrLn record.compress
  IO.println s!"Recorded {declarations.size} declarations; {env.header.moduleNames.size} modules"

[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 risk] Optimizes proof elaboration in a mathematical theorem.

No blocking issue was identified in the PR’s proof changes.

Summary

The PR rewrites five proof bodies in FiveEighthsTheorem to reduce elaboration work while leaving their declarations and statements unchanged. The changes since the previous review come from merging main and do not alter the PR’s proof file.

_{Reviews (4) · Last reviewed commit: "Merge current main without changing proj..."}

[Vilin97]

{
"summary": "At head 14c832c, the five proof-body changes preserve the counting argument while making witnesses, denominator nonvanishing, centralizer symmetry, and reciprocal inequalities explicit. I read the full source diff and inspected the saved environment manifests and benchmark/profile logs: all 45 declaration records agree after metadata/bound-name normalization, including non-theorem values; main-proof work falls from 17,690,471 to 9,136,354 raw profiler heartbeats. The observed median project-clean build falls from 3.2682s to 3.0951s on the shared VM. The two reciprocal wrappers rise modestly in profile cost, as disclosed, without offsetting the main improvement. Saved scoped validation logs pass; aggregate CI is still required. No new build was run for this review.",
"assessment": {
"scope": "targeted proof elaboration optimization",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The unchanged counting proof becomes more explicit and avoids broad search, with measured cost reduction and no new maintenance finding."
},
"verdict": "approve",
"findings": []
}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 16 tracked declarations across 1 modified file kept their type; only proofs / definition bodies changed.

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Compile cost of modified files — base → head

Heartbeats: 78 → 78 (+0, +0.0%). Declarations: 16 → 16.

Per-file wall sum: 6.4 s → 6.5 s (+1.9%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal.

Files: 1 compared — 0 cheaper, 0 costlier, 1 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%).

Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from Mathlib's linter.countHeartbeats, in maxHeartbeats units. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/FiveEighthsTheorem/Basic.lean	+22/-17	78	78	+0	+0.0%	6.40	6.52
Total	+22/-17	78	78	+0	+0.0%	6.4	6.5

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head 90f3538c7efbade36d3cec4fa383e84211a039e9. The complete FiveEighthsRoth proof-only refactor preserves the tracked statement types and reduces measured elaboration cost. It adds no new mathematical claim. The complete source/dependency review and recovered repairs were reconciled through the lossless main integration; fresh protected CI remains the integration authority.

Build project: pending/not yet reported, Content / non-content separation: SUCCESS, Documentation preflight: SUCCESS. These are observed check states, not an assertion that unfinished checks passed.

The remaining authority boundary is operational: this repository has allow_auto_merge=false, and GitHub rejected enablePullRequestAutoMerge with “Auto merge is not allowed for this repository.” The maintainer must make protected queuing available through an authorized repository-setting decision, or remove this label and perform a normal squash merge after the required checks and current-base integration pass. This cycle does not change repository settings or bypass protection. No unresolved substantive author-actionable finding justifies another change request or closure; the label is not for draft status, missing profiling, or an old advisory score.

[Vilin97]

🤖 LLM review — refactor (gpt-6-astra)

Reviewed head: 90f3538c7efbade36d3cec4fa383e84211a039e9

Verdict: ✅ approve

The refactor preserves the step-by-step counting argument while replacing broad automation with explicit witnesses, a shared nonzero-cardinality fact, and targeted rewrites. Centralizer membership and the final arithmetic become easier to follow and debug. The supplied measurements report a substantial main-proof improvement despite small increases in two wrappers. Build and timing results were not independently reproduced because this checkout lacks dependencies.

Aspect	Value
Scope	proof elaboration optimization
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The changes reduce reliance on broad proof search without sacrificing mathematical structure or introducing actionable maintenance debt.

---

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