Optimize FiveEighths cardinality bridge

[Vilin97]

Summary

Optimizes the existing FiveEighthsTheorem project at 90a7c3320e0f79010d4ae72978377094092c546c by replacing the explicit subtype-cardinality equivalence in commProb_eq_ncard_div_sq with Lean's definitional congruence after unfolding commProb_def. The public declaration and all project mathematics remain unchanged.

Invariant audit

I generated a Lean environment manifest for all 45 declarations whose names contain FiveEighths, recording each fully elaborated type, safety flag, and definition value (theorem proof values are intentionally excluded because proof terms may change). Comparing base and head found:

• 45 declarations before and after
• no added or removed declarations
• no changed elaborated types, definition values, or safety flags

Measurements

• Base SHA: 90a7c3320e0f79010d4ae72978377094092c546c
• Head SHA: 21a45fec2357cd67bc7b2c42f9db1627ba2d0f26
• commProb_le_five_eighths_of_finite source elaboration: 14,497,276 → 8,609,290 heartbeats (40.6% reduction), measured with Lean's synchronous command profiler and trace.profiler.useHeartbeats=true.
• Warm lake build LeanPool.FiveEighthsTheorem.Imports: base 1.53 s and optimized 1.70 s in separate runs; wall time is dominated by imports and varied with concurrent VM load, so the declaration heartbeat profile is the meaningful signal. A clean base build was 9.24 s; the clean optimized run rebuilt shared dependency caches and is not used as a direct comparison.

Checks

• lake build LeanPool.FiveEighthsTheorem
• lake build --wfail LeanPool.FiveEighthsTheorem
• lake exe mk_all --module --check
• lake exe runLinter LeanPool.FiveEighthsTheorem
• lake exe lint-style LeanPool.FiveEighthsTheorem
• lake shake --force --keep-public --explain LeanPool.FiveEighthsTheorem.Basic (no import reduction suggested)
• uv run python -m lean_pool.quality --repo .. --static-only
• git diff --check

The full repository quality command was also attempted after the project build. It could not audit other projects because this worktree does not contain a full LeanPool build; it reported missing .olean files for unbuilt projects. The selected project declaration manifest, build, linter, style, index, and static quality checks passed. CI's pool build is the complete repository validation.

No CI/configuration/gate files or generated indexes were modified. This PR is intentionally open and has no auto-merge 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.

[Medium impact] No actionable defect was found in this proof-only change.

Summary

Replaces the explicit cardinality equivalence in commProb_eq_ncard_div_sq with rw [commProb_def] followed by congr 1.

• The commuting-pair equation now uses a shorter proof.

_{Reviews (1) · Last reviewed commit: "Optimize commuting probability cardinali..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "At 21a45fe, commProb_eq_ncard_div_sq replaces a representation-only subtype equivalence with rw [commProb_def] followed by congr 1. Pinned Mathlib definitions identify Commute with multiplication equality and Nat.card of a set with Set.ncard, so no mathematical argument is hidden. Whole-file forward and inverse comparison preserves every statement, definition, import, and other proof. Exact-head Build pool and Build project succeeded. The reported 40.6% heartbeat reduction remains an author measurement; this review did not reproduce it. The configured review approves this exact head. The PR merged through the protected native queue on 2026-10-13 at 18:23:30 UTC. Combined Lean CI run 38444123438 succeeded at merge commit 018a230; the accepted proof blob is unchanged in that commit and current main.",
"assessment": {
"scope": "local proof simplification",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "low",
"assessment_one_sentence": "The targeted rewrite removes redundant representation plumbing while retaining a short, explicit proof and the complete public mathematics."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: 21a45fec2357cd67bc7b2c42f9db1627ba2d0f26

Verdict: ✅ approve

This proof golf replaces a five-line explicit subtype-cardinality equivalence with rw [commProb_def] and a targeted definitional congr 1. The bridge remains local and direct, while the declaration elaborates with fewer heartbeats and no callers or surrounding structure are affected.

Aspect	Value
Scope	proof golf
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	➖ unchanged
Risk	✅ low

The refactor removes redundant proof machinery without introducing opaque automation or a material robustness risk, so it is safe to merge.

---

Tokens: 835,296 in / 6,998 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $3.4462 (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.