Hypercubes as Cartesian products

This file starts the bridge from the abstract Cartesian-product pebbling theorem to hypercubes. The first ingredient is the coordinate split Q_{a+m} ≃ Q_a × Q_m.

def PebblingLean.Hypercube.splitVertex (a m : ℕ) (v : HypercubeVertex (a + m)) : HypercubeVertex a × HypercubeVertex m

Split a vertex of Q_{a+m} into its first a and last m coordinates.

Equations

• PebblingLean.Hypercube.splitVertex a m v = (fun (i : Fin a) => v (Fin.castAdd m i), fun (j : Fin m) => v (Fin.natAdd a j))

def PebblingLean.Hypercube.appendVertex {a m : ℕ} (p : HypercubeVertex a × HypercubeVertex m) : HypercubeVertex (a + m)

Append vertices of Q_a and Q_m to obtain a vertex of Q_{a+m}.

Equations

• PebblingLean.Hypercube.appendVertex p = Fin.append p.1 p.2

def PebblingLean.Hypercube.splitVertexEquiv (a m : ℕ) : HypercubeVertex (a + m) ≃ HypercubeVertex a × HypercubeVertex m

Coordinate splitting gives a vertex equivalence Q_{a+m} ≃ Q_a × Q_m.

Equations

• PebblingLean.Hypercube.splitVertexEquiv a m = { toFun := PebblingLean.Hypercube.splitVertex a m, invFun := PebblingLean.Hypercube.appendVertex, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PebblingLean.Hypercube.splitVertexEquiv_apply (a m : ℕ) (v : HypercubeVertex (a + m)) : (splitVertexEquiv a m) v = splitVertex a m v

@[simp]

theorem PebblingLean.Hypercube.splitVertexEquiv_symm_apply {a m : ℕ} (p : HypercubeVertex a × HypercubeVertex m) : (splitVertexEquiv a m).symm p = appendVertex p

theorem PebblingLean.Hypercube.dist_appendVertex {a m : ℕ} (x x' : HypercubeVertex a) (z z' : HypercubeVertex m) : dist (appendVertex (x, z)) (appendVertex (x', z')) = dist x x' + dist z z'

Hamming distance splits over appended coordinates.

theorem PebblingLean.Hypercube.appendVertex_adj_iff {a m : ℕ} (p q : HypercubeVertex a × HypercubeVertex m) : (graph (a + m)).Adj (appendVertex p) (appendVertex q) ↔ ((graph a).cartesianProduct (graph m)).Adj p q

Appended vertices are adjacent exactly when one factor is adjacent and the other factor is unchanged.

theorem PebblingLean.Hypercube.splitVertex_adj_iff {a m : ℕ} {v w : HypercubeVertex (a + m)} : (graph (a + m)).Adj v w ↔ ((graph a).cartesianProduct (graph m)).Adj (splitVertex a m v) (splitVertex a m w)

The coordinate split preserves adjacency.

def PebblingLean.Hypercube.splitGraphIso (a m : ℕ) : GraphIso (graph (a + m)) ((graph a).cartesianProduct (graph m))

Graph isomorphism Q_(a+m) ≃ Q_a □ Q_m.

Equations

• PebblingLean.Hypercube.splitGraphIso a m = { toEquiv := PebblingLean.Hypercube.splitVertexEquiv a m, adj_iff := ⋯ }

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_split_product_of_fiber_demands {a m : ℕ} {E : Pebbling (HypercubeVertex m)} {cost : HypercubeVertex m → ℕ} (hE : Pebbling.Solvable (graph m) E) (hcost : ∀ (z : HypercubeVertex m), E z ≠ 0 → Pebbling.HasSolvableAtMostSize (graph a) (E z) (cost z)) : Pebbling.HasSolvableAtMostSize (graph (a + m)) 1 (∑ z : HypercubeVertex m, if E z = 0 then 0 else cost z)

Hypercube-specific deterministic product step. A solvable distribution E on Q_m specifies how many pebbles must be prepared in each Q_a fiber; if those fiber demands can be met within the given costs, then Q_(a+m) has a solvable distribution with the summed cost.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_split_product_of_demand_cost {a m : ℕ} {E : Pebbling (HypercubeVertex m)} {demandCost : ℕ → ℕ} (hE : Pebbling.Solvable (graph m) E) (hcost : ∀ (T : ℕ), T ≠ 0 → Pebbling.HasSolvableAtMostSize (graph a) T (demandCost T)) : Pebbling.HasSolvableAtMostSize (graph (a + m)) 1 (∑ z : HypercubeVertex m, if E z = 0 then 0 else demandCost (E z))

Product step where the first-factor cost depends only on the demand value E z, not on the fiber location z.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_split_product_of_linear_demand_cost {a m K : ℕ} {E : Pebbling (HypercubeVertex m)} (hE : Pebbling.Solvable (graph m) E) (hcost : ∀ (T : ℕ), Pebbling.HasSolvableAtMostSize (graph a) T (K * T)) : Pebbling.HasSolvableAtMostSize (graph (a + m)) 1 (K * E.size)

Linear fiber-demand recurrence: if every demand T in Q_a can be solved with at most K*T pebbles, then using a solvable distribution E on Q_m as the second-factor demand pattern costs at most K * |E|.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_split_product_of_highDemand_demand_cost {a m T : ℕ} {E : Pebbling (HypercubeVertex m)} {demandCost : ℕ → ℕ} (hT : 1 ≤ T) (hE : Pebbling.SolvableAtLeast (graph m) E T) (hcost : ∀ (t : ℕ), t ≠ 0 → Pebbling.HasSolvableAtMostSize (graph a) t (demandCost t)) : Pebbling.HasSolvableAtMostSize (graph (a + m)) 1 (∑ z : HypercubeVertex m, if E z = 0 then 0 else demandCost (E z))

If the second factor is T-solvable with T ≥ 1, it may be used as the solvable demand pattern in the product step.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_split_product_of_uniform_fiber_bound {a m Tbase Tfiber K : ℕ} {E : Pebbling (HypercubeVertex m)} (hTbase : 1 ≤ Tbase) (hE : Pebbling.SolvableAtLeast (graph m) E Tbase) (hpile_le : ∀ (z : HypercubeVertex m), E z ≤ Tfiber) (hfiber : Pebbling.HasSolvableAtMostSize (graph a) Tfiber K) : Pebbling.HasSolvableAtMostSize (graph (a + m)) 1 (E.supportSize * K)

Uniform high-demand fiber recurrence. If E is a T-solvable second-factor distribution and every occupied pile of E has size at most Tfiber, then one Tfiber-solvable construction in Q_a can be reused for every occupied fiber.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_split_product_of_uniform_fiber_bound_minPile {a m Tbase Tfiber S K : ℕ} {E : Pebbling (HypercubeVertex m)} (hTbase : 1 ≤ Tbase) (hE : Pebbling.SolvableAtLeast (graph m) E Tbase) (hpile_le : ∀ (z : HypercubeVertex m), E z ≤ Tfiber) (hmin : E.MinOccupiedPileSize S) (hfiber : Pebbling.HasSolvableAtMostSize (graph a) Tfiber (S * K)) : Pebbling.HasSolvableAtMostSize (graph (a + m)) 1 (E.size * K)

Uniform fiber recurrence with occupied-pile compression. If each occupied pile of E has at least S pebbles, and a Tfiber-solvable construction in Q_a costs at most S*K, then the product cost is bounded by |E|*K.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_split_product_of_highDemand {a m Tbase costBound S K : ℕ} (hTbase : 1 ≤ Tbase) (hhigh : HasHighDemandDistribution m Tbase costBound S) (hfiber : Pebbling.HasSolvableAtMostSize (graph a) costBound (S * K)) : Pebbling.HasSolvableAtMostSize (graph (a + m)) 1 (costBound * K)

Recurrence step from a high-demand distribution. If Q_m has a Tbase-solvable distribution of size at most costBound whose occupied piles have size at least S, and Q_a can solve demand costBound with cost S*K, then Q_(a+m) has a solvable distribution with cost costBound*K.

theorem PebblingLean.Hypercube.hasHighDemandDistribution_split_product_of_highDemand {a m Tbase costBound S K Snew : ℕ} (hTbase : 1 ≤ Tbase) (hhigh : HasHighDemandDistribution m Tbase costBound S) (hfiber : HasHighDemandDistribution a costBound (S * K) Snew) : HasHighDemandDistribution (a + m) 1 (costBound * K) Snew

High-demand product recurrence preserving the next pile-size invariant. The same high-demand fiber construction in Q_a is reused for every occupied fiber over Q_m; occupied-pile compression in the Q_m distribution pays for this reuse.

theorem PebblingLean.Hypercube.hasHighDemandDistribution_split_product_of_highDemand_variable {a m Tbase costBound S K Snew : ℕ} (hTbase : 1 ≤ Tbase) (hhigh : HasHighDemandDistribution m Tbase costBound S) (hfiber : ∀ (t : ℕ), S ≤ t → HasHighDemandDistribution a t (t * K) Snew) : HasHighDemandDistribution (a + m) 1 (costBound * K) Snew

Variable-demand high-demand product recurrence.

This is the paper-facing product step. If an occupied second-factor pile has size s_z, we use a first-factor construction for demand s_z and cost s_z*K. Summing over occupied fibers gives total cost |E|*K, and the high-demand bound on E then gives costBound*K.