Product constructions

This file begins the deterministic part of the upper-bound proof. The main result here is the slice simulation lemma: a pebbling sequence in one factor of a Cartesian product can be executed inside a fixed slice of the product.

def PebblingLean.Graph.cartesianProduct {V : Type u} {W : Type v} (G : Graph V) (H : Graph W) : Graph (V × W)

Cartesian product of simple graphs.

Equations

• G.cartesianProduct H = { Adj := fun (p q : V × W) => G.Adj p.1 q.1 ∧ p.2 = q.2 ∨ p.1 = q.1 ∧ H.Adj p.2 q.2, symm := ⋯, loopless := ⋯ }

def PebblingLean.Pebbling.fibersDistribution {V : Type u} {W : Type v} (F : W → Pebbling V) : Pebbling (V × W)

A product distribution assembled from first-factor fibers indexed by the second factor. The value at (x, z) is the value of the z-fiber at x.

Equations

• PebblingLean.Pebbling.fibersDistribution F p = F p.2 p.1

@[simp]

theorem PebblingLean.Pebbling.fibersDistribution_apply {V : Type u} {W : Type v} (F : W → Pebbling V) (x : V) (z : W) : fibersDistribution F (x, z) = F z x

def PebblingLean.Pebbling.replaceFiber {V : Type u} {W : Type v} [DecidableEq W] (F : W → Pebbling V) (z : W) (E : Pebbling V) : W → Pebbling V

Replace one first-factor fiber in a family of fibers.

Equations

• PebblingLean.Pebbling.replaceFiber F z E z' = if z' = z then E else F z'

