Tier 1: omit hm — replace 'linter.unusedSectionVars false' with surgical omit (22 files)

[Xinze-Li-Moqian]

Part of umbrella #48.

Scope

22 files currently silence the unused-section-vars linter via set_option linter.unusedSectionVars false (a leftover from the explicit-g cascade's section-var widening). Each file should be cleaned by replacing the silence with surgical omit [...] in theorem ... on the specific declarations that need it, then deleting the global silence.

Reference: commit 7f1103d ("Koszul: omit unused [hm : HasMetric I M] in 10 theorems") did this for Riemannian/Connection/Koszul.lean — same pattern applies.

Files (22)

Run grep -rln "set_option linter.unusedSectionVars false" --include="*.lean" OpenGALib for the current list. Top candidates by likely density:

• OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
• OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
• OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean
• OpenGALib/Riemannian/Operators/ConnectionLaplacian.lean
• OpenGALib/Riemannian/Connection/LeviCivita.lean
• OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
• OpenGALib/Riemannian/Curvature/Tensoriality.lean
• … (15 more — full list via grep)

Acceptance

• 0 files contain set_option linter.unusedSectionVars false
• Full lake build clean with linter at baseline 0
• Sorry / shake / axiom counts unchanged

Suggested split

3-5 PRs grouped by sub-directory (e.g., one PR for Operators/Bochner/, one for Connection/, one for Curvature/). Coordinate via comments on this issue to avoid two-people-editing-the-same-file.

Notes

Both maintainers assigned — pick what fits your bandwidth. Claim a sub-group in a comment before starting.