Tier 1: finish strict-defeq workaround removal (~7 sites left after #43)

[Xinze-Li-Moqian]

Part of umbrella #48. Depends on PR #43 (poet77) merging first.

Scope

PR #43 removes most uses of set_option backward.isDefEq.respectTransparency false, but ~7 sites remain (PR #43 documents 3 as residual; the rest are in Operators):

• OpenGALib/Riemannian/TensorBundle/Defs.lean × 1 (documented in [Depends on #41] Reduce strict defeq compatibility options (#8) #43)
• OpenGALib/Riemannian/TensorBundle/BundleSectionContinuity.lean × 1 (documented in [Depends on #41] Reduce strict defeq compatibility options (#8) #43)
• OpenGALib/Riemannian/Util/Tangent/TensorBundleCoercions.lean × 1 (documented in [Depends on #41] Reduce strict defeq compatibility options (#8) #43)
• OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean × 2
• OpenGALib/Riemannian/Operators/Laplacian.lean × 1
• OpenGALib/Riemannian/Operators/Hessian.lean × 3
• OpenGALib/Riemannian/Operators/HessianLie.lean × 1
• OpenGALib/Riemannian/Util/CovDerivSmoothness.lean × 1

Total ~11 sites; the 3 in #43's documented list may be genuinely blocked-upstream (and stay), the rest are SE-tractable.

Approach per site

Each transparency-false hides a strict-defeq friction. Replace with:

1. A structural fix in the proof body (preferred — same idea as PR [Depends on #41] Reduce strict defeq compatibility options (#8) #43)
2. Or a targeted lemma in a Util file if the friction is reused
3. Avoid bumping maxHeartbeats as a workaround (see memory)

Acceptance

• ≤ 3 remaining sites, each documented inline with a -- blocked-upstream: Mathlib issue #XXXX comment + reference link
• Full lake build clean

Suggested split

4-6 PRs, one per operator file. Run after #43 lands to avoid textual conflict.

Notes

Both maintainers assigned — coordinate via comments. The 3 sites poet77 already documented in #43 should be reviewed for whether they're genuinely upstream-blocked or could be fixed locally with more proof work.