feat: sharp asymptotic bounds for runs of multiples

[Vilin97]

Adds the sharp extremal order n log n log log n for the sum of first missing multiple indices in an arbitrary finite set of positive integers. The project includes entropy and chain-compression upper bounds and two matching lower-bound constructions, with reusable counting entropy, compression, prime estimates, and block replication.

Source: jas-ho/runs-of-multiples-lean, pinned at 8b7e5f23534c321722725f78b6e64981557f0ef5, Apache-2.0. Its completed formalization commit is dated 2026-10-09 08:21:13 UTC, inside this acquisition cycle's window [2026-10-02 09:15:20 UTC, 2026-10-09 09:15:20 UTC). The upstream production account dates the proof work to October 7; eligibility does not rely on a mirror or indexing update.

Provenance is AI: Claude Opus 5.5 wrote both Lean proofs under Jason Hoelscher-Obermaier's direction; GPT-6-Astra wrote the informal compression argument. The card and entry module credit the owner and proof model and cite the pinned source. All 16 upstream proof modules and the small examples are retained, with five extracted modules for shared prime inputs/estimates, analytic estimates, block replication and the transfer to every large cardinality. PDFs, tools, upstream configuration and caches are not vendored. LeanPool.lean remains fixed; one YAML card and the generated public project wrapper are added.

The port targets Lean Pool's exact Lean v4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e, adds module visibility and license/attribution headers, and documents four previously undocumented chain-system fields. Both endpoint theorem statements and all useful generality are preserved. The two routes share basic definitions, elementary estimates and padding; the upper-bound arguments and lower-block constructions remain distinct.

Measured optimization used clean project outputs with cached pinned dependencies, default Lake scheduling, and the same command: /usr/bin/time -v lake --wfail build LeanPool.RunsOfMultiples.Imports. Baseline 35.64 s; the final source measured 22.17 s and 24.05 s in two clean builds (32.5–37.8% faster); CPU user time 69.32 → 56.30 / 58.75 s. The previous checkpoint measured 20.52 s; wall time varies with shared-VM scheduling, so the final measurements are both reported. The pass split serial prime/upper dependencies, made the lower constructions compile independently, replaced duplicate padding proofs with a general block-transfer theorem, and restricted nonlinear arithmetic to the needed facts. Synchronous allocation-heartbeat profiles fell 200,815 → 63,533 for upper_of_primeInput, 199,588 → 35,165 for many_primes, and 91,666 → 30,156 for fibre_bound; two ~131,000-heartbeat padding proofs became one ~36,695-heartbeat general proof, and restricting the final upper-core arithmetic reduced it 35,801 → 12,483. These profiles are diagnostic; their wall times are not mixed with build measurements. No heartbeat override or suppression is introduced.

Local validation passed:

• Clean warning-free project build and lake exe mk_all --module --check.
• The repository's slow declaration linters: 23 modules, 459 declarations.
• lake exe lint-style LeanPool.RunsOfMultiples.Imports.
• Full repository static quality checks; project card/declaration checks; axiom closure for 185 named source declarations, and the option/backdoor audit over every imported project module.
• Content-only diff and git diff --check; no Python changes.

No duplicate was found in current-main cards/source/history, Lean Pool PRs/issues, Mathlib source/code searches, or TauCeti code/PR searches by repository, namespace and distinctive terminology. This is search evidence, not an exhaustive claim about mathematical prior literature. The cited upstream write-ups state the matching asymptotic bounds; the Lean uses (q,4q] and a larger logarithmic cutoff to discharge the prime input with Mathlib's Chebyshev estimates, as upstream documents.

Final-head CI and the configured Greptile/GPT reviews have validated this head. The infrastructure rollout PR610/PR611 is merged; exact current-main CI was verified green at fbe0fe3397f00e1933ffec1aed9a7f882898b1d2 (full pool build, lint and quality run). No protected rollout branch or gate is changed.

Final-head CI passed the project build, indexes, linters, style and repository quality audit. Greptile found no actionable issue; GPT and the separate thorough review both approve exact head eb39eb3. The refreshed advisory profile covered all 23 files without profile errors (36.47 s on its GitHub runner; distinct from the controlled local comparison).

Admitted to the protected native queue at 10:48:45 UTC on October 9, after all required contexts passed or were normally scope-skipped. Current-main parent c4d20f0 also has successful exact-head queue CI; Lean and Mathlib pins are unchanged. The current pinned TauCeti tree was checked for the selected project in addition to the prior code/issue searches. Full integration CI is still running. All 24 queued project/card files match the approved head byte for byte; the author branch has not been rebased to chase main. Final acquisition state: auto-merge pending in the native queue.

[greptile-apps]

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

[Low impact] No blocking code issue was found in the current changes; upstream source checks remain unverified.

Summary

Adds sharp bounds of order n log n log log n for sums of first missing multiple indices, with entropy and compression proofs and two lower-bound constructions.

• Since the previous review, only four arithmetic tactics in upper_core changed.
• Both headline statements match the card’s claims, including lower bounds for every sufficiently large cardinality.
• No new actionable issue or mounted-rule violation was found. No previous finding threads were supplied.
• Upstream license, source fidelity, proof provenance, and acquisition dates remain externally unverified. The reported performance measurements were not independently repeated.

_{Reviews (2) · Last reviewed commit: "Restrict arithmetic search in the upper ..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 36.47 s (= 0.61 min) — user 64.06 s, sys 9.25 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 889,245 maxHeartbeats units across 23 valid files (3,839 added LOC).

Sum of lean --profile: 51630.9 ms (= 51.63 s) across 23 valid files. Import-excluded time: 32851.9 ms (= 32.85 s).

Count-heartbeats wall-clock total: 113.58 s. Repeated import cost inside lean --profile: 18779.0 ms (= 18.78 s).

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Commands	Errors
LeanPool/RunsOfMultiples/Alt/Lower.lean	526	227,642	20.67	7.72	6.86	0.87	109	0
LeanPool/RunsOfMultiples/Upper.lean	381	146,549	11.68	5.06	4.34	0.72	18	0
LeanPool/RunsOfMultiples/Lower.lean	294	100,738	7.93	3.93	3.03	0.90	42	0
LeanPool/RunsOfMultiples/Alt/Radical.lean	336	66,799	7.52	3.29	2.45	0.84	21	0
LeanPool/RunsOfMultiples/OneStep.lean	204	62,337	8.21	3.24	2.52	0.72	15	0
LeanPool/RunsOfMultiples/PrimeEstimates.lean	219	60,108	8.88	3.50	2.61	0.89	16	0
LeanPool/RunsOfMultiples/Alt/Chains.lean	429	54,237	5.45	2.46	1.96	0.50	40	0
LeanPool/RunsOfMultiples/BlockLower.lean	110	36,580	6.46	2.82	2.03	0.79	7	0
LeanPool/RunsOfMultiples/LowerEstimates.lean	71	31,195	4.29	1.96	1.06	0.90	16	0
LeanPool/RunsOfMultiples/Alt/Upper.lean	86	26,644	3.77	1.82	0.97	0.85	9	0
LeanPool/RunsOfMultiples/Alt/Compression.lean	360	25,972	4.12	1.73	1.23	0.50	41	0
LeanPool/RunsOfMultiples/Entropy.lean	197	21,525	2.86	1.51	0.83	0.69	43	0
LeanPool/RunsOfMultiples/Replication.lean	101	10,594	1.90	0.87	0.40	0.47	11	0
LeanPool/RunsOfMultiples/Defs.lean	119	7,290	2.08	0.88	0.44	0.44	31	0
LeanPool/RunsOfMultiples/Examples.lean	60	5,116	2.16	0.78	0.34	0.44	10	0
LeanPool/RunsOfMultiples/Edges.lean	88	3,954	2.17	1.03	0.32	0.71	11	0
LeanPool/RunsOfMultiples/Primes.lean	48	724	2.31	1.12	0.25	0.87	10	0
LeanPool/RunsOfMultiples/PrimeInput.lean	36	423	1.45	0.95	0.21	0.74	8	0
LeanPool/RunsOfMultiples/Alt/Main.lean	35	334	2.02	1.15	0.24	0.91	6	0
LeanPool/RunsOfMultiples/Main.lean	40	334	2.30	1.13	0.24	0.90	6	0
LeanPool/RunsOfMultiples/Alt/Defs.lean	33	149	1.28	0.59	0.17	0.43	7	0
LeanPool/RunsOfMultiples.lean	36	0	1.85	3.02	0.20	2.82	3	0
LeanPool/RunsOfMultiples/Imports.lean	30	0	2.22	1.07	0.17	0.90	1	0
Total	3,839	889,245	113.58	51.63	32.85	18.78	481	0

Aggregate phase totals

Phase	Time
import	18779.0 ms (= 18.78 s)
interpretation	10328.0 ms (= 10.33 s)
tactic execution	7403.2 ms (= 7.40 s)
typeclass inference	5099.5 ms (= 5.10 s)
type checking	1827.1 ms (= 1.83 s)
linting	1809.8 ms (= 1.81 s)
norm_num	1397.1 ms (= 1.40 s)
simp	1205.6 ms (= 1.21 s)
ring	792.3 ms (= 0.79 s)
tacticAnalysis	709.4 ms (= 0.71 s)
elaboration	679.7 ms (= 0.68 s)
initialization	673.3 ms (= 0.67 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.RunsOfMultiples.Upper	7.00 s
LeanPool.RunsOfMultiples.Alt.Lower	6.80 s
LeanPool.RunsOfMultiples.PrimeEstimates	6.00 s
LeanPool.RunsOfMultiples.Alt.Radical	5.80 s
LeanPool.RunsOfMultiples.Lower	5.50 s
LeanPool.RunsOfMultiples.BlockLower	5.10 s
LeanPool.RunsOfMultiples.OneStep	4.40 s
LeanPool.RunsOfMultiples.LowerEstimates	3.90 s
LeanPool.RunsOfMultiples.Alt.Chains	3.90 s
LeanPool.RunsOfMultiples.PrimeInput	3.30 s
LeanPool.RunsOfMultiples.Alt.Compression	2.60 s
LeanPool.RunsOfMultiples.Defs	2.50 s

Per-file `lean --profile` output

LeanPool/RunsOfMultiples.lean

import took 2.82s
cumulative profiling times:
	elaboration 0.229ms
	import 2.82s
	initialization 28ms
	interpretation 164ms
	linting 1.01ms
	module linting 0.00187ms
	overlappingInstancesLinter 0.649ms
	parsing 0.365ms
	tacticAnalysis 5.66ms
real 3.48
user 1.05
sys 0.65

LeanPool/RunsOfMultiples/Alt/Chains.lean

import took 496ms
cumulative profiling times:
	attribute application 0.109ms
	blocked (unaccounted) 1.89ms
	congr simp thm 2.07ms
	elaboration 70.2ms
	fix level params 1.04ms
	import 496ms
	initialization 26ms
	instantiate metavars 9.05ms
	interpretation 352ms
	let-to-have transformation 0.158ms
	linting 57.2ms
	module linting 0.00182ms
	norm_num 3.92ms
	overlappingInstancesLinter 8.72ms
	parsing 19ms
	process pre-definitions 19.6ms
	ring 44ms
	share common exprs 16.5ms
	simp 80.7ms
	tactic execution 515ms
	tacticAnalysis 89ms
	type checking 430ms
	typeclass inference 213ms
real 1.76
user 2.45
sys 0.46

LeanPool/RunsOfMultiples/Alt/Compression.lean

import took 498ms
cumulative profiling times:
	attribute application 0.177ms
	blocked (unaccounted) 0.42ms
	compilation (IR) 0.157ms
	compilation (LCNF base) 0.959ms
	compilation (LCNF impure) 0.683ms
	compilation (LCNF mono) 1.98ms
	congr simp thm 7.31ms
	elaboration 64.8ms
	fix level params 0.843ms
	import 498ms
	initialization 26ms
	instantiate metavars 3.21ms
	interpretation 328ms
	let-to-have transformation 0.173ms
	linting 38.9ms
	module linting 0.00222ms
	norm_num 1.95ms
	overlappingInstancesLinter 11.2ms
	parsing 15.3ms
	process pre-definitions 11.1ms
	ring 14.4ms
	share common exprs 6.75ms
	simp 74.6ms
	tactic execution 259ms
	tacticAnalysis 52.9ms
	type checking 161ms
	typeclass inference 148ms
real 1.50
user 1.73
sys 0.46

LeanPool/RunsOfMultiples/Alt/Defs.lean

import took 426ms
cumulative profiling times:
	attribute application 0.0178ms
	elaboration 4.46ms
	fix level params 0.0164ms
	import 426ms
	initialization 44.8ms
	instantiate metavars 0.0186ms
	interpretation 102ms
	let-to-have transformation 0.0217ms
	linting 2.21ms
	module linting 0.00205ms
	overlappingInstancesLinter 2.18ms
	parsing 1.07ms
	process pre-definitions 0.537ms
	share common exprs 0.0545ms
	tacticAnalysis 5.35ms
	type checking 0.2ms
	typeclass inference 3.1ms
real 1.04
user 0.64
sys 0.43

LeanPool/RunsOfMultiples/Alt/Lower.lean

import took 868ms
linting took 148ms
linting took 218ms
linting took 168ms
linting took 183ms
linting took 142ms
tactic execution of Lean.Parser.Tactic.congr took 341ms
tactic execution of Lean.Parser.Tactic.rintro took 227ms
tactic execution of Lean.Parser.Tactic.refine took 143ms
tactic execution of Lean.Parser.Tactic.refine took 210ms
linting took 253ms
tactic execution of Lean.Parser.Tactic.refine took 299ms
tactic execution of Lean.Parser.Tactic.refine took 155ms
tactic execution of Lean.Parser.Tactic.refine took 325ms
linting took 198ms
cumulative profiling times:
	attribute application 0.508ms
	blocked (unaccounted) 0.351ms
	compilation (IR) 0.221ms
	compilation (LCNF base) 4.37ms
	compilation (LCNF impure) 0.931ms
	compilation (LCNF mono) 1.53ms
	congr simp thm 8.35ms
	elaboration 123ms
	fix level params 2.59ms
	import 868ms
	initialization 26.4ms
	instantiate metavars 11.4ms
	interpretation 906ms
	let-to-have transformation 0.491ms
	linting 1.39s
	module linting 0.00242ms
	norm_num 239ms
	overlappingInstancesLinter 13.3ms
	parsing 28.6ms
	process pre-definitions 37.2ms
	ring 103ms
	share common exprs 37.9ms
	simp 132ms
	tactic execution 2.92s
	tacticAnalysis 92.1ms
	type checking 291ms
	typeclass inference 485ms
real 3.32
user 7.53
sys 0.60

LeanPool/RunsOfMultiples/Alt/Main.lean

import took 907ms
cumulative profiling times:
	attribute application 0.0158ms
	elaboration 7.5ms
	fix level params 0.0217ms
	import 907ms
	initialization 26.4ms
	instantiate metavars 0.0205ms
	interpretation 191ms
	let-to-have transformation 0.0301ms
	linting 2.58ms
	module linting 0.0028ms
	overlappingInstancesLinter 1.32ms
	parsing 1.49ms
	process pre-definitions 0.194ms
	share common exprs 0.0979ms
	tacticAnalysis 6.57ms
	type checking 0.348ms
	typeclass inference 4.87ms
real 1.61
user 1.12
sys 0.52

LeanPool/RunsOfMultiples/Alt/Radical.lean

import took 839ms
cumulative profiling times:
	attribute application 0.111ms
	congr simp thm 8.74ms
	elaboration 41.4ms
	fix level params 1.42ms
	import 839ms
	initialization 30.9ms
	instantiate metavars 5.34ms
	interpretation 706ms
	let-to-have transformation 0.14ms
	linting 47ms
	module linting 0.00552ms
	norm_num 49.3ms
	overlappingInstancesLinter 6.04ms
	parsing 16.3ms
	process pre-definitions 22.7ms
	ring 75.7ms
	share common exprs 16.1ms
	simp 230ms
	tactic execution 415ms
	tacticAnalysis 59.8ms
	type checking 137ms
	typeclass inference 583ms
real 2.26
user 3.20
sys 0.56

LeanPool/RunsOfMultiples/Alt/Upper.lean

import took 851ms
tactic execution of Mathlib.Tactic.nlinarith took 117ms
cumulative profiling times:
	attribute application 0.0242ms
	congr simp thm 5.44ms
	elaboration 11.5ms
	fix level params 0.268ms
	import 851ms
	initialization 26.3ms
	instantiate metavars 0.797ms
	interpretation 401ms
	let-to-have transformation 0.0374ms
	linting 7.06ms
	module linting 0.00224ms
	norm_num 1.59ms
	overlappingInstancesLinter 1.78ms
	parsing 3.97ms
	process pre-definitions 3.62ms
	ring 19.4ms
	share common exprs 2.62ms
	simp 87.8ms
	tactic execution 203ms
	tacticAnalysis 15.3ms
	type checking 28.7ms
	typeclass inference 152ms
real 2.21
user 1.77
sys 0.55

LeanPool/RunsOfMultiples/BlockLower.lean

import took 793ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 188ms
cumulative profiling times:
	attribute application 0.065ms
	congr simp thm 5ms
	elaboration 21.1ms
	fix level params 0.904ms
	import 793ms
	initialization 27.9ms
	instantiate metavars 4.28ms
	interpretation 900ms
	let-to-have transformation 0.0401ms
	linting 17.9ms
	module linting 0.00216ms
	norm_num 78.8ms
	overlappingInstancesLinter 2.52ms
	parsing 7.22ms
	process pre-definitions 13.1ms
	ring 52.1ms
	share common exprs 26.8ms
	simp 84.4ms
	tactic execution 242ms
	tacticAnalysis 29.4ms
	type checking 64.1ms
	typeclass inference 450ms
real 3.26
user 2.79
sys 0.53

LeanPool/RunsOfMultiples/Defs.lean

import took 440ms
cumulative profiling times:
	attribute application 0.113ms
	compilation (IR) 0.12ms
	compilation (LCNF base) 1.71ms
	compilation (LCNF impure) 0.464ms
	compilation (LCNF mono) 0.72ms
	congr simp thm 0.389ms
	elaboration 23.6ms
	fix level params 0.236ms
	import 440ms
	initialization 37.1ms
	instantiate metavars 0.542ms
	interpretation 167ms
	let-to-have transformation 0.12ms
	linting 12.6ms
	module linting 0.00181ms
	overlappingInstancesLinter 4.05ms
	parsing 6.05ms
	process pre-definitions 2.97ms
	share common exprs 1.4ms
	simp 11.7ms
	tactic execution 54.1ms
	tacticAnalysis 17.1ms
	type checking 51.6ms
	typeclass inference 46.1ms
real 1.14
user 0.92
sys 0.43

LeanPool/RunsOfMultiples/Edges.lean

import took 712ms
cumulative profiling times:
	attribute application 0.0317ms
	congr simp thm 0.204ms
	elaboration 12ms
	fix level params 0.102ms
	import 712ms
	initialization 27.4ms
	instantiate metavars 0.278ms
	interpretation 174ms
	let-to-have transformation 0.0505ms
	linting 7.32ms
	module linting 0.00217ms
	overlappingInstancesLinter 3.07ms
	parsing 2.95ms
	process pre-definitions 1.79ms
	share common exprs 0.669ms
	simp 1.51ms
	tactic execution 38.2ms
	tacticAnalysis 9.84ms
	type checking 10.7ms
	typeclass inference 32.7ms
real 1.42
user 1.03
sys 0.49

LeanPool/RunsOfMultiples/Entropy.lean

import took 689ms
cumulative profiling times:
	attribute application 0.195ms
	blocked (unaccounted) 0.71ms
	congr simp thm 5.59ms
	elaboration 48.1ms
	fix level params 0.54ms
	import 689ms
	initialization 32.6ms
	instantiate metavars 1.25ms
	interpretation 251ms
	let-to-have transformation 0.211ms
	linting 17.8ms
	module linting 0.00177ms
	norm_num 0.111ms
	overlappingInstancesLinter 6.26ms
	parsing 8.75ms
	process pre-definitions 6.46ms
	ring 2.42ms
	share common exprs 3.75ms
	simp 100ms
	tactic execution 130ms
	tacticAnalysis 29.7ms
	type checking 39.4ms
	typeclass inference 141ms
real 1.56
user 1.52
sys 0.50

LeanPool/RunsOfMultiples/Examples.lean

import took 442ms
cumulative profiling times:
	attribute application 0.0287ms
	congr simp thm 0.543ms
	elaboration 7.94ms
	fix level params 0.104ms
	import 442ms
	initialization 35.8ms
	instantiate metavars 0.094ms
	interpretation 135ms
	let-to-have transformation 0.0255ms
	linting 4.35ms
	module linting 0.00195ms
	overlappingInstancesLinter 1.67ms
	parsing 4.61ms
	process pre-definitions 1.61ms
	share common exprs 0.867ms
	simp 8.68ms
	tactic execution 61.6ms
	tacticAnalysis 10.6ms
	type checking 16.7ms
	typeclass inference 46.4ms
real 1.18
user 0.85
sys 0.40

LeanPool/RunsOfMultiples/Imports.lean

import took 895ms
cumulative profiling times:
	elaboration 0.102ms
	import 895ms
	initialization 26.5ms
	interpretation 144ms
	linting 0.265ms
	module linting 0.00209ms
	overlappingInstancesLinter 0.123ms
	parsing 0.00257ms
	tacticAnalysis 0.425ms
real 1.56
user 1.04
sys 0.52

LeanPool/RunsOfMultiples/Lower.lean

import took 901ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 109ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 136ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 103ms
cumulative profiling times:
	attribute application 0.195ms
	compilation (IR) 0.0599ms
	compilation (LCNF base) 0.618ms
	compilation (LCNF impure) 0.228ms
	compilation (LCNF mono) 0.189ms
	congr simp thm 6.77ms
	elaboration 72.6ms
	fix level params 1.68ms
	import 901ms
	initialization 27.3ms
	instantiate metavars 4.15ms
	interpretation 1.13s
	let-to-have transformation 0.249ms
	linting 52.3ms
	module linting 0.00239ms
	norm_num 134ms
	overlappingInstancesLinter 6.44ms
	parsing 22ms
	process pre-definitions 22.8ms
	ring 112ms
	share common exprs 24.5ms
	simp 88.5ms
	tactic execution 412ms
	tacticAnalysis 65.1ms
	type checking 169ms
	typeclass inference 681ms
real 2.54
user 3.84
sys 0.59

LeanPool/RunsOfMultiples/LowerEstimates.lean

import took 902ms
cumulative profiling times:
	attribute application 0.0675ms
	congr simp thm 1.09ms
	elaboration 16.9ms
	fix level params 0.756ms
	import 902ms
	initialization 26.8ms
	instantiate metavars 1.26ms
	interpretation 526ms
	let-to-have transformation 0.0915ms
	linting 15.1ms
	module linting 0.0022ms
	norm_num 29.5ms
	overlappingInstancesLinter 2.81ms
	parsing 4.02ms
	process pre-definitions 7.1ms
	ring 59.6ms
	share common exprs 9.05ms
	simp 10.4ms
	tactic execution 62.8ms
	tacticAnalysis 14.5ms
	type checking 59.5ms
	typeclass inference 208ms
real 1.86
user 1.87
sys 0.54

LeanPool/RunsOfMultiples/Main.lean

import took 895ms
cumulative profiling times:
	attribute application 0.0164ms
	elaboration 7.36ms
	fix level params 0.0237ms
	import 895ms
	initialization 31ms
	instantiate metavars 0.0204ms
	interpretation 178ms
	let-to-have transformation 0.0295ms
	linting 2.58ms
	module linting 0.00228ms
	overlappingInstancesLinter 1.09ms
	parsing 1.4ms
	process pre-definitions 0.52ms
	share common exprs 0.0928ms
	tacticAnalysis 7.99ms
	type checking 0.387ms
	typeclass inference 4.9ms
real 1.60
user 1.09
sys 0.53

LeanPool/RunsOfMultiples/OneStep.lean

import took 721ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 130ms
cumulative profiling times:
	attribute application 0.0796ms
	congr simp thm 9.95ms
	elaboration 32.1ms
	fix level params 1.15ms
	import 721ms
	initialization 32.6ms
	instantiate metavars 3.26ms
	interpretation 956ms
	let-to-have transformation 0.123ms
	linting 32.6ms
	module linting 0.00571ms
	norm_num 141ms
	overlappingInstancesLinter 4.13ms
	parsing 10.9ms
	process pre-definitions 18.5ms
	ring 62.6ms
	share common exprs 15.6ms
	simp 140ms
	tactic execution 319ms
	tacticAnalysis 36ms
	type checking 129ms
	typeclass inference 571ms
real 2.31
user 3.20
sys 0.49

LeanPool/RunsOfMultiples/PrimeEstimates.lean

import took 887ms
cumulative profiling times:
	attribute application 0.0681ms
	congr simp thm 3.13ms
	elaboration 31.2ms
	fix level params 1.27ms
	import 887ms
	initialization 27.1ms
	instantiate metavars 7.68ms
	interpretation 939ms
	let-to-have transformation 0.0769ms
	linting 19.1ms
	module linting 0.00199ms
	norm_num 419ms
	overlappingInstancesLinter 4.39ms
	parsing 12.2ms
	process pre-definitions 26.2ms
	ring 116ms
	share common exprs 33.6ms
	simp 32.9ms
	tactic execution 370ms
	tacticAnalysis 46.9ms
	type checking 91.3ms
	typeclass inference 428ms
real 3.02
user 3.41
sys 0.58

LeanPool/RunsOfMultiples/PrimeInput.lean

import took 738ms
cumulative profiling times:
	attribute application 0.0196ms
	compilation (IR) 0.126ms
	compilation (LCNF base) 1.91ms
	compilation (LCNF impure) 0.618ms
	compilation (LCNF mono) 1ms
	elaboration 9.21ms
	fix level params 0.0239ms
	import 738ms
	initialization 26.7ms
	instantiate metavars 0.0104ms
	interpretation 152ms
	let-to-have transformation 0.0148ms
	linting 2.57ms
	module linting 0.00229ms
	overlappingInstancesLinter 1.6ms
	parsing 1.54ms
	process pre-definitions 0.252ms
	share common exprs 0.0247ms
	tacticAnalysis 3.23ms
	type checking 2.49ms
	typeclass inference 6.63ms
real 1.41
user 0.96
sys 0.48

LeanPool/RunsOfMultiples/Primes.lean

import took 866ms
cumulative profiling times:
	attribute application 0.0248ms
	elaboration 7.38ms
	fix level params 0.0443ms
	import 866ms
	initialization 26.6ms
	instantiate metavars 0.0735ms
	interpretation 184ms
	let-to-have transformation 0.0342ms
	linting 2.91ms
	module linting 0.00224ms
	norm_num 0.598ms
	overlappingInstancesLinter 1.51ms
	parsing 1.77ms
	process pre-definitions 0.548ms
	share common exprs 0.291ms
	tactic execution 7.64ms
	tacticAnalysis 5.44ms
	type checking 2.74ms
	typeclass inference 12.3ms
real 1.56
user 1.07
sys 0.54

LeanPool/RunsOfMultiples/Replication.lean

import took 475ms
cumulative profiling times:
	attribute application 0.0251ms
	congr simp thm 0.578ms
	elaboration 10.4ms
	fix level params 0.204ms
	import 475ms
	initialization 26.3ms
	instantiate metavars 1.04ms
	interpretation 152ms
	let-to-have transformation 0.044ms
	linting 12.5ms
	module linting 0.00222ms
	norm_num 0.324ms
	overlappingInstancesLinter 2.29ms
	parsing 4.14ms
	process pre-definitions 3.18ms
	ring 6.04ms
	share common exprs 2.82ms
	simp 13.4ms
	tactic execution 73.9ms
	tacticAnalysis 16.5ms
	type checking 32.9ms
	typeclass inference 40.5ms
real 1.24
user 0.92
sys 0.44

LeanPool/RunsOfMultiples/Upper.lean

import took 718ms
tactic execution of Mathlib.Tactic.nlinarith took 509ms
cumulative profiling times:
	attribute application 0.0841ms
	congr simp thm 6.15ms
	elaboration 56.6ms
	fix level params 1.64ms
	import 718ms
	initialization 26.8ms
	instantiate metavars 7.59ms
	interpretation 1.19s
	let-to-have transformation 0.16ms
	linting 63.9ms
	module linting 0.00207ms
	norm_num 298ms
	overlappingInstancesLinter 7.08ms
	parsing 21.4ms
	process pre-definitions 34.9ms
	ring 125ms
	share common exprs 29.5ms
	simp 109ms
	tactic execution 1.32s
	tacticAnalysis 90ms
	type checking 109ms
	typeclass inference 842ms
real 3.61
user 5.00
sys 0.53

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[Vilin97]

/review

Please review exact head eb39eb3cdbbda7b95097a9d7f149f69ac02348a9. Lean Action CI is running; its eventual result should be checked directly rather than assumed.

Pinned source: https://github.com/jas-ho/runs-of-multiples-lean/tree/8b7e5f23534c321722725f78b6e64981557f0ef5 . The root LICENSE is Apache-2.0, and the production account identifies Claude Opus 5.5 as author of both Lean proofs. Completed-code commit b5a952cd725aae012d046d4e83b85f89bdc3499a is dated 2026-10-09 08:21:13 UTC, inside the eligible interval [2026-10-02T09:15:20Z, 2026-10-09T09:15:20Z).

The PR description records the coherent dependency closure, mathematical fidelity, source variations, all-cardinalities lower bound, local trust/linter checks and measured optimization. Greptile has reviewed this exact head and found no actionable issue; its external-source limitations need direct source inspection. No CI gate, waiver or protected rollout branch is changed.

[Vilin97]

/profile

Refresh the advisory compile profile for final head eb39eb3cdbbda7b95097a9d7f149f69ac02348a9 after the four restricted-arithmetic edits. The earlier profile is preserved as a checkpoint; local baseline and both final clean-build measurements are in the PR description.

[Vilin97]

Separate acquisition-agent review of exact head eb39eb3cdbbda7b95097a9d7f149f69ac02348a9: APPROVE. All five current project-review rubrics pass, with no unresolved finding. This is the acquisition agent's thorough review after implementation, separate from the configured GPT worker; it is not represented as an independent human or second-agent approval.

I inspected the complete 24-file import diff, all 16 upstream Lean files in bounded reads, both endpoint declarations, both source write-ups' theorem/proof sections, the semantic port changes, and all five extracted modules. No elided source slice is relied on for this verdict.

• Faithfulness and trust: kVal_set_nonempty, kVal_not_mem and forall_mul_mem_iff identify the least positive missing multiplier for positive inputs. Both headline statements match upstream after whitespace normalization. The lower bound gives a set of exactly every sufficiently large cardinality. The upper proof's prime input and both positive-density lower blocks are proved. The 185 named source declarations passed the repository's axiom-closure audit; all 23 modules passed the option/backdoor audit. No forbidden mechanism or policy waiver was introduced.
• Sources, license and provenance: I read the pinned Apache-2.0 LICENSE and production account at upstream 8b7e5f23534c321722725f78b6e64981557f0ef5. Completed-code commit b5a952cd725aae012d046d4e83b85f89bdc3499a is dated October 9, 08:21:13 UTC, within this run's exact seven-day window. The account credits Claude Opus 5.5 for both Lean proofs and GPT-6-Astra for the informal compression proof; the import records AI provenance and retains publishing-owner attribution. The informal asymptotic statement matches both formal headlines. The upstream documents the Chebyshev-compatible interval/cutoff and padding variations; these preserve the claimed asymptotic order.
• Novelty and significance: Current-main cards/source/history and pool PR/issue searches found no selected repository, namespace or distinctive-term duplicate. Local pinned Mathlib and public Mathlib/TauCeti searches found no corresponding headline declaration. Shared prime, entropy and smooth-number vocabulary is not by itself a duplicate of this theorem. The matching bounds and two constructions are substantial, and the abstract chain-compression and generic block-transfer infrastructure are worth preserving. This does not assert a complete survey of informal mathematical literature.
• Engineering and measured cost: All 16 upstream proof/example modules form the retained coherent closure; no monorepo tools, PDFs or caches are vendored. The two routes share basic definitions, estimates and padding, as the card explicitly says. Five extracted modules remove serial prime/upper dependencies and let the lower constructions compile independently. A generic transfer lemma replaces duplicate ~131,000-heartbeat proofs with one ~36,695-heartbeat proof. Restricted arithmetic reduces many_primes from 199,588 to 35,165 allocation heartbeats, fibre_bound from 91,666 to 30,156, and upper_core from 35,801 to 12,483. Clean project build wall time was 35.64 seconds before optimization and 22.17 / 24.05 seconds for this final source, under the same command and cached pinned dependencies; these are individual shared-VM timings. Readability and theorem strength are preserved.
• Validation: Local warning-free clean builds, index/style checks, slow declaration linters (459 declarations), static quality, card/declaration validation and trust audits passed. Final-head Lean Action CI succeeded, including the warning-free project build, current-index check, slow declaration linters, style checks and repository quality audit. All currently reported check contexts passed or were skipped by their normal path scopes. Greptile reviewed this exact head with no actionable issue; the configured GPT review also approves this exact head with all five rubrics passing. Its initial CI-pending note records the state when that review began; final-head CI subsequently completed successfully. All required checks were green or normally scope-skipped and no review threads existed at native queue admission.

Structured rubric verdicts:

{
  "reviewed_head": "eb39eb3cdbbda7b95097a9d7f149f69ac02348a9",
  "diff_coverage": "complete: all 24 changed files and the coherent proof dependency closure",
  "overall_verdict": "approve",
  "faithfulness": {
    "verdict": "pass",
    "bottom_line": "Both headline declarations prove the matching extremal asymptotic bounds described by the card.",
    "proves_the_claim": "proves_it",
    "claim_note": "The upper bound holds for every sufficiently large positive finite set; a single positive lower constant works for some set of exactly each sufficiently large cardinality.",
    "assumed_inputs": "The headlines have no extra mathematical hypotheses. Positivity and sufficiently large cardinality are explicit. PrimeInput is discharged from Mathlib Chebyshev estimates; both lower-block hypotheses are constructed.",
    "findings": []
  },
  "novelty": {
    "verdict": "pass",
    "bottom_line": "No existing Mathlib, pooled or TauCeti formalization of either headline was found.",
    "already_formalized": "",
    "novelty_note": "Mathlib supplies Chebyshev and smooth-number ingredients; these do not already establish the uniform first-missing-multiple extremal bound. Repository, namespace and distinctive-term searches found no duplicate headline.",
    "findings": []
  },
  "significance": {
    "verdict": "pass",
    "bottom_line": "This is a substantial completed extremal number-theory project with useful entropy and compression infrastructure.",
    "fit": "good_fit",
    "level": "research",
    "branch": "extremal and analytic number theory",
    "mode": "mixed",
    "significance_one_sentence": "Two distinct arguments determine the sharp order n log n log log n, with abstract chain compression, entropy counting and all-cardinalities block transfer supporting later work.",
    "findings": []
  },
  "sources": {
    "verdict": "pass",
    "bottom_line": "The pinned upstream write-ups, completed source, Apache license and production account support the result, date and AI attribution.",
    "source_match": "matches",
    "findings": []
  },
  "quality": {
    "verdict": "pass",
    "bottom_line": "The dependency split, generic block-transfer theorem and restricted arithmetic preserve reusable generality while reducing measured build and elaboration work; some concrete Nat/Real bookkeeping remains.",
    "code_quality": 4,
    "findings": []
  }
}

[Vilin97]

🤖 LLM review (gpt-6.1-sol, 5 rubrics)

Reviewed head: eb39eb3cdbbda7b95097a9d7f149f69ac02348a9

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Both headlines match the card; exact-head CI build and lint steps passed, while repository quality checks remain pending (CI).
Novelty	✅ pass	Direct searches of pinned and current Mathlib and pool sources found no duplicate of either headline; the supplied semantic search report covers unrelated results and is unverifiable for this PR.
Significance	✅ pass	The two main theorems establish a research-level sharp extremal asymptotic, supported by substantial entropy and compression theory.
Sources	✅ pass	Both endpoint statements match the pinned upstream result, and the prior Lean formalization and separate informal compression proof are credited.
Code quality (advisory)	✅ pass	Concrete ChainSys implementations and the shared lower_bound_of_block transfer keep both routes maintainable; CI for this head now reports success, though I did not rebuild locally because dependencies are absent.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Only positivity and sufficiently large cardinality, as disclosed; primeInput discharges PrimeInput, exists_closed constructs the required closure, and block and Alt.block_alt supply the lower constructions.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	extremal number theory
Mode	theory_building
Code quality	4 / 5

Statement check: Both theorems prove a uniform eventual upper bound and a fixed positive matching lower bound witnessed by a set of exactly n positive integers for every sufficiently large n.

RunsOfMultiples.main_theorem and main_theorem_alt determine the extremal order n log n log log n for sums of first missing multiple indices, with constructions for every sufficiently large cardinality and supporting entropy, chain-compression, radical, and smooth-number results.

---

Tokens: 8,215,856 in / 40,396 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $33.4694 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Reviewed exact head eb39eb3cdbbda7b95097a9d7f149f69ac02348a9. The review covered all 24 added files, including both proof routes, shared estimates, examples and project card.

Both headlines faithfully formalize the sharp extremal order n log n log log n for finite sets of positive integers. The upper bound is uniform over sufficiently large sets; the positive lower bound supplies a set of every sufficiently large prescribed cardinality. The prime input is discharged from the imported estimates, and the compression route constructs its required closure properties. The lower constructions and shared dilation/padding argument preserve the multiple relations. Both pinned write-ups state this result and address every large cardinality: entropy proof, compression proof.

This is a substantial extremal number theory contribution with reusable entropy, compression and replication lemmas. AI provenance agrees with the pinned first-party disclosure; the upstream license is Apache-2.0. Finite official Mathlib/TauCeti searches found no concrete duplicate.

One nonblocking documentation correction: Alt/Lower.lean:280 should describe the m = 0 inequality as 1 ≤ 2. Its proof already handles that case correctly.

The source judgment is favorable at this exact head. Its project CI now reports success. The existing protected queue entry still needs its integration checks; this review neither replaces those checks nor creates another queue entry.