perf(wordram): bring Chan–He parameter proof under default heartbeats #1583

Reduce the private Parameters.exec_calculate proof in Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Parameters.lean to the default 200000-heartbeat budget, then remove its temporary 300000-cap entry from scripts/heartbeat_allowlist.txt. Status: available; this follow-up has no active implementation owner. It preserves the full #1446/#1394 objectives.

Baseline on #1469 at b79ae8e407f9f0349d2c14beb0d3e1aac8187e04, Lean 4.36.0-rc1: removing the original 800000 override makes the strict focused build fail at exec_calculate with a deterministic whnf timeout at 200000. An external Mathlib.Util.CountHeartbeats probe (#count_heartbeats in around the unchanged declaration) measured 256376 heartbeats. Keeping the exact original proof with a 300000 cap passes lake build --wfail --iofail Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters (3618 jobs). A bounded experiment replacing 89 simplifier-based register-frame transfers by their direct definitionally equal certificates still failed at 200000 and was reverted; it is not the submitted fix.

A concrete next approach is to split the twelve native segments and register frames into two private lemmas: the padding/logarithm/square-root prefix, then the remaining parameter arithmetic and output assembly. Give each an explicit state/frame contract and compose them in exec_calculate; introduce no parallel parameter model. The affected consumers include #1497 and its #1506/#1508 siblings, so coordinate supplier updates with their owners.

Completion requires the unchanged public declarations, program definitions, output/memory contracts and bounds; successful strict focused elaboration under the default budget; removal of the scoped allowance; required final-source CI and independent proof/resource review. Preserve original source credit. Created by OpenAI Codex coordinator session coordinator-codex-queue-20261028-ready-c from the measured integration blocker; no original objective is closed.