[Umbrella] Post-cascade engineering sweep — tech-debt cleanup after explicit-g landing

[Xinze-Li-Moqian]

Goal

With the explicit-g cascade (#9) landed, several engineering-debt items remain or surfaced. This umbrella bundles them so we can track progress and split work without losing sight of the whole. Items are organized by tier; either maintainer can pick what fits their bandwidth and split into sub-PRs as appropriate.

Sub-issues

Tier 1 — Mechanical, low risk, parallel-friendly

• Tier 1: omit hm — replace 'linter.unusedSectionVars false' with surgical omit (22 files) #49 — omit hm cleanup: replace set_option linter.unusedSectionVars false with surgical omit (22 files)
• Tier 1: finish strict-defeq workaround removal (~7 sites left after #43) #50 — Finish strict-defeq workaround removal — ~7 sites left (depends on [Depends on #41] Reduce strict defeq compatibility options (#8) #43 merging)
• Tier 1: eliminate maxHeartbeats 800000 hack in BundleSectionContinuity.lean #51 — Eliminate maxHeartbeats 800000 hack in BundleSectionContinuity.lean (1 file)
• Tier 1: add README.md to 20 sub-directories currently lacking one #52 — Add README.md to 20 sub-directories currently lacking one

Tier 2 — Larger scope, discuss before PR

• Tier 2: drive shake baseline 38 → 0 #53 — Drive shake baseline 38 → 0 (~50-80 unused-import edits)
• Tier 2: split files exceeding 800 LOC into themed sub-modules #54 — Split files >800 LOC (RiemannCurvature 1089, LeviCivita 945, Tensoriality 931, MusicalIso 711)

Tier 3 — Design / process

• Tier 3: design — IsStationary/IsStable/IsUnstable quantified-Prop vs explicit-g #55 — Decide quantified-Prop vs explicit-g for IsStationary/IsStable/IsUnstable
• Tier 3: draft docs/AI_COLLAB.md — AI-driven PR conventions #56 — Draft docs/AI_COLLAB.md for AI-driven PR conventions

Working agreement

• All sub-issues assigned to both @Xinze-Li-Moqian and @poet77.
• Either maintainer can pick up an item; comment on the sub-issue to claim before starting.
• Sub-PRs welcome — feel free to split any item into smaller chunks as practical.
• Tier 1 items can proceed independently in parallel.
• Tier 2 items: discuss in the sub-issue thread before opening a PR (especially the file split — anchor-file semantics matter).
• Tier 3 items: align as peers before drafting.

Recommended order

After poet77's #41 / #43 land into main:

1. Tier 1: omit hm — replace 'linter.unusedSectionVars false' with surgical omit (22 files) #49 omit hm cleanup (parallel across files, low risk)
2. Tier 1: add README.md to 20 sub-directories currently lacking one #52 README additions (parallel-friendly, splittable)
3. Tier 1: eliminate maxHeartbeats 800000 hack in BundleSectionContinuity.lean #51 maxHeartbeats hack removal (1 PR)
4. Tier 1: finish strict-defeq workaround removal (~7 sites left after #43) #50 strict-defeq workaround finish (post-[Depends on #41] Reduce strict defeq compatibility options (#8) #43)
5. Tier 2: drive shake baseline 38 → 0 #53 shake baseline drive (long-running, low priority)
6. Tier 2: split files exceeding 800 LOC into themed sub-modules #54 file split + Tier 3: design — IsStationary/IsStable/IsUnstable quantified-Prop vs explicit-g #55 IsStationary discussion (after Tier 1 cleared)
7. Tier 3: draft docs/AI_COLLAB.md — AI-driven PR conventions #56 AI_COLLAB.md (anytime, needs peer alignment)

Acceptance for the umbrella

• All Tier 1 sub-issues closed
• Tier 2 sub-issues either resolved or explicitly deferred with rationale
• Tier 3 sub-issues either resolved or explicitly deferred with rationale
• CI baselines updated to reflect new shake / sorry / linter counts where applicable