Tier 1: eliminate maxHeartbeats 800000 hack in BundleSectionContinuity.lean

[Xinze-Li-Moqian]

Part of umbrella #48.

Scope

OpenGALib/Riemannian/TensorBundle/BundleSectionContinuity.lean:24 contains:

set_option maxHeartbeats 800000

This is a single residual maxHeartbeats bump in the codebase. Per project convention (memory: "Don't bump maxHeartbeats as a fix — Lean timeouts at whnf/elab signal structural proof issues; investigate root cause instead"), this should be removed by finding the structural cause.

Approach

1. Profile what whnf / elab steps consume the heartbeat budget
2. Either: introduce a helper lemma to stop reduction earlier, refactor the proof structure, or split the file
3. Or: identify a Mathlib-level performance issue and document inline with -- blocked-upstream: ...

Acceptance

• maxHeartbeats bump removed
• File builds with default heartbeats
• Build time for this module ≤ current

Suggested split

1 PR. Single file, contained scope.

Notes

Both maintainers assigned. This is a focused 4-6 hour debugging task; whoever wants the puzzle, comment to claim.