refactor: drop unused triple_ratio_bound_bundle wrappers

[phasetr]

Deletion

Drop 8 unreferenced Λ-layer wrapper theorems (zero proof-power loss). Underlying ratio_bound lemmas and the base triple_ratio_sandwich_bundle{,_beta_zero} bundles remain.

• Ambient TripleRatios.lean (5): triple_ratio_bound_bundle, _beta_zero, _ferromagnetic, triple_ratio_sandwich_bundle_ferromagnetic, _beta_zero_ferromagnetic
• Concrete HighTemperatureBoundsTripleRatioBoundBundle.lean (3): whole file removed + umbrella import dropped
• Prose reconciled: sibling HighTemperatureBoundsTripleRatio.lean header count 7->4 and stale "Moved" section
• Untouched: AmbientLattice/SpecialCases/HighTemperatureBoundsTripleRatioBoundBundle.lean (along-exhaustion cluster, distinct file)

Verification

• lake build: green, warning-free (5057 jobs)
• audit_gate.py --full: V1-V4 PASS; --self-test 166 OK
• dead_candidate_scan.py --self-test: 79 OK (fixtures recalibrated, see below)
• lake exe GKSTest: PASS

Scanner: post-deletion cascade check (underlying consumed lemmas)

# python3 scripts/dead_candidate_scan.py <underlying-lemmas>
-- published-result: 2 --
-- load-bearing: 6 --
-- uncertain: 0 --
-- safe-to-delete: 0 --
-- cascade (informational, never auto-deleted): 0 --

# python3 scripts/dead_candidate_scan.py <underlying-lemmas> --lean
--lean cross-check: 8 candidate(s) compared against the elaborated graph; no consumer seen by Lean was missed on a safe-to-delete verdict
canary: 1064 declarations carrying 'Λ'x1061, 'β'x1, 'σ'x2 each find themselves: PASS
canary: 10903 code citations in tex/proof-guide.tex, none broken across a line: PASS
-- published-result: 2 --
-- load-bearing: 6 --
-- uncertain: 0 --
-- safe-to-delete: 0 --
-- cascade (informational, never auto-deleted): 0 --

cascade = 0, uncertain = 0, safe-to-delete = 0: every underlying lemma the deleted wrappers consumed stays PUBLISHED/LOAD_BEARING. No new dead candidate cascaded.

Fixture recalibration (_ferromagnetic family)

total 245 -> 241 (safe 114 -> 110; uncertain 44 / load-bearing 52 / published 35 invariant); zero-consumer 131 -> 128. The three invariant classes confirm no surviving lemma was reclassified. All 4 deleted _ferromagnetic decls were safe-to-delete; 3 were zero-consumer, the ambient _bound_bundle_ferromagnetic fed the _latticeGraph leaf (also deleted).

LIMITS banner (scanner)

LIMITS: this scan is textual. It cannot see simp/aesop set usage, tactic-generated
references, open/export-shortened names, or metaprogrammed names. It does not check
autoImplicit binder drift (a `#check @` dump is a separate gate). Doc rows that depend
on a lemma without naming it are invisible. Run with --lean on a green build to
cross-check the elaborated dependency graph; run --explain for the full table.
A "safe-to-delete" verdict is a necessary, not a sufficient, condition for deletion.

[phasetr]

Note (history correction): the original merge commit of this PR was amended locally and force-pushed to main post-merge, which rewrote published history — a process violation. main has been rolled back to be11e98d (the pre-#4669 state) and the byte-identical content was re-merged cleanly via #4671 (squash commit cc5dce87, committer GitHub, no amend, no post-merge force-push). Tracking issue #4670 is closed by #4671. No content change.