Optimize Redhill subsum sign arguments

[Vilin97]

Redhill's subsum proofs repeatedly re-established elementary facts about SignType inside large arithmetic contexts. In particular, OddCase.isSubsumBlock_redEmb1 spent most of its elaboration cost using tauto to assemble a constant function from three equal signs. This replaces that search with explicit equalities and reuses small sign-bound lemmas in the general and odd cases.

Only three files in the existing Redhill project change. All pre-existing declaration signatures and definitions stay fixed; two supporting lemmas are added. Existing imports, the project YAML card, and generated indexes remain unchanged.

Base: 3c52e024b18d022029a368447e929bc80ccd1364 (fetched and verified again immediately before commit).
Head: 921ca6a2657995e2dd27ac8081656214affc6cf2
Toolchain: the repository's existing Lean/Mathlib v4.35.0-rc3 pins.

Redhill was selected after comparing tactic concentration in existing projects: 138 grind occurrences across roughly 3,500 lines and 10–12-second coprimality/subsum modules in the initial build. Synchronous profiling then identified the specific sign argument below. This is evidence for a useful local target, not a claim of a global optimum across the pool.

Invariant audit

Before editing, an external Lean environment inspector imported all 21 project modules with importAll := true, extensions disabled, and trust level zero. It serialized every module-owned ConstantInfo: full elaborated type expression DAG, universe parameters, safety/partial flags, declaration kind, associated declarations, reducibility hints, and non-theorem values/inductive/recursor data. The comparator checks structural expressions after discarding only expression metadata; theorem proof bodies may differ. It keys entries by both module and name, retaining generated private declarations and repeated equation-theorem names.

Result: 965 pre-existing module/declaration entries (963 distinct names), zero missing and zero changed; exactly two new sign lemmas, giving 967 entries (965 names). This covers definition values as well as theorem types. The axiom audit also walks generated private declarations. Source review confirms no changes to notation, namespace/export declarations, attributes, definitions, or existing statement syntax.

Manifest SHA-256:

• Base: 10840c1772cc4d22e214274fb38d519e67aadbd56f5a6f98dc515744f3b4f328
• Head: e784c37520a884e3384ac9aa96f63c2bb61bb7300a2b076a13975bccead1e062

Measurements

Three project rebuilds per revision on the same Azure VM, deleting all Redhill artifacts under .lake/build/lib/lean and .lake/build/ir before each lake build LeanPool.Redhill.Imports. Dependencies remained cached; Lake used its normal parallelism. All six runs succeeded without warnings. No local linters or other local profiling jobs ran concurrently with these measurements.

Measurement	Base	Optimized
Project build, three runs (seconds)	31.602787 / 32.646992 / 29.731653	29.608550 / 30.636105 / 30.041932
Median project build (seconds)	31.602787	30.041932
Odd.Subsum instrumented serial run (seconds)	29.209237	10.476919
General.Subsum instrumented serial run (seconds)	21.165995	17.789162
OddCase.isSubsumBlock_redEmb1 heartbeats	117,728.755	2,566.544
OddCase.natAbs_le_redEmb1_reduced heartbeats	6,241.170	3,963.443
GeneralCase.X4_le_natAbs_b4 heartbeats	20,588.006	20,254.266
GeneralCase.X4_le_natAbs_b3 heartbeats	24,475.100	24,183.177
GeneralCase.X_le_natAbs_redEmb1 heartbeats	29,785.229	29,294.457

Observed median full-build improvement: 4.94%. The main hotspot uses 97.82% fewer heartbeats. The isolated serial runs use -DElab.async=false -Dtrace.Elab.command=true -Dtrace.profiler=true -Dtrace.profiler.useHeartbeats=true -Dtrace.profiler.threshold=1000000000000000000, with each module's native --setup file. Heartbeats are raw profiler allocations divided by 1,000; the largest command trace for each declaration is reported, without adding its nested macro-expansion traces.