def PebblingLean.Pebbling.updateFibers {V : Type u} {W : Type v} [DecidableEq W] (F F' : W → Pebbling V) (s : Finset W) : W → Pebbling V

The family obtained by replacing all fibers in s by their target fibers.

Equations

• PebblingLean.Pebbling.updateFibers F F' s z = if z ∈ s then F' z else F z

theorem PebblingLean.Pebbling.size_fibersDistribution {V : Type u} {W : Type v} [Fintype V] [Fintype W] (F : W → Pebbling V) : (fibersDistribution F).size = ∑ z : W, (F z).size

Total size of a fiber-assembled product distribution.

theorem PebblingLean.Pebbling.size_fibersDistribution_le {V : Type u} {W : Type v} [Fintype V] [Fintype W] {F : W → Pebbling V} {cost : W → ℕ} (hcost : ∀ (z : W), (F z).size ≤ cost z) : (fibersDistribution F).size ≤ ∑ z : W, cost z

A pointwise fiber cost bound gives a product cost bound.

def PebblingLean.Pebbling.sliceDistribution {V : Type u} {W : Type v} [DecidableEq V] (x : V) (E : Pebbling W) : Pebbling (V × W)

A distribution supported in the slice {x} × W, with profile E in the second coordinate.

Equations

• PebblingLean.Pebbling.sliceDistribution x E p = if p.1 = x then E p.2 else 0

@[simp]

theorem PebblingLean.Pebbling.sliceDistribution_apply_on {V : Type u} {W : Type v} [DecidableEq V] (x : V) (E : Pebbling W) (z : W) : sliceDistribution x E (x, z) = E z

@[simp]

theorem PebblingLean.Pebbling.sliceDistribution_apply_off {V : Type u} {W : Type v} [DecidableEq V] {x x' : V} (E : Pebbling W) (z : W) (h : x' ≠ x) : sliceDistribution x E (x', z) = 0

theorem PebblingLean.Pebbling.replaceFiber_move_left {V : Type u} {W : Type v} [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E F : Pebbling V} {Fs : W → Pebbling V} {z : W} (hmove : Move G E F) : Move (G.cartesianProduct H) (fibersDistribution (replaceFiber Fs z E)) (fibersDistribution (replaceFiber Fs z F))

One move in the first factor can be replayed inside a fixed fiber of the Cartesian product, leaving all other fibers unchanged.

theorem PebblingLean.Pebbling.replaceFiber_reaches_left {V : Type u} {W : Type v} [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E F : Pebbling V} {Fs : W → Pebbling V} {z : W} (hreach : Reaches G E F) : Reaches (G.cartesianProduct H) (fibersDistribution (replaceFiber Fs z E)) (fibersDistribution (replaceFiber Fs z F))

A pebbling sequence in the first factor can be replayed inside a fixed fiber of the product.

theorem PebblingLean.Pebbling.fibers_reaches_of_forall_reaches {V : Type u} {W : Type v} [Finite W] [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {F F' : W → Pebbling V} (hreach : ∀ (z : W), Reaches G (F z) (F' z)) : Reaches (G.cartesianProduct H) (fibersDistribution F) (fibersDistribution F')

Independent first-factor preparations in every fiber can be composed into one product pebbling sequence.

theorem PebblingLean.Pebbling.slice_move_right {V : Type u} {W : Type v} [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E F : Pebbling W} {x : V} (hmove : Move H E F) : Move (G.cartesianProduct H) (sliceDistribution x E) (sliceDistribution x F)

One move in the second factor can be replayed inside a fixed product slice.

theorem PebblingLean.Pebbling.slice_reaches_right {V : Type u} {W : Type v} [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E F : Pebbling W} {x : V} (hreach : Reaches H E F) : Reaches (G.cartesianProduct H) (sliceDistribution x E) (sliceDistribution x F)

A pebbling sequence in the second factor can be replayed inside a fixed slice of the product.

theorem PebblingLean.Pebbling.slice_canReachAtLeast_right {V : Type u} {W : Type v} [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E : Pebbling W} {x : V} {target : W} {T : ℕ} (hcan : CanReachAtLeast H E target T) : CanReachAtLeast (G.cartesianProduct H) (sliceDistribution x E) (x, target) T

If E solves a target in the second factor, then the corresponding slice distribution solves the corresponding product target.

theorem PebblingLean.Pebbling.canReachAtLeast_of_dominates_slice_right {V : Type u} {W : Type v} [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {D : Pebbling (V × W)} {E : Pebbling W} {x : V} {target : W} {T : ℕ} (hdom : D.Dominates (sliceDistribution x E)) (hcan : CanReachAtLeast H E target T) : CanReachAtLeast (G.cartesianProduct H) D (x, target) T

Once a product distribution dominates a prepared slice, any target reachable from the slice is also reachable from the product distribution.

theorem PebblingLean.Pebbling.canReachAtLeast_after_prepared_slice_right {V : Type u} {W : Type v} [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {D Dprep : Pebbling (V × W)} {E : Pebbling W} {x : V} {target : W} {T : ℕ} (hprepReach : Reaches (G.cartesianProduct H) D Dprep) (hprepDom : Dprep.Dominates (sliceDistribution x E)) (hcan : CanReachAtLeast H E target T) : CanReachAtLeast (G.cartesianProduct H) D (x, target) T

Composition bridge for the deterministic product step: if a first phase reaches a distribution dominating the prepared slice {x} × W, then a solution inside the W factor can be appended to solve the product target.

theorem PebblingLean.Pebbling.fibers_prepare_slice_right {V : Type u} {W : Type v} [Finite W] [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E : Pebbling W} {F : W → Pebbling V} {x : V} (hcan : ∀ (z : W), CanReachAtLeast G (F z) x (E z)) : ∃ (Dprep : Pebbling (V × W)), Reaches (G.cartesianProduct H) (fibersDistribution F) Dprep ∧ Dprep.Dominates (sliceDistribution x E)

If every fiber can prepare the number of pebbles prescribed by E at the same first-coordinate target x, then the product distribution can be moved to a distribution dominating the slice {x} × W with profile E.

theorem PebblingLean.Pebbling.solvable_product_of_fiber_demands {V : Type u} {W : Type v} [Finite W] [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E : Pebbling W} {F : W → Pebbling V} (hE : Solvable H E) (hF : ∀ (z : W), SolvableAtLeast G (F z) (E z)) : Solvable (G.cartesianProduct H) (fibersDistribution F)

Deterministic product step. If E solves H, and each z-fiber has enough demand-solvability in G to prepare E z pebbles at any chosen first-coordinate target, then the assembled product distribution solves G □ H.

theorem PebblingLean.Pebbling.hasSolvableAtMostSize_product_of_fiber_demands {V : Type u} {W : Type v} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] {G : Graph V} {H : Graph W} {E : Pebbling W} {cost : W → ℕ} (hE : Solvable H E) (hcost : ∀ (z : W), E z ≠ 0 → HasSolvableAtMostSize G (E z) (cost z)) : HasSolvableAtMostSize (G.cartesianProduct H) 1 (∑ z : W, if E z = 0 then 0 else cost z)

Costed form of the deterministic product step, matching the recursive upper-bound bookkeeping: only occupied vertices of E need nonzero demand distributions in the first factor.