Repository navigation
Import sharp Graham–LPT scheduling bounds and equality cases - #694
Conversation
|
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 the reviewed changes. SummaryImports Graham’s scheduling bounds, tight examples, equality cases, and fixed-job-count supremum. The latest changes share prefix-sum proofs between real loads and integer counts and weights.
Reviews (5) · Last reviewed commit: "Share generic prefix sum identities acro..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Proof profile (new / modified Lean files)
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: 710,847 maxHeartbeats units across 19 valid files (3,915 added LOC). Sum of Count-heartbeats wall-clock total: 167.65 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.GrahamLPT.OptList |
17.00 s |
LeanPool.GrahamLPT.Certificates |
8.60 s |
LeanPool.GrahamLPT.Equality |
7.20 s |
LeanPool.GrahamLPT.Counter |
6.30 s |
LeanPool.GrahamLPT.Key |
6.20 s |
LeanPool.GrahamLPT.CoffmanSethi |
5.90 s |
LeanPool.GrahamLPT.TightLPT |
5.30 s |
LeanPool.GrahamLPT.FixedCount |
5.20 s |
LeanPool.GrahamLPT.LPTBound |
5.10 s |
LeanPool.GrahamLPT.TightList |
4.60 s |
LeanPool.GrahamLPT.GrahamScaled |
3.80 s |
LeanPool.GrahamLPT.ListOptimum |
3.70 s |
Per-file `lean --profile` output
LeanPool/GrahamLPT.lean
import took 1.32s
cumulative profiling times:
elaboration 0.373ms
import 1.32s
initialization 36.6ms
interpretation 134ms
linting 0.94ms
module linting 0.00176ms
overlappingInstancesLinter 1.07ms
parsing 0.0609ms
tacticAnalysis 2.24ms
real 2.21
user 0.93
sys 0.96
LeanPool/GrahamLPT/Basic.lean
import took 817ms
cumulative profiling times:
attribute application 0.415ms
compilation (IR) 0.0776ms
compilation (LCNF base) 0.68ms
compilation (LCNF impure) 0.373ms
compilation (LCNF mono) 0.557ms
congr simp thm 8.47ms
elaboration 117ms
fix level params 1.8ms
import 816ms
initialization 30.1ms
instantiate metavars 3.53ms
interpretation 431ms
let-to-have transformation 0.516ms
linting 44.1ms
module linting 0.00154ms
norm_num 0.261ms
overlappingInstancesLinter 13.9ms
parsing 34.5ms
process pre-definitions 18.5ms
ring 6.05ms
share common exprs 9.99ms
simp 238ms
tactic execution 259ms
tacticAnalysis 96.4ms
type checking 108ms
typeclass inference 592ms
real 2.22
user 2.65
sys 0.90
LeanPool/GrahamLPT/Certificates.lean
import took 802ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 189ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 193ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 246ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 256ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 246ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 175ms
cumulative profiling times:
attribute application 0.0909ms
congr simp thm 3.2ms
elaboration 66.6ms
fix level params 1.46ms
import 802ms
initialization 30.9ms
instantiate metavars 5.04ms
interpretation 1.95s
let-to-have transformation 0.192ms
linting 49.3ms
module linting 0.00145ms
norm_num 17.2ms
overlappingInstancesLinter 5.71ms
parsing 22.9ms
process pre-definitions 20.3ms
ring 113ms
share common exprs 23.8ms
simp 119ms
tactic execution 281ms
tacticAnalysis 59ms
type checking 117ms
typeclass inference 816ms
real 3.54
user 4.40
sys 0.88
LeanPool/GrahamLPT/CoffmanSethi.lean
import took 791ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 443ms
cumulative profiling times:
attribute application 0.16ms
compilation (IR) 0.145ms
compilation (LCNF base) 1.73ms
compilation (LCNF impure) 0.695ms
compilation (LCNF mono) 1.17ms
congr simp thm 5.21ms
elaboration 71.7ms
fix level params 1.8ms
import 791ms
initialization 31.1ms
instantiate metavars 6.28ms
interpretation 1.14s
let-to-have transformation 0.222ms
linting 56.3ms
module linting 0.0014ms
norm_num 73.2ms
overlappingInstancesLinter 8.37ms
parsing 33ms
process pre-definitions 20.5ms
ring 78.3ms
share common exprs 20.9ms
simp 218ms
tactic execution 505ms
tacticAnalysis 95.7ms
type checking 302ms
typeclass inference 884ms
real 2.86
user 4.19
sys 0.88
LeanPool/GrahamLPT/Counter.lean
import took 780ms
tactic execution of Lean.Parser.Tactic.omega took 162ms
tactic execution of Lean.Parser.Tactic.omega took 164ms
cumulative profiling times:
attribute application 0.112ms
congr simp thm 12ms
elaboration 50.4ms
fix level params 3.16ms
import 780ms
initialization 30.3ms
instantiate metavars 71ms
interpretation 1.66s
let-to-have transformation 0.216ms
linting 19.5ms
module linting 0.00148ms
norm_num 194ms
overlappingInstancesLinter 4.28ms
parsing 16.4ms
process pre-definitions 46.2ms
ring 7.17ms
share common exprs 26.8ms
simp 401ms
tactic execution 615ms
tacticAnalysis 48.4ms
type checking 265ms
typeclass inference 619ms
real 3.07
user 4.70
sys 0.88
LeanPool/GrahamLPT/Defs.lean
import took 776ms
cumulative profiling times:
attribute application 0.063ms
compilation (IR) 0.574ms
compilation (LCNF base) 11.6ms
compilation (LCNF impure) 2.7ms
compilation (LCNF mono) 5.13ms
elaboration 33ms
fix level params 0.0889ms
import 776ms
initialization 35.3ms
instantiate metavars 0.109ms
interpretation 194ms
let-to-have transformation 0.0958ms
linting 6.45ms
module linting 0.00139ms
overlappingInstancesLinter 3.82ms
parsing 5.7ms
process pre-definitions 4.16ms
share common exprs 0.455ms
tacticAnalysis 17ms
type checking 3.82ms
typeclass inference 36.6ms
real 1.74
user 1.04
sys 0.84
LeanPool/GrahamLPT/Equality.lean
import took 818ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 113ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 177ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 151ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 455ms
cumulative profiling times:
attribute application 0.342ms
blocked (unaccounted) 0.0618ms
congr simp thm 6.22ms
elaboration 224ms
fix level params 4.53ms
import 818ms
initialization 30.4ms
instantiate metavars 19.6ms
interpretation 2.38s
let-to-have transformation 0.787ms
linting 119ms
module linting 0.00156ms
norm_num 26.1ms
overlappingInstancesLinter 14.2ms
parsing 69.9ms
process pre-definitions 49.8ms
ring 224ms
share common exprs 66.5ms
simp 341ms
tactic execution 1.06s
tacticAnalysis 175ms
type checking 665ms
typeclass inference 1.69s
real 4.04
user 7.80
sys 0.89
LeanPool/GrahamLPT/FixedCount.lean
import took 806ms
cumulative profiling times:
attribute application 0.253ms
congr simp thm 3.23ms
elaboration 83.7ms
fix level params 1.62ms
import 806ms
initialization 30.3ms
instantiate metavars 4.99ms
interpretation 720ms
let-to-have transformation 0.372ms
linting 48.3ms
module linting 0.00139ms
norm_num 95.3ms
overlappingInstancesLinter 11.2ms
parsing 30ms
process pre-definitions 17.9ms
ring 69.9ms
share common exprs 18.1ms
simp 111ms
tactic execution 353ms
tacticAnalysis 81.6ms
type checking 247ms
typeclass inference 655ms
real 2.64
user 3.26
sys 0.86
LeanPool/GrahamLPT/GrahamScaled.lean
import took 800ms
cumulative profiling times:
attribute application 0.0798ms
congr simp thm 0.62ms
elaboration 27ms
fix level params 0.387ms
import 800ms
initialization 30.6ms
instantiate metavars 1.14ms
interpretation 212ms
let-to-have transformation 0.106ms
linting 12.6ms
module linting 0.00147ms
norm_num 0.677ms
overlappingInstancesLinter 4.62ms
parsing 9.52ms
process pre-definitions 4.33ms
ring 4.35ms
share common exprs 2.78ms
simp 9.81ms
tactic execution 86.4ms
tacticAnalysis 28ms
type checking 14.4ms
typeclass inference 62.4ms
real 1.84
user 1.20
sys 0.87
LeanPool/GrahamLPT/Imports.lean
import took 789ms
cumulative profiling times:
elaboration 0.0985ms
import 789ms
initialization 30.1ms
interpretation 117ms
linting 0.25ms
module linting 0.00196ms
overlappingInstancesLinter 0.105ms
parsing 0.00167ms
tacticAnalysis 0.419ms
real 1.67
user 0.87
sys 0.85
LeanPool/GrahamLPT/Key.lean
import took 789ms
cumulative profiling times:
attribute application 0.0626ms
blocked (unaccounted) 0.567ms
congr simp thm 1.88ms
elaboration 27.8ms
fix level params 0.67ms
import 789ms
initialization 31.1ms
instantiate metavars 3.31ms
interpretation 392ms
let-to-have transformation 0.0973ms
linting 30.9ms
module linting 0.00143ms
norm_num 0.985ms
overlappingInstancesLinter 9.47ms
parsing 19.6ms
process pre-definitions 7.36ms
ring 16.3ms
share common exprs 6.97ms
simp 75.6ms
tactic execution 254ms
tacticAnalysis 45.9ms
type checking 134ms
typeclass inference 328ms
real 2.58
user 2.08
sys 0.85
LeanPool/GrahamLPT/LPTBound.lean
import took 789ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 187ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 145ms
cumulative profiling times:
attribute application 0.0322ms
congr simp thm 1.15ms
elaboration 16.7ms
fix level params 0.519ms
import 789ms
initialization 38.1ms
instantiate metavars 1.24ms
interpretation 654ms
let-to-have transformation 0.0661ms
linting 14.3ms
module linting 0.0015ms
norm_num 45.5ms
overlappingInstancesLinter 3.15ms
parsing 4.42ms
process pre-definitions 4.35ms
ring 25.9ms
share common exprs 6.31ms
simp 10ms
tactic execution 69.6ms
tacticAnalysis 18.8ms
type checking 32.4ms
typeclass inference 205ms
real 2.32
user 1.85
sys 0.85
LeanPool/GrahamLPT/LPTForm.lean
import took 784ms
cumulative profiling times:
attribute application 0.0328ms
congr simp thm 0.565ms
elaboration 20.7ms
fix level params 0.211ms
import 784ms
initialization 30.5ms
instantiate metavars 0.521ms
interpretation 179ms
let-to-have transformation 0.0896ms
linting 7.19ms
module linting 0.00173ms
overlappingInstancesLinter 6.28ms
parsing 4.45ms
process pre-definitions 1.65ms
share common exprs 1.13ms
simp 9.01ms
tactic execution 29ms
tacticAnalysis 17.5ms
type checking 4.93ms
typeclass inference 77.6ms
real 1.75
user 1.07
sys 0.84
LeanPool/GrahamLPT/ListBound.lean
import took 789ms
cumulative profiling times:
attribute application 0.0328ms
congr simp thm 1.15ms
elaboration 15.7ms
fix level params 0.473ms
import 789ms
initialization 30.1ms
instantiate metavars 0.952ms
interpretation 327ms
let-to-have transformation 0.06ms
linting 10.9ms
module linting 0.00147ms
norm_num 25.2ms
overlappingInstancesLinter 4.01ms
parsing 3.4ms
process pre-definitions 3.67ms
ring 26.3ms
share common exprs 5.31ms
simp 9.54ms
tactic execution 40.9ms
tacticAnalysis 14.7ms
type checking 35.6ms
typeclass inference 100ms
real 1.87
user 1.33
sys 0.84
LeanPool/GrahamLPT/ListOptimum.lean
import took 816ms
cumulative profiling times:
attribute application 0.0637ms
congr simp thm 0.789ms
elaboration 34.4ms
fix level params 0.747ms
import 816ms
initialization 31.5ms
instantiate metavars 4.66ms
interpretation 436ms
let-to-have transformation 0.107ms
linting 27.1ms
module linting 0.00242ms
norm_num 1.9ms
overlappingInstancesLinter 8.02ms
parsing 15.1ms
process pre-definitions 8.87ms
ring 40ms
share common exprs 8.75ms
simp 38.3ms
tactic execution 176ms
tacticAnalysis 51.9ms
type checking 72.9ms
typeclass inference 159ms
real 2.03
user 1.81
sys 0.87
LeanPool/GrahamLPT/OptList.lean
import took 797ms
simp took 175ms
simp took 125ms
simp took 200ms
simp took 117ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_SplitIfs___elabRules_Mathlib_Tactic_splitIfs_1._boxed took 197ms
cumulative profiling times:
attribute application 0.152ms
compilation (IR) 0.33ms
compilation (LCNF base) 5.81ms
compilation (LCNF impure) 1.58ms
compilation (LCNF mono) 3.11ms
congr simp thm 56.5ms
elaboration 68.1ms
fix level params 2.92ms
import 797ms
initialization 29.9ms
instantiate metavars 23.9ms
interpretation 995ms
let-to-have transformation 0.232ms
linting 50.9ms
module linting 0.00151ms
norm_num 113ms
overlappingInstancesLinter 11.1ms
parsing 19.1ms
process pre-definitions 70.9ms
ring 84.3ms
share common exprs 35.9ms
simp 7.59s
tactic execution 2.4s
tacticAnalysis 124ms
type checking 2.2s
typeclass inference 1.97s
real 8.12
user 16.52
sys 0.92
LeanPool/GrahamLPT/Ratio.lean
import took 791ms
cumulative profiling times:
attribute application 0.0298ms
congr simp thm 0.529ms
elaboration 8.82ms
fix level params 0.365ms
import 791ms
initialization 30.8ms
instantiate metavars 0.973ms
interpretation 314ms
let-to-have transformation 0.0796ms
linting 5.34ms
module linting 0.00157ms
norm_num 70.9ms
overlappingInstancesLinter 2.52ms
parsing 5.2ms
process pre-definitions 3.57ms
ring 15.9ms
share common exprs 4.4ms
simp 10.4ms
tactic execution 43ms
tacticAnalysis 14.2ms
type checking 26.7ms
typeclass inference 115ms
real 1.94
user 1.35
sys 0.86
LeanPool/GrahamLPT/TightLPT.lean
import took 804ms
tactic execution of Lean.Parser.Tactic.omega took 202ms
tactic execution of Lean.Parser.Tactic.omega took 120ms
type checking took 122ms
cumulative profiling times:
attribute application 0.217ms
congr simp thm 5.53ms
dsimp 11.3ms
elaboration 83.2ms
fix level params 2.44ms
import 804ms
initialization 30.1ms
instantiate metavars 7.85ms
interpretation 867ms
let-to-have transformation 0.373ms
linting 46.6ms
module linting 0.00152ms
norm_num 76.4ms
overlappingInstancesLinter 9.04ms
parsing 32.3ms
process pre-definitions 23.2ms
ring 114ms
share common exprs 38.2ms
simp 280ms
tactic execution 1.29s
tacticAnalysis 77.1ms
type checking 1.09s
typeclass inference 1.28s
real 3.50
user 6.06
sys 0.86
LeanPool/GrahamLPT/TightList.lean
import took 798ms
cumulative profiling times:
attribute application 0.167ms
congr simp thm 4.76ms
elaboration 53ms
fix level params 1.12ms
import 798ms
initialization 30.1ms
instantiate metavars 3.18ms
interpretation 514ms
let-to-have transformation 0.248ms
linting 30ms
module linting 0.00152ms
norm_num 7.64ms
overlappingInstancesLinter 6.99ms
parsing 19.8ms
process pre-definitions 11.4ms
ring 50.8ms
share common exprs 11.9ms
simp 327ms
tactic execution 249ms
tacticAnalysis 55.6ms
type checking 160ms
typeclass inference 377ms
real 2.20
user 2.60
sys 0.85
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
|
/review Exact head: |
|
/review Exact head: |
|
{ |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent Source review — APPROVE at 616cc2dd4878920103867423b4b359c7e04d91e6.
{
"review": "Permanent reviewer — independent Source review",
"head_sha": "616cc2dd4878920103867423b4b359c7e04d91e6",
"conclusion": "approve",
"coverage": "All 20 current added files: the complete 17-module mathematical development, public entry and generated Imports, and project card. The original import and all 19 parent-to-child changes were checked against full source and complete native patches; both literal reuses and the deleted forwarding module were verified.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"bottom_line": "The sharp list/LPT factors, positive equality classification and fixed-count supremum match the actual scheduling model and disclosed hypotheses.",
"claim_note": "Jobs are finite real vectors and schedules are assignments to actual machines. List scheduling chooses a least-loaded machine at every prefix; LPT supplies a permutation making the lengths antitone and the same greedy relation. No approximation or optimality conclusion is assumed in those definitions. The bounds quantify every permitted tie breaking against every comparison assignment. Concrete unit/Graham assignments establish sharpness. Equality necessity derives the critical-job/equal-load structure and job multiplicities; sufficiency transports the actual tight family by positive scaling and permutation. The fixed-n proof uses positive epsilon-tail instances, proves OPT > 0 before division and constructs ratios above any proposed smaller upper bound.",
"assumed_inputs": "Nonzero machine count. The approximation factors require nonnegative processing times; schedule existence permits arbitrary real lengths. Positive equality classification additionally requires m >= 2, n > 0 and every job positive. The fixed-count IsLUB requires n >= 2m + 1 and positive jobs. Empty/zero instances are allowed in the nonnegative bound statements without dividing by their optimum.",
"findings": []
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"bottom_line": "The finite inspected library comparisons do not supply this scheduling theory.",
"novelty_note": "Compared the actual pinned Mathlib finite-extrema and finite-function-space contracts (Finset.le_sup', its infimum dual, Fintype.piFinset and Pi.instFintype), together with bounded scheduling/makespan/greedy searches in Mathlib, TauCeti and the current pool's project routing. These provide infrastructure or unrelated results rather than the imported sharp scheduling/equality theory. No matching development was identified within those scopes; this is not an exhaustive absence or first-formalization claim.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"branch": "approximation algorithms and scheduling",
"mode": "theory_building",
"bottom_line": "A substantial completed mathematical development suitable for the pool.",
"significance_one_sentence": "Two sharp universal approximation factors, all-tie tight witnesses, a positive equality classification and a fixed-job-count supremum are supported by reusable schedule existence, optimum attainment, permutation/scaling and critical-job/counting results.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"bottom_line": "Pinned upstream contracts, licensing, attribution and proof provenance support the import.",
"source_note": "Verified the pinned upstream MIT license and complete notice retained in the entry, JD Jones attribution and public AI disclosure. Completion commit d863c08b53520eab4e89fedec2776cb3d53c2061 (2026-10-11) contains the original 39 public contracts; the later pin preserves them and adds two explicit-order contracts. All 41 current public theorem headers match the pinned upstream contracts exactly; their proofs now live directly under the public names. Helper renames and the new proved restriction lemmas do not weaken the headline statements. Graham's 1969 Theorem 2 (printed p.421) states the sharp LPT factor for independent positive-duration jobs; the entry discloses the extension to zero lengths. Dósa's Theorem 2 and the inspected Della Croce–Scatamacchia propositions match the disclosed variants. The separate fixed-count IsLUB is expressly distinguished from Dósa's stronger Remark 1. Historical verification and author timing/compiled-audit claims have not been rerun.",
"findings": []
},
"code_quality": {
"verdict": "pass",
"code_quality": 3,
"bottom_line": "Competent structure with the concrete duplication finding addressed.",
"quality_note": "loadBefore_restrict proves equality of finite prefix sums, and IsListSchedule.restrict derives the inherited greedy relation. FixedCount identifies the retained prefix with grahamJobs and reuses the existing pairing/load proof. The pairing helper preserves its weaker 2m <= n domain; removing epsilon hypotheses strengthens only prefix results, while positivity and ordering assumptions remain where needed for the tail/LPT argument. The 41 forwarding contracts are removed in favor of the actual public proof producers, with all headline statement headers retained. Existing projects, LeanPool.lean, dependency pins and gates are unchanged.",
"findings": []
},
"validation": "This is exact-head Source acceptance at 616cc2d. The existing author-requested configured review and full applicable authored/native checks must still qualify before protected queue admission. Written-source checks do not certify the author's compiled 719-declaration audit or timings; the old-head profile is advisory and supplies no current-head or whole-CI credit.",
"resolved_findings": [
{
"thread": 4323909878,
"path": "LeanPool/GrahamLPT/FixedCount.lean",
"issue": "Repeated prefix-pairing and load-saturation proofs.",
"resolution": "The reviewed 616cc2d restriction lemmas and Graham-prefix transfer reuse the existing proof, preserving the weaker pairing-helper domain and the separate positive-tail analysis."
}
]
}
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All seven card headlines match the Lean; CI remains pending, and a Mathlib-fetch HTTP 403 prevented local build verification. |
| Novelty | ✅ pass |
No named duplicate of the seven headlines was found in the searched Mathlib, Tau Ceti, or pool sources; the exact-head CI build remains in progress. |
| Significance | ✅ pass |
The sharp bounds and extremal classification justify pooling this scheduling theory; CI remains pending, and a Mathlib-fetch HTTP 403 prevented local elaboration. |
| Sources | ✅ pass |
The Graham, Dósa and Della Croce–Scatamacchia sources support the attributed results, with scope differences labelled and upstream formalization credited; CI remains pending. |
| Code quality (advisory) | ✅ pass |
Competent modular Lean with shared prefix proofs; CI remains pending, and a Mathlib-fetch HTTP 403 prevented local elaboration. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Nonzero machines; nonnegative lengths for bounds and improvement; nonempty positive instances and at least two machines for classification; positive lengths and the stated job-count threshold for the supremum. These restrictions are disclosed. Schedule existence, attained optima, and tight witnesses are proved rather than assumed. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | approximation algorithms and scheduling |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The Lean proves both sharp bounds, the least LPT factor, classification up to positive scaling and job permutation, the fixed-count supremum, and the stated schedule existence and improvement results.
The least-factor theorems, positive-instance equality classification, and fixed-job-count ratio suprema develop a substantial theory around Graham’s scheduling bounds.
Faithfulness findings (1)
- prompt-injection — PR-wide
The contributor-owned acquisition comment supplies an approval conclusion and a prefilled faithfulness verdict, risking anchoring of the independent review. These assertions were disregarded; retain checkable evidence without proposed reviewer verdicts.
Evidence: prose only: the contributor-owned discussion in .review-pr.json contains "conclusion": "approve" and a faithfulness section containing "verdict": "pass".
Novelty findings (1)
- prompt-injection — PR-wide
The contributor-owned self-review embeds approval and a prefilled novelty verdict in the review evidence, risking anchoring of this independent review; those assertions were disregarded.
Evidence: .review-pr.json, comments[4].body contains "conclusion": "approve" and a novelty assessment with "verdict": "pass".
Significance findings (1)
- prompt-injection — PR-wide
The contributor-owned acquisition report supplies approval and a prefilled significance verdict, creating an anchoring risk for independent review. Remove proposed verdicts from reviewer evidence; these assertions were disregarded.
Evidence: The contributor report in .review-pr.json contains "conclusion": "approve" and a significance assessment containing "verdict": "pass" and "fit": "good_fit".
Sources findings (1)
- prompt-injection — PR-wide
The contributor-owned acquisition report supplies approval and a prefilled sources verdict, risking anchoring of the independent review. These claims were disregarded and the sources checked directly. Remove proposed reviewer verdicts from contributor evidence.
Evidence: The discussion in .review-pr.json contains a contributor-owned report with "conclusion": "approve" and a "sources" rubric containing "verdict": "pass" and "source_match": "matches".
Code quality findings (1)
- prompt-injection — PR-wide
The contributor-owned self-review supplies approval and a prefilled quality verdict, risking influence on the independent review; these claims were disregarded. Omit proposed reviewer verdicts from contributor evidence.
Evidence: The contributor-owned self-review in .review-pr.json contains "conclusion": "approve" and a "quality" section containing "verdict": "pass", "code_quality": 3, and "findings": [].
Tokens: 12,677,148 in / 44,447 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $51.3753 (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.
|
/review Exact head: |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent Source review — APPROVE at 8f733d0cf7694d9f1ffd2da511bd329c2a0e87f3.
{
"review": "Permanent reviewer — independent Source review",
"head_sha": "8f733d0cf7694d9f1ffd2da511bd329c2a0e87f3",
"conclusion": "approve",
"coverage": "All 20 current added files bound by complete Git blobs and native patches. Independently reviewed all five 616cc2d→8f733d0 file deltas (17 hunks, 29 additions/78 deletions), verified 15 literal parent reuses, all 41 intended public statement headers, and the current project/pool/root Merkle and import graph. The earlier full mathematical/provenance review is retained only after this explicit current-source preservation check.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"bottom_line": "The scheduling model, hypotheses and headline theorem types are preserved; nine original proofs now directly produce their existing descriptive public theorems.",
"claim_note": "Jobs are finite real vectors and schedules are assignments to actual machines. List scheduling chooses a least-loaded machine at every prefix; LPT supplies a permutation making the lengths antitone and the same greedy relation. No approximation or optimality conclusion is assumed in those definitions. The bounds quantify every permitted tie breaking against every comparison assignment. Concrete unit/Graham assignments establish sharpness. Equality necessity derives the critical-job/equal-load structure and job multiplicities; sufficiency transports the actual tight family by positive scaling and permutation. The fixed-n proof uses positive epsilon-tail instances, proves OPT > 0 before division and constructs ratios above any proposed smaller upper bound. The current child only consolidates nine producer/forwarder pairs. Each full original proof command survives under the descriptive name, with internal references renamed; no additional theorem premise, scheduling condition or arithmetic step is introduced.",
"assumed_inputs": "Nonzero machine count. The approximation factors require nonnegative processing times; schedule existence permits arbitrary real lengths. Positive equality classification additionally requires m >= 2, n > 0 and every job positive. The fixed-count IsLUB requires n >= 2m + 1 and positive jobs. Empty/zero instances are allowed in the nonnegative bound statements without dividing by their optimum.",
"findings": []
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"bottom_line": "The finite inspected library comparisons do not supply this scheduling theory.",
"novelty_note": "The project card, mathematical scope, dependency pins and all 41 intended public statement headers are unchanged by the inspected child. The prior bounded Mathlib/TauCeti/current-pool contract comparison therefore remains applicable to the same theory; no exhaustive absence or first-formalization claim is made.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"branch": "approximation algorithms and scheduling",
"mode": "theory_building",
"bottom_line": "A substantial completed mathematical development suitable for the pool.",
"significance_one_sentence": "Two sharp universal approximation factors, all-tie tight witnesses, a positive equality classification and a fixed-job-count supremum are supported by reusable schedule existence, optimum attainment, permutation/scaling and critical-job/counting results.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"bottom_line": "Pinned upstream contracts, licensing, attribution and proof provenance support the import.",
"source_note": "The MIT notice, attribution, AI provenance, pinned upstream source and paper distinctions are literal parent reuses. All 41 intended public theorem headers still match the previously verified pinned-upstream contracts. The nine eliminated prefixed helper names are consolidated into existing descriptive public names, retaining their original proofs. This changes the unmerged helper-name surface, not the mathematical statements or the declared project API. The prior Graham/Dósa/Della Croce–Scatamacchia source checks remain applicable to these unchanged contracts.",
"findings": []
},
"code_quality": {
"verdict": "pass",
"code_quality": 3,
"bottom_line": "The nine residual duplicate theorem forwarders are removed without changing the mathematics.",
"quality_note": "In Basic, CoffmanSethi, Counter and ListOptimum, each original proof is renamed at its earlier producer position and the later public forwarder is deleted. GrahamScaled and all other actual consumers use the descriptive name. The five entire code-token streams equal the parent after exactly those nine forwarder removals and nine identifier substitutions; 13,635 surviving noncomment tokens and all 69 surviving declarations in the changed files are preserved under that map. There are 193 written declarations project-wide, with no stale helper references. Module/public-exposure controls, imports, definitions, assumptions, options, project card, other projects, dependency pins and gates are unchanged.",
"findings": []
},
"validation": "Exact-head Source acceptance only. Protected admission requires the matching current configured result and complete applicable authored/native CI. The current proper authored run is 39413790459 (core 118598182713); no green result is inferred from cancelled616c CI, the earlier configured2232 result, or the author's local compiled710-declaration/linter/timing claims. No local Lean compiler or benchmark was run by this Source review.",
"resolved_findings": [
{
"thread": 4323909878,
"path": "LeanPool/GrahamLPT/FixedCount.lean",
"issue": "Repeated prefix-pairing and load-saturation proofs.",
"resolution": "The reviewed 616cc2d restriction lemmas and Graham-prefix transfer reuse the existing proof, preserving the weaker pairing-helper domain and the separate positive-tail analysis."
},
{
"comment": 6289494467,
"issue": "Nine exported helper/public theorem pairs with duplicate statements.",
"resolution": "The five-file 8f733d0 delta moves the original proofs under the existing descriptive public names, removes the nine forwarders and updates every actual helper consumer. All 41 intended public statement headers remain identical; nine unmerged prefixed helper names are deliberately removed."
}
]
}
|
/review Exact head: |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent Source review — APPROVE at ad9d5db168ec7a59aea3f8d07065068b03aa2ce5.
{
"review": "Permanent reviewer — independent Source review",
"head_sha": "ad9d5db168ec7a59aea3f8d07065068b03aa2ce5",
"conclusion": "approve",
"coverage": "All20 current added files bound by full Git blobs/native patches; complete8f733d0→ad9d5db two-file delta (5hunks,54additions/96deletions),18literal parentreuses,all193 existing named headers/all41 intended pinned-public contracts and currentproject/pool/rootMerkles/importDAG verified. Prior full mathematics/provenance applies only after this explicit current-source preservation check.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"bottom_line": "All scheduling models, hypotheses and headline theorem types survive; the padded-family optimum proof now reuses the existing optimal witness through a proved finite tail-load bound.",
"claim_note": "Jobs are finite real vectors and schedules are assignments to actual machines. List scheduling chooses a least-loaded machine at every prefix; LPT supplies a permutation making the lengths antitone and the same greedy relation. No approximation or optimality conclusion is assumed in those definitions. The bounds quantify every permitted tie breaking against every comparison assignment. Concrete unit/Graham assignments establish sharpness. Equality necessity derives the critical-job/equal-load structure and job multiplicities; sufficiency transports the actual tight family by positive scaling and permutation. The fixed-n proof uses positive epsilon-tail instances, proves OPT > 0 before division and constructs ratios above any proposed smaller upper bound. The new generic lemma bounds each full machine load by its prefix load plus n*epsilon, assuming only epsilon>=0 and that each later job is at most epsilon. Its pointwise finite-sum proof handles arbitrary signed prefix lengths and any cutoff. The padded-family proof obtains the proved Graham optimal witness, extends it by machine zero, proves exact restricted prefix loads3m and uses the new tail bound. The existing fc_le_len also reuses the actual Graham job-length lower bound. Both changed existing theorems retain exactly their previous assumptions and conclusions; no scheduling result is inserted as an assumption.",
"assumed_inputs": "Nonzero machine count. The approximation factors require nonnegative processing times; schedule existence permits arbitrary real lengths. Positive equality classification additionally requires m >= 2, n > 0 and every job positive. The fixed-count IsLUB requires n >= 2m + 1 and positive jobs. Empty/zero instances are allowed in the nonnegative bound statements without dividing by their optimum.",
"findings": []
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"bottom_line": "The finite inspected library comparisons do not supply this scheduling theory.",
"novelty_note": "The card, pinned dependencies and all41 intended public contracts are literal-preserved by the inspected child. The prior bounded Mathlib/Tau Ceti/current-pool comparison remains applicable to those same headline results; the extra generic helper is supporting infrastructure, with no first-formalization or exhaustive absence claim.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"branch": "approximation algorithms and scheduling",
"mode": "theory_building",
"bottom_line": "A substantial completed mathematical development suitable for the pool.",
"significance_one_sentence": "Two sharp universal approximation factors, all-tie tight witnesses, a positive equality classification and a fixed-job-count supremum are supported by reusable schedule existence, optimum attainment, permutation/scaling and critical-job/counting results.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"bottom_line": "Pinned upstream contracts, licensing, attribution and proof provenance support the import.",
"source_note": "The pinned upstream/source citations, MIT notice, attribution, AI provenance, card and entry are literal parent files. All193 existing named declaration headers and all41 intended published upstream signatures are preserved. The prior Graham/Dósa/Della Croce–Scatamacchia source distinctions remain applicable to these unchanged contracts, including the separately proved fixed-count supremum. No contributor self-review or prior-verdict prose supplies independent authority.",
"findings": []
},
"code_quality": {
"verdict": "pass",
"code_quality": 3,
"bottom_line": "The duplicated padded-family optimal assignment proof is replaced by the existing witness and a reusable finite tail-load estimate.",
"quality_note": "Only Basic and FixedCount change. One new proved helper is added; fc_le_len and fc_exists_opt are the only changed existing proof bodies. The two padded-prefix lemmas move earlier with their complete original commands; the other191 old commands, every existing header, imports/exposure/options/definitions and18other files are preserved. There are194 written named declarations after excluding comments. The old machine-fiber/pairing construction is absent from fc_exists_opt. Current total3951Lean lines/4008total lines; no waiver, dependency pin, workflow or gate change.",
"findings": []
},
"validation": "Source acceptance at this exacthead only. Current authored run39418314780/suite106814557484/attempt1 had only livePlan118613178058 and no assigned Buildpool/core in the actual initial completejoblist. Complete applicable authored/native checks and a matching configured result remain required. Currentownerrequest6290265229 already exists; do not duplicate. Old8fSource5584407501/configured2233 and dated8fCI are historical, with no green or acceptance transfer. No local Lean compiler/kernel/benchmark was run; contributor compiled681/linter/timing claims are not adopted.",
"resolved_findings": [
{
"comment": 6289494467,
"configured_job": 2233,
"reviewed_parent": "8f733d0cf7694d9f1ffd2da511bd329c2a0e87f3",
"issue": "fc_exists_opt duplicated the Graham optimal assignment and machine-fiber construction.",
"resolution": "Atad9d, the actual proof calls tg_exists_opt, extends its witness, transports the exact prefix loads through restriction equalities and applies the proved general tail bound. No copied machine-fiber proof remains."
},
{
"scope": "PR-wide provenance/anchoring advisory",
"resolution": "Current contributor text labels its acquisition self-review separately. Independent mathematics/source judgments above use actual pinned code, contracts and references; contributor approval prose receives no authority."
}
]
}
|
/review Exact head: |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent Source review — APPROVE at 3fa7de32378bfd36c36a85a7e3f75934e4f20350.
{
"review": "Permanent reviewer — independent Source review",
"head_sha": "3fa7de32378bfd36c36a85a7e3f75934e4f20350",
"conclusion": "approve",
"coverage": "All20 current files verified by completeGitblobs/modes, all20currentmain-added nativepatch forward/inverse roundtrips, completead9d→3fa7 two-file delta (7hunks,39additions/75deletions),18literalparentfiles and project/pool/rootMerkles/importDAG. All41 intended pinned-public signatures remain exact; all194 written contracts agree under the explicit cs_sum_succ→sum_prefix_succ and cs_sum_fiber→sum_prefix_fiber helper renames. The common192 names keep their headers.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"bottom_line": "The scheduling results and hypotheses are unchanged; generic prefix identities now support both real loads and integer weights/counts.",
"claim_note": "The actual generic recurrence sums f over jobs with index below k+1 on machine i. Its finite pointwise proof isolates j=k and then the two Nat cutoff cases for j≠k; AddCommMonoid is sufficient, with no order, positivity or nonzero-machine assumption. The generic fiber identity exchanges finite sums and counts each job at its unique assigned machine, for any cutoff including0 and beyondn. The real load recurrence and prefix total specialize those identities by definitional reduction. bs_sum_load obtains the full total using the exact cutoff n and each Fin index's bound. Integer floor-weight and count recurrences and both fiber-sum bounds in CoffmanSethi use the same generic producers; their statements and hypotheses remain fixed. All scheduling model definitions, sharpness/equality/fixed-count contracts, constructive witnesses and eighteen other files are literal parent content after the full preservation check. No conclusion is inserted as an assumption, and zero/empty instances introduce no division.",
"assumed_inputs": "Nonzero machine count. The approximation factors require nonnegative processing times; schedule existence permits arbitrary real lengths. Positive equality classification additionally requires m >= 2, n > 0 and every job positive. The fixed-count IsLUB requires n >= 2m + 1 and positive jobs. Empty/zero instances are allowed in the nonnegative bound statements without dividing by their optimum.",
"findings": []
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"bottom_line": "The finite inspected library comparisons do not supply this scheduling theory.",
"novelty_note": "The card, dependencies and all41 intended public contracts remain unchanged. Prior bounded Mathlib/Tau Ceti/currentpool comparisons apply to those exact same scheduling statements; generic prefix-sum support carries no independent first-formalization or exhaustive absence claim.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"branch": "approximation algorithms and scheduling",
"mode": "theory_building",
"bottom_line": "A substantial completed mathematical development suitable for the pool.",
"significance_one_sentence": "Two sharp universal approximation factors, all-tie tight witnesses, a positive equality classification and a fixed-job-count supremum are supported by reusable schedule existence, optimum attainment, permutation/scaling and critical-job/counting results.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"bottom_line": "Pinned upstream contracts, licensing, attribution and proof provenance support the import.",
"source_note": "The pinned upstream/source citations, MIT notice, attribution, AI provenance, card and entry are literal parent files. All41 intended published upstream signatures remain exact. The two explicitly renamed generic prefix helpers retain their types, and the other192 written headers remain fixed. Prior Graham/Dósa/Della Croce–Scatamacchia source distinctions continue to apply, including the separately proved fixed-count supremum. Contributor verdicts and local compiler/timing claims supply no independent authority.",
"findings": []
},
"code_quality": {
"verdict": "pass",
"code_quality": 3,
"bottom_line": "The generic and real-valued prefix-sum proofs now share one implementation in Basic.",
"quality_note": "Basic defines sum_prefix_succ and sum_prefix_fiber; real load identities specialize them, and CoffmanSethi reuses them for integer counts/floor-weights. The duplicated cs_sum_succ/cs_sum_fiber bodies are removed and four downstream references are updated. The two helper renames are explicit rather than a claim that all names were preserved. Existing changed proof commands are bs_loadBefore_succ, bs_sum_loadBefore, bs_sum_load, cs_inv_all and lpt_job_position_le; all other retained commands and every retained header are fixed. Completecurrent source is3915Lean lines/3972total with194written named declarations. Imports, exposure, options, definitions, projectcard, pins and gates are unchanged. No waiver is added.",
"findings": []
},
"validation": "Source acceptance at this exacthead only. Proper authored run39423878557/suite106829965340/attempt1/core118631819414 is live; allfive mandatory stages were pending at the initial completefive-job capture. Existing matching configuredrequest6291051860 is pending and must not be duplicated. Oldad9 Source5584733940/configured2234 are historical; its cancelled CI39418314780 provides no current validation. Complete applicable authored/native checks and currentconfigured result remain required before normalqueue admission. No local Lean compiler/kernel/benchmark was run here; author676compiled-declaration counts and timing/heartbeat claims are attributed only.",
"resolved_findings": [
{
"comment": 6289494467,
"configured_job": 2234,
"reviewed_parent": "ad9d5db168ec7a59aea3f8d07065068b03aa2ce5",
"issue": "Generic prefix recurrence and fiber identities in CoffmanSethi duplicate real-valued Basic proofs.",
"resolution": "At3fa7, both generic producers live in Basic; real load proofs specialize them and integer weight/count consumers reuse them. Completeactual changed bodies and consumers independently reviewed; the advisory is addressed in source, with hosted elaboration still pending."
}
]
}
1 participant
Adds a self-contained theory of identical-machine scheduling: Graham's sharp
2 - 1/mlist-scheduling and4/3 - 1/(3m)LPT bounds, explicit tight instances, Dósa's classification of all positive tight instances, and the LPT-ratio supremum at every fixed job countn ≥ 2m + 1. The definitions quantify over arbitrary real job lengths and every allowed tie breaking; the existence, scaling, relabeling, critical-job and optimality results provide reusable scheduling infrastructure.Upstream is JD-Jones-ASES/graham-lpt-lean, pinned to
c8ed035b407cc554faf4b68df0cf3edc70058977. Its MIT license and JD Jones's copyright notice are retained in the entry module. Provenance isAI: the upstream disclosure says JD Jones directed the work, Claude wrote the development, and GPT supplied a pre-submission consultation. No independent human review is claimed.This acquisition uses the eligible interval [2026-08-20 09:45:10 UTC, 2026-10-13 09:45:10 UTC). Eligibility rests on material completion, rather than a repository refresh: checkpoint d863c08b5352 is dated 2026-10-11 18:57:04 UTC and records the completed 39-theorem development and successful verification. GitHub's public event feed records the repository public at 2026-10-11 16:02:53 UTC and the completed checkpoint pushed at 2026-10-11 18:57:07 UTC, corroborating the commit time. The imported latest revision also includes the subsequent explicit-order and documentation repairs, bringing the named contracts to 41.
The import contains all 17 mathematical modules and the proved named contracts. It omits the open challenge copy, redundant umbrella, test/audit programs, generators and registry tooling. One YAML card and the generated public
Imports.leanregister the project;LeanPool.leanis unchanged. All 41 published theorem signatures match upstream exactly. Their proofs now live directly under the public names instead of 50 redundant forwarding/helper declarations. Eleven helper definitions were renamed for Mathlib compatibility, and the prefix-restriction refactor strengthens helper statements by dropping unnecessary hypotheses. No theorem has been weakened.Port and optimization work:
v4.35.0-rc2to the pool's exactv4.35.0-rc3pins (Mathlibc55e6e786f49471c72fbddbec5415808896aec1e).OptList → TightLPTdependency and the redundant umbrella module.show/changewarnings, a proof-focus warning, and eleven helper-definition naming errors, without suppressions.Controlled project rebuilds used the same Azure VM, exact dependency checkouts, prebuilt dependencies, and
/usr/bin/time -v lake build LeanPool.GrahamLPT, deleting only this project's generated artifacts before each run. Other VM workloads were present, so these are observed samples, not a hardware-independent guarantee.The two final clean samples reduce wall time by 42.1–42.2% (about 1.73×) and maximum process RSS by 64.9–65.1%. They received 182–190% CPU, compared with 252% for the preceding 22.47-second sample; shared-VM load limits per-edit wall-time attribution. Summed synchronous command-profile heartbeat counts for Basic and CoffmanSethi fall from 71,719,805 to 65,773,810 (8.3%) after the generic consolidation, measured against the same built imports. Total process CPU time falls from the initial port's 127.32 seconds to 61.47–64.09 seconds in the final clean samples. Per-file timings and declaration profiles identified
FixedCountandOptList; the optimization preserves all mathematical generality. Logs and the upstream/signature comparison are retained in the acquisition workspace.Local validation:
lake exe mk_all --module --checkand Mathlib text style checks.Final-source Lean Action CI is successful: full-pool build and warning check, declaration linters, text style and repository quality all pass. All other required contexts pass or are correctly scoped out for this content-only diff. Independent review comments remain separate from this source and validation description. Merge uses the repository's protected native queue.