Validation

• lake build LeanPool.Redhill.Imports, repeated clean project builds, and explicit final warning scan.
• lake env lean --run scripts/ci/lint-project.lean <all 21 Redhill modules>: passed (965 declaration names).
• lake exe lint-style LeanPool.Redhill.Imports: passed.
• Existing repository quality functions, externally scoped to all 21 project files and the unchanged redhill.yaml: headers, forbidden constructs/options, size limits, card/declaration resolution, axioms, and compiled option/backdoor audit passed.
• Separate all-declaration axiom traversal: only Classical.choice, propext, and Quot.sound.
• python3 scripts/project-indexes.py --repo <Redhill-only projection> --module --check: passed using the unchanged official generator; no source modules were added, removed, or moved.
• git diff --check: passed.
• lake shake --force --keep-public LeanPool.Redhill.Imports: analyzed the built target and returned its existing seven groups of redundant-import suggestions (exit 1). Imports were left unchanged; no waiver was added.

Measurements use warm dependencies on a shared VM; they do not establish a statistical speedup for every CI run. Instrumented serial time is separate from parallel build time. The whole-pool build/lint gates remain for CI. Full logs, source snapshots, exporter, comparator, timing scripts, and the exact-head checkpoint are preserved on the VM under /data/codex/scratch/vilin/optimization-20261015/.

Leave this PR open for normal protected review. No merge, queue entry, or auto-merge is requested by this cycle.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium impact] No blocking issue was found in this proof-only refactor.

Summary

Replaces repeated sign searches with two shared bounds and explicit equalities across three existing Redhill modules.

• General subsum proofs reuse sign bounds and order facts.
• Odd subsum proofs build sign equalities directly.

_{Reviews (1) · Last reviewed commit: "Optimize Redhill subsum sign arguments" · Reviewed by Greptile}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 921ca6a2657995e2dd27ac8081656214affc6cf2

Verdict: ✅ approve

The refactor extracts two reusable sign bounds, replaces repeated sign searches with explicit order lemmas, and replaces the odd subsum proof’s tauto step with direct equalities. Existing arithmetic case splits remain intact. The helper’s simp_all is confined to nine elementary cases, so it adds no meaningful brittleness. Builds and reported timings were not independently rerun because dependency artifacts are absent from this checkout.

Aspect	Value
Scope	tactic rewrite and lemma extraction
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The refactor preserves proof structure while replacing contextual automation with reusable sign facts and explicit equality proofs.

---

Tokens: 391,457 in / 4,399 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $1.6318 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

Reviewed 921ca6a2657995e2dd27ac8081656214affc6cf2: the complete three-file refactor is source-favorable. My review and an independent source review found no blocking issue.

The two shared sign bounds correctly handle all three signs and every distinct pair. The strict-order replacements retain the zero and negative cases. In the odd subsum proof, the witness b 0 now follows directly from the two equalities, with the required symmetry; the arithmetic case splits and existing statement syntax remain intact. No existing definition, import, attribute or namespace changes. The small finite-case simp_all proof adds no material maintenance debt.

Assessment: tactic replacement and lemma extraction; maintainability improved; more robust; low risk; findings: none.

Exact-head CI is green, including Build pool and Build project, and configured review 2133 independently reports approval. I did not rerun builds, the compiled environment comparison or profiling. The reported timing reductions are the author’s measurements on a shared VM.

Source review is complete. This unchanged accepted head entered the protected native queue at 07:10:58Z against validated main0c1132c7a9a2b320f9c37556412a4733e45c6a47. The queue completed combined commit d4f532e: Build pool116857798210 and the required Build project aggregate succeeded, with all eight normal required contexts satisfied by applicable successes or scope skips. GitHub records the PR merged at 2026-10-16T07:36:44Z into that same integration commit. No author-branch update, admin merge, auto-merge setting or gate waiver was used. Current main may advance independently; later admissions require their own fresh main and source checks.