Repository navigation
Conversation
Import the formalization of Ruzsa, "Sum of sets in several dimensions" (Combinatorica 14 (1994), doi:10.1007/BF01302969), from gdahia/SumOfSetsInSeveralDimensions at bd2694b: the lower bound |A + B| ≥ |A| + Σ min(d, |A| - t) for sumsets of affine dimension d in R^D, its sharpness (Theorem 2), the asymmetric Freiman lemma, and bounds on the Freiman dimension of sets of small doubling. The library moves under LeanPool.SumOfSetsInSeveralDimensions with its imports rewritten, and the unused [DecidableEq G] arguments of freimanModelDim, freimanDim and three lemmas about them are dropped for the unused-arguments linter. The Palomar Challenge and Solution modules are left out, since Solution only restates the library theorems. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] The targeted repair fixes the reported mismatch; no blocking code issue remains. SummaryImports Ruzsa’s sumset bounds, sharpness results, and Freiman dimension bounds.
Reviews (2) · Last reviewed commit: "Update LeanPool/projects/sum-of-sets-in-..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com>
|
/review |
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: 828,293 maxHeartbeats units across 14 valid files (1,906 added LOC). Sum of Count-heartbeats wall-clock total: 117.04 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.SumOfSetsInSeveralDimensions.GeometricDeletion |
5.60 s |
LeanPool.SumOfSetsInSeveralDimensions.LowerBoundValues |
4.20 s |
LeanPool.SumOfSetsInSeveralDimensions.AffineDim |
3.50 s |
LeanPool.SumOfSetsInSeveralDimensions.FreimanDimensionSumsetBounds |
3.40 s |
LeanPool.SumOfSetsInSeveralDimensions.AffineDimSumset |
3.30 s |
LeanPool.SumOfSetsInSeveralDimensions.LowerBoundFunction |
3.10 s |
LeanPool.SumOfSetsInSeveralDimensions.LowerBound |
3.10 s |
LeanPool.SumOfSetsInSeveralDimensions.Construction |
3.00 s |
LeanPool.SumOfSetsInSeveralDimensions.Normalize |
2.60 s |
LeanPool.SumOfSetsInSeveralDimensions.FreimanDimension |
2.30 s |
LeanPool.SumOfSetsInSeveralDimensions.ClosedForm |
1.90 s |
LeanPool.SumOfSetsInSeveralDimensions.MinCardAdd |
1.00 s |
Per-file `lean --profile` output
LeanPool/SumOfSetsInSeveralDimensions.lean
import took 1.62s
cumulative profiling times:
declTypeLinter 0.752ms
elaboration 0.394ms
import 1.62s
initialization 37.5ms
interpretation 134ms
linting 0.697ms
module linting 0.0116ms
parsing 0.0541ms
tacticAnalysis 1.04ms
real 2.49
user 0.91
sys 0.96
LeanPool/SumOfSetsInSeveralDimensions/AffineDim.lean
import took 1.21s
cumulative profiling times:
attribute application 2.1ms
congr simp thm 1.46ms
declTypeLinter 4.54ms
elaboration 38.1ms
fix level params 0.42ms
grind 3.61ms
grind mark subsingleton 0.135ms
grind simp 1.02ms
import 1.21s
initialization 36.2ms
instantiate metavars 0.492ms
interpretation 221ms
let-to-have transformation 0.198ms
linting 10.3ms
module linting 0.0139ms
parsing 7.47ms
process pre-definitions 4.15ms
share common exprs 2.3ms
simp 48.5ms
sym canon 0.834ms
sym typeclass inference 5.67ms
tactic execution 57.8ms
tacticAnalysis 4.78ms
type checking 48.1ms
typeclass inference 153ms
real 2.30
user 1.54
sys 0.92
LeanPool/SumOfSetsInSeveralDimensions/AffineDimSumset.lean
import took 951ms
cumulative profiling times:
attribute application 0.0531ms
congr simp thm 1.2ms
declTypeLinter 5.73ms
elaboration 24.7ms
fix level params 0.322ms
import 951ms
initialization 33.5ms
instantiate metavars 0.609ms
interpretation 202ms
let-to-have transformation 0.0804ms
linting 9.52ms
module linting 0.0131ms
parsing 5.23ms
process pre-definitions 2.18ms
share common exprs 1.45ms
simp 52ms
tactic execution 98.4ms
tacticAnalysis 2.66ms
type checking 40.4ms
typeclass inference 104ms
real 2.05
user 1.35
sys 0.91
LeanPool/SumOfSetsInSeveralDimensions/ClosedForm.lean
import took 864ms
cumulative profiling times:
attribute application 0.127ms
congr simp thm 3.07ms
declTypeLinter 3.98ms
elaboration 58.2ms
fix level params 0.52ms
grind 111ms
grind ac 0.154ms
grind cutsat 5.36ms
grind ematch 8.37ms
grind linarith 0.0145ms
grind mark subsingleton 13.9ms
grind ring 0.525ms
grind simp 93.1ms
import 864ms
initialization 31.7ms
instantiate metavars 1.93ms
interpretation 255ms
let-to-have transformation 0.238ms
linting 14.5ms
module linting 0.0142ms
norm_num 13.4ms
parsing 8.71ms
process pre-definitions 3.8ms
ring 7.83ms
share common exprs 3.98ms
simp 39.1ms
sym canon 20.1ms
sym typeclass inference 126ms
tactic execution 83.2ms
tacticAnalysis 5.34ms
type checking 212ms
typeclass inference 196ms
real 2.12
user 2.04
sys 0.88
LeanPool/SumOfSetsInSeveralDimensions/Construction.lean
import took 951ms
sym typeclass inference of Lean.Grind.IsCharP took 148ms
sym typeclass inference of Lean.Grind.OrderedRing took 146ms
sym typeclass inference of Lean.Grind.IsCharP took 155ms
sym typeclass inference of Lean.Grind.OrderedRing took 141ms
grind took 139ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 258ms
cumulative profiling times:
attribute application 0.205ms
blocked (unaccounted) 0.855ms
congr simp thm 11.8ms
declTypeLinter 8.99ms
elaboration 73.5ms
fix level params 1.87ms
grind 267ms
grind ac 0.3ms
grind cutsat 57.6ms
grind ematch 46.9ms
grind linarith 0.198ms
grind mark subsingleton 27ms
grind ring 18.9ms
grind simp 119ms
import 951ms
initialization 32ms
instantiate metavars 6.11ms
interpretation 569ms
let-to-have transformation 0.373ms
linting 46.8ms
module linting 0.0108ms
norm_num 2.92ms
parsing 18.1ms
process pre-definitions 13.1ms
ring 18.2ms
share common exprs 12.7ms
simp 187ms
sym canon 30.4ms
sym typeclass inference 1.02s
tactic execution 402ms
tacticAnalysis 8.35ms
type checking 248ms
typeclass inference 604ms
real 3.06
user 4.63
sys 0.90
LeanPool/SumOfSetsInSeveralDimensions/FreimanDimension.lean
import took 808ms
cumulative profiling times:
attribute application 0.0411ms
compilation (IR) 0.161ms
compilation (LCNF base) 4.18ms
compilation (LCNF impure) 0.753ms
compilation (LCNF mono) 1.2ms
congr simp thm 0.458ms
declTypeLinter 7.34ms
elaboration 10.9ms
fix level params 0.117ms
grind 7.67ms
grind mark subsingleton 0.68ms
grind simp 3.65ms
import 808ms
initialization 31.6ms
instantiate metavars 0.177ms
interpretation 174ms
let-to-have transformation 0.0373ms
linting 4.45ms
module linting 0.0145ms
parsing 3.23ms
process pre-definitions 1.17ms
share common exprs 0.286ms
sym canon 1.32ms
sym typeclass inference 8.43ms
tactic execution 8.42ms
tacticAnalysis 3.37ms
type checking 9.37ms
typeclass inference 16.1ms
real 1.76
user 1.01
sys 0.85
LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean
import took 955ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 154ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 171ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 131ms
cumulative profiling times:
attribute application 0.275ms
congr simp thm 15.7ms
declTypeLinter 17.1ms
elaboration 151ms
fix level params 3.95ms
grind 175ms
grind ac 0.366ms
grind cutsat 10.1ms
grind ematch 34.6ms
grind linarith 0.0629ms
grind mark subsingleton 19.8ms
grind ring 2.26ms
grind simp 113ms
import 955ms
initialization 31.9ms
instantiate metavars 6.7ms
interpretation 1.08s
let-to-have transformation 0.538ms
linting 47ms
module linting 0.014ms
norm_num 46.3ms
parsing 27.4ms
process pre-definitions 21.5ms
ring 81ms
share common exprs 25.8ms
simp 290ms
sym canon 24.6ms
sym typeclass inference 354ms
tactic execution 300ms
tacticAnalysis 9.62ms
type checking 334ms
typeclass inference 1.16s
real 3.07
user 5.15
sys 0.95
LeanPool/SumOfSetsInSeveralDimensions/GeometricDeletion.lean
import took 966ms
sym typeclass inference of Lean.Grind.IsCharP took 170ms
sym typeclass inference of Lean.Grind.OrderedRing took 144ms
sym typeclass inference of Lean.Grind.IsCharP took 156ms
sym typeclass inference of Lean.Grind.OrderedRing took 155ms
sym typeclass inference of Lean.Grind.IsCharP took 161ms
sym typeclass inference of Lean.Grind.OrderedRing took 146ms
sym typeclass inference of Lean.Grind.IsCharP took 154ms
sym typeclass inference of Lean.Grind.OrderedRing took 148ms
sym typeclass inference of Lean.Grind.IsCharP took 153ms
sym typeclass inference of Lean.Grind.OrderedRing took 156ms
sym typeclass inference of Lean.Grind.IsCharP took 161ms
sym typeclass inference of Lean.Grind.IsCharP took 120ms
cumulative profiling times:
attribute application 0.31ms
congr simp thm 9.51ms
declTypeLinter 10.8ms
elaboration 220ms
fix level params 2.56ms
grind 271ms
grind ac 0.148ms
grind cutsat 1.02ms
grind ematch 8.35ms
grind linarith 0.0839ms
grind mark subsingleton 31.8ms
grind ring 0.166ms
grind simp 101ms
import 966ms
initialization 31.5ms
instantiate metavars 6.63ms
interpretation 418ms
let-to-have transformation 0.946ms
linting 83.7ms
module linting 0.0127ms
norm_num 10.1ms
parsing 31ms
process pre-definitions 19.4ms
share common exprs 14.7ms
simp 315ms
sym canon 42.3ms
sym typeclass inference 4.77s
tactic execution 905ms
tacticAnalysis 12.1ms
type checking 413ms
typeclass inference 1.43s
real 5.66
user 9.91
sys 0.94
LeanPool/SumOfSetsInSeveralDimensions/Imports.lean
import took 858ms
cumulative profiling times:
declTypeLinter 0.126ms
elaboration 0.15ms
import 858ms
initialization 31.9ms
interpretation 122ms
linting 0.238ms
module linting 0.00836ms
parsing 0.00195ms
tacticAnalysis 0.14ms
real 1.74
user 0.95
sys 0.83
LeanPool/SumOfSetsInSeveralDimensions/LowerBound.lean
import took 813ms
cumulative profiling times:
attribute application 0.0574ms
blocked (unaccounted) 0.0951ms
congr simp thm 5.85ms
declTypeLinter 3.29ms
elaboration 39ms
fix level params 0.41ms
grind 370ms
grind mark subsingleton 42.9ms
grind simp 313ms
import 813ms
initialization 41.5ms
instantiate metavars 2.37ms
interpretation 221ms
let-to-have transformation 0.169ms
linting 12ms
module linting 0.0148ms
parsing 7.83ms
process pre-definitions 2.52ms
share common exprs 2.33ms
simp 93.9ms
sym canon 51.3ms
sym typeclass inference 933ms
tactic execution 103ms
tacticAnalysis 4.76ms
type checking 161ms
typeclass inference 470ms
real 3.77
user 3.59
sys 0.85
LeanPool/SumOfSetsInSeveralDimensions/LowerBoundFunction.lean
import took 668ms
cumulative profiling times:
attribute application 0.117ms
compilation (IR) 0.194ms
compilation (LCNF base) 2.28ms
compilation (LCNF impure) 0.819ms
compilation (LCNF mono) 1.21ms
congr simp thm 1.78ms
declTypeLinter 4.77ms
elaboration 35.2ms
fix level params 0.304ms
grind 113ms
grind ac 0.267ms
grind cutsat 6.52ms
grind ematch 16.4ms
grind linarith 0.0287ms
grind mark subsingleton 8.47ms
grind ring 3.18ms
grind simp 103ms
import 668ms
initialization 31.9ms
instantiate metavars 2.68ms
interpretation 213ms
let-to-have transformation 0.131ms
linting 11.6ms
module linting 0.0143ms
parsing 7.35ms
process pre-definitions 2.83ms
share common exprs 1.64ms
simp 3.94ms
sym canon 11.1ms
sym typeclass inference 57.6ms
tactic execution 66.7ms
tacticAnalysis 4.69ms
type checking 220ms
typeclass inference 91.1ms
real 1.87
user 1.65
sys 0.76
LeanPool/SumOfSetsInSeveralDimensions/LowerBoundValues.lean
import took 743ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 369ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 628ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 356ms
cumulative profiling times:
attribute application 0.0559ms
congr simp thm 5.75ms
declTypeLinter 3.58ms
elaboration 29.2ms
fix level params 1.11ms
grind 220ms
grind ac 0.131ms
grind cutsat 5.4ms
grind ematch 11.8ms
grind linarith 0.0234ms
grind mark subsingleton 26.4ms
grind ring 1.83ms
grind simp 302ms
import 743ms
initialization 35.2ms
instantiate metavars 8.29ms
interpretation 1.58s
let-to-have transformation 0.0887ms
linting 13ms
module linting 0.0135ms
norm_num 12ms
parsing 5.67ms
process pre-definitions 11.4ms
ring 88.9ms
share common exprs 20ms
simp 416ms
sym canon 32.1ms
sym typeclass inference 113ms
tactic execution 97ms
tacticAnalysis 3.85ms
type checking 410ms
typeclass inference 415ms
real 2.84
user 4.51
sys 0.83
LeanPool/SumOfSetsInSeveralDimensions/MinCardAdd.lean
import took 803ms
cumulative profiling times:
attribute application 0.0764ms
congr simp thm 1.37ms
declTypeLinter 3.76ms
elaboration 26ms
fix level params 0.453ms
grind 26.6ms
grind mark subsingleton 2.21ms
grind simp 13.3ms
import 803ms
initialization 37.9ms
instantiate metavars 1.03ms
interpretation 217ms
let-to-have transformation 0.164ms
linting 10.7ms
module linting 0.00977ms
parsing 8.96ms
process pre-definitions 4.07ms
share common exprs 2.55ms
simp 29.6ms
sym canon 8.59ms
sym typeclass inference 155ms
tactic execution 59.1ms
tacticAnalysis 3.99ms
type checking 31.8ms
typeclass inference 153ms
real 1.89
user 1.50
sys 0.83
LeanPool/SumOfSetsInSeveralDimensions/Normalize.lean
import took 809ms
cumulative profiling times:
attribute application 0.118ms
congr simp thm 1.82ms
declTypeLinter 4.03ms
elaboration 46.4ms
fix level params 0.505ms
import 809ms
initialization 32ms
instantiate metavars 1.38ms
interpretation 203ms
let-to-have transformation 0.143ms
linting 12.2ms
module linting 0.0123ms
parsing 7.73ms
process pre-definitions 4.98ms
share common exprs 2.87ms
simp 16.5ms
tactic execution 57.9ms
tacticAnalysis 4.07ms
type checking 25.9ms
typeclass inference 85.9ms
real 1.81
user 1.25
sys 0.83
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source review of e3d4e889a2fcdf28c150a42d9ac2677aa764e9b9: approve.
This is a significant, completed formalization of the dimensional sumset lower bound, its asymmetric Freiman consequence, exact attained minima, and additional Freiman-model dimension bounds. The review covered all 12 mathematical modules. The geometric deletion proof derives its four cases from actual subspace and finite-cardinality arguments, and the strong induction discharges their premises after genuine finite-minimum normalization. The extremizers are explicit axis/basis sets with full affine dimension; both minimization theorems have actual admissible witnesses, including the boundary cases.
The Freiman transport preserves two-term additive relations and sumset cardinalities. Positive model dimension supplies an actual rational model; the zero-dimension branches are handled separately. Nonemptiness, cancellativity where required, and the cardinality order are retained. The new card correction restores B nonempty and |B| ≤ |A| in its final result. All 14 Lean files remain byte-identical to the fully reviewed initial head, and all seven advertised results are public through the registered entry module.
The pinned upstream supports the Apache-2.0 license and AI provenance. Ten mathematical modules differ only in import prefixes; the other two additionally remove the five unused DecidableEq binders disclosed in the facade. The broader exact-minimum range and the additional model-dimension consequences are disclosed extensions. I checked their actual proofs; full text of the 1994 paper was unavailable, so I do not claim a line-by-line paper comparison.
Bounded comparisons with current Mathlib, Tau Ceti and the pool found related Freiman-map, covering, growth and PFR infrastructure, without a matching sharp dimensional lower/exact-minimum endpoint among the inspected candidates. The import graph is acyclic and the implementation has no material quality finding.
This records source acceptance at this exact head. The five independent configured reviews, current applicable hosted checks and normal protected integration remain separate. No local compiler build was run.
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All seven card headlines match the Lean statements and proofs; full CI remains pending. |
| Novelty | ✅ pass |
No headline duplicate was identified in the checked declarations; the broader Tau Ceti comparison remains unverifiable. |
| Significance | ✅ pass |
The PR develops a completed research-level theory of sharp sumset bounds and their Freiman dimension consequences. |
| Sources | ✅ pass |
The upstream formalization is credited and variants are labelled; the publisher’s abstract supports the closed-form bound, but the full theorem statements remain independently unverifiable. |
| Code quality (advisory) | ✅ pass |
The geometry and arithmetic are factored into focused lemmas, with one minor API restriction; no local rebuild was run because Lake dependencies are absent. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The card discloses the nonemptiness, cardinality, dimension and doubling hypotheses, including cancellation for the doubling bounds; no additional mathematical result is assumed. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | additive combinatorics |
| Mode | theory_building |
| Code quality | 4 / 5 |
Statement check: The Lean proves the stated sumset inequalities, constructs attaining examples throughout the advertised range, and derives both small-doubling bounds for its rational-model Freiman dimension.
The Lean proves Ruzsa’s dimension-sensitive sumset lower bound, constructs sets attaining it, establishes exact minimum cardinalities, and derives quantitative Freiman dimension bounds for sets with small doubling.
Code quality findings (1)
- overstrong-typeclass —
LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean:203
The model-bound theorems at lines 202 and 288, and their_of_finrank_span_sub_eqwrappers at 217 and 301, unnecessarily require cancellation. Their proofs use the commutative-monoid model bound, cardinality preservation, and numerical arithmetic. Weaken these four declarations to[AddCommMonoid G]so they also apply to sets with Freiman models in noncancellative ambient monoids.
Evidence:theorem le_two_mul_sub_one_of_isAddFreimanIso {G : Type*} [DecidableEq G] [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ}usesmod_cast two_mul_card_add_mul_card_le_of_isAddFreimanIso hX hf hdim. That helper is declaredlemma two_mul_card_add_mul_card_le_of_isAddFreimanIso {G : Type*} [DecidableEq G] [AddCommMonoid G]. The second theorem,le_sub_one_add_mul_div_card_of_isAddFreimanIso, uses the same helper andhave hr := le_two_mul_sub_one_of_isAddFreimanIso hX hXX hf hdim; both wrappers delegate to these theorems.
Tokens: 5,991,858 in / 33,724 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $24.4733 (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.
Import the formalization of Ruzsa, "Sum of sets in several dimensions" (Combinatorica 14 (1994), from$\left\lvert A + B \right\rvert \ge \left\lvert A \right\rvert + \sum \min(d, \left\lvert A\right\rvert - t)$ for sumsets of affine dimension $d$ in $\mathbb{R}^D$ , its sharpness (Theorem 2), the asymmetric Freiman lemma, and bounds on the Freiman dimension of sets of small doubling.
gdahia/SumOfSetsInSeveralDimensionsat bd2694b: the lower boundThe library moves under LeanPool.SumOfSetsInSeveralDimensions with its imports rewritten. I have also a Palomar submission for an earlier version of it.
The goal is to later add Chang's version of Freiman's theorem, formalized in https://github.com/gdahia/ChangFreimanRuzsa. That, however, is blocked by TauCeti's version here not having Minkowski's second theorem, and by lack of some of the Fourier machinery in https://github.com/YaelDillies/apap