Targets
Several Riemannian/Util/ files are very small and thematically adjacent:
| File |
LOC |
Proposed |
ConnectionLaplacianSimp.lean |
41 |
merge into new OperatorSimp.lean |
DivergenceSimp.lean |
41 |
merge into new OperatorSimp.lean |
CovDerivBridges.lean |
52 |
merge into CovDerivSmoothness.lean |
Result: 3 small files → 1 merged + 1 absorbed. Net -2 files.
Rationale
- ~40-50 LOC files don't justify their own file overhead (imports, namespace header, docstring).
- "Common Closure Principle" (Robert C. Martin) — operator simp lemmas coevolve, belong together.
- CLAUDE.md "Design is subtraction": prefer fewer files when content is small + thematically tight.
Cascade
Consumers of ConnectionLaplacianSimp / DivergenceSimp / CovDerivBridges update imports. Smallish (~5-10 sites).
Acceptance
- Build clean
- Shake baseline maintained
- Sorry count unchanged
Related
Depends on or conflicts with: #5 (Util sub-directory reorg) — if #5 lands first, this consolidation happens inside the Util/Simp/ and Util/CovDeriv/ sub-dirs.
Targets
Several
Riemannian/Util/files are very small and thematically adjacent:ConnectionLaplacianSimp.leanOperatorSimp.leanDivergenceSimp.leanOperatorSimp.leanCovDerivBridges.leanCovDerivSmoothness.leanResult: 3 small files → 1 merged + 1 absorbed. Net -2 files.
Rationale
Cascade
Consumers of
ConnectionLaplacianSimp/DivergenceSimp/CovDerivBridgesupdate imports. Smallish (~5-10 sites).Acceptance
Related
Depends on or conflicts with: #5 (Util sub-directory reorg) — if #5 lands first, this consolidation happens inside the
Util/Simp/andUtil/CovDeriv/sub-dirs.