PebblingNumberConjecture.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

11 declarations, 1 contain sorry, 0 declared as axioms

Pebbling number conjecture

References:

Imports (1)

FormalConjecturesUtil

def PebblingNumberConjecture.PebbleDistribution A Pebble distribution is an assignment of zero or more pebbles to each of the vertices line 36 source
Source documentation
A Pebble distribution is an assignment of zero or more pebbles to each of the vertices.

no axioms what this means
Proof uses: Nat
```
def PebbleDistribution (V : Type) := V → ℕ
```
def PebblingNumberConjecture.NumberOfPebbles The number of pebbles of a distribution is the total number summed over all vertices line 41 source
Source documentation
The number of pebbles of a distribution is the total number summed over all vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, PebblingNumberConjecture.PebbleDistribution, Nat
Proof uses: Finset.sum, Finset.univ
1 instances, coercions and auxiliary constants left out.
```
def NumberOfPebbles [Fintype V] : (PebbleDistribution V) → ℕ := fun D => ∑ v, D v
```
Mentions: PebblingNumberConjecture.PebbleDistribution
def PebblingNumberConjecture.IsPebblingMove Documented declaration: IsPebblingMove line 48 source
Source documentation
A pebbling move on a graph consists of choosing a vertex with at least two pebbles, removing two pebbles from it, and adding one to an adjacent vertex (the second removed pebble is discarded from play).

no axioms what this means
Statement uses: DecidableEq, SimpleGraph, PebblingNumberConjecture.PebbleDistribution
Proof uses: Exists, And, GE.ge, Nat, OfNat.ofNat, SimpleGraph.Adj, Eq, ite, HAdd.hAdd, HSub.hSub
6 instances, coercions and auxiliary constants left out.
```
def IsPebblingMove (G : SimpleGraph V) (A B : PebbleDistribution V) : Prop :=
…
```
Mentions: PebblingNumberConjecture.PebbleDistribution
theorem PebblingNumberConjecture.IsPebblingMove.refl line 56 source
no axioms what this means
Statement uses: DecidableEq, SimpleGraph, PebblingNumberConjecture.PebbleDistribution, LE.le, Nat, OfNat.ofNat, SimpleGraph.Adj, PebblingNumberConjecture.IsPebblingMove, ite, Eq, HAdd.hAdd, HSub.hSub
Proof uses: Exists.intro, Exists, And, GE.ge, And.intro, rfl
12 instances, coercions and auxiliary constants left out.

inductive PebblingNumberConjecture.PebblePath A pebble path is a series of pebbling moves line 67 source

Source documentation

A pebble path is a series of pebbling moves.

no axioms what this means

inductive PebblePath {α : Type} (r : α → α → Prop) : α → α → Type
  | refl (a : α) : PebblePath r a a
  | step {a b c : α} (p : PebblePath r a b) (h : r b c) : PebblePath r a c

/--
Indicates whether there exists a sequence of pebbling moves transforming one pebble distribution
to another.
-/

Mentions: c

def PebblingNumberConjecture.ExistsPebblePath Indicates whether there exists a sequence of pebbling moves transforming one pebble distribution to another line 75 source
Source documentation
Indicates whether there exists a sequence of pebbling moves transforming one pebble distribution to another.

no axioms what this means
Proof uses: Nonempty, PebblingNumberConjecture.PebblePath
```
def ExistsPebblePath {α : Type} (r : α → α → Prop) (a b : α) : Prop :=
…
```
def PebblingNumberConjecture.IsReachable A pebble distribution B is reachable from another pebble distribution A, if there exists a sequence of pebbling moves transforming the first into the second line 82 source
Source documentation
A pebble distribution B is reachable from another pebble distribution A, if there exists a sequence of pebbling moves transforming the first into the second.

no axioms what this means
Statement uses: DecidableEq, SimpleGraph, PebblingNumberConjecture.PebbleDistribution
Proof uses: PebblingNumberConjecture.ExistsPebblePath, PebblingNumberConjecture.IsPebblingMove
```
def IsReachable (G : SimpleGraph V) (A B : PebbleDistribution V) : Prop :=
…
```
Mentions: PebblingNumberConjecture.PebbleDistribution
theorem PebblingNumberConjecture.IsReachable.refl line 86 source
no axioms what this means
Statement uses: DecidableEq, SimpleGraph, PebblingNumberConjecture.PebbleDistribution, PebblingNumberConjecture.IsReachable
Proof uses: Nonempty.intro, PebblingNumberConjecture.PebblePath, PebblingNumberConjecture.IsPebblingMove, PebblingNumberConjecture.PebblePath.refl

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def PebblingNumberConjecture.PebblingNumber Documented declaration: PebblingNumber line 95 source
Source documentation
The pebbling number of a graph G, is the lowest natural number n that satisfies the following condition: Given any target or 'root' vertex in the graph and any initial pebbles distribution with n pebbles on the graph, another pebble distribution is reachable in which the designated root vertex has one or more pebbles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, SimpleGraph, Nat
Proof uses: InfSet.sInf, Set.ofPred, PebblingNumberConjecture.PebbleDistribution, Eq, PebblingNumberConjecture.NumberOfPebbles, Exists, And, PebblingNumberConjecture.IsReachable, LE.le, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
noncomputable def PebblingNumber [Fintype V] (G : SimpleGraph V) : ℕ :=
…
```
theorem PebblingNumberConjecture.PebblingNumber_completeGraph The pebbling number of the complete graph on n vertices is n line 102 source
Source documentation
The pebbling number of the complete graph on n vertices is n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Fintype, Eq, Nat, PebblingNumberConjecture.PebblingNumber, SimpleGraph.completeGraph, Fintype.card
Proof uses: IsLeast.csInf_eq, Set.ofPred, PebblingNumberConjecture.PebbleDistribution, PebblingNumberConjecture.NumberOfPebbles, Exists, And, PebblingNumberConjecture.IsReachable, LE.le, OfNat.ofNat, And.intro, Membership.mem, Set, lowerBounds, dite, Classical.propDecidable, Exists.intro, PebblingNumberConjecture.IsReachable.refl, Eq.rec, Nat.one_le_of_lt, Not and 84 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
theorem PebblingNumber_completeGraph [Fintype V] :
    PebblingNumber (SimpleGraph.completeGraph V) = Fintype.card V := by
…
```
Mentions: PebblingNumberConjecture.PebblingNumber
theorem PebblingNumberConjecture.pebbling_number_conjecture The pebbling number conjecture: the pebbling number of a Cartesian product of connected graphs is at most equal to the product of the pebbling numbers of the factors sorry line 134 source
Source documentation
The pebbling number conjecture: the pebbling number of a Cartesian product of connected graphs is at most equal to the product of the pebbling numbers of the factors. See Asplund, Hurlbert, and Kenter.

L4DEL explanation
The pebbling number conjecture: the pebbling number of a Cartesian product of connected graphs is at most equal to the product of the pebbling numbers of the factors. See Asplund, Hurlbert, and Kenter.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: DecidableEq, Fintype, SimpleGraph, SimpleGraph.Connected, LE.le, Nat, PebblingNumberConjecture.PebblingNumber, Prod, SimpleGraph.boxProd, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pebbling_number_conjecture {W : Type} [Fintype V] [Fintype W] [DecidableEq W]
    (G : SimpleGraph V) (H : SimpleGraph W) (hG : G.Connected) (hH : H.Connected) :
    PebblingNumber (G □ H) ≤ PebblingNumber G * PebblingNumber H := by
…
```
Mentions: PebblingNumberConjecture.PebblingNumber