Lower-bound infrastructure for hypercubes

This file starts the formal version of the weight-function lower bound. The main result here is the first inequality in the paper's lower-bound proof: for a solvable distribution on Q_n, every target has initial weight at least one, and hence the sum of all target weights is at least |Q_n|.

theorem PebblingLean.Hypercube.one_le_weight_of_canReach {n : ℕ} {D : Pebbling (HypercubeVertex n)} {target : HypercubeVertex n} (hcan : Pebbling.CanReach (graph n) D target) : 1 ≤ Pebbling.weight dist D target

For the hypercube, any target reachable from D has initial weight at least one with respect to that target.

theorem PebblingLean.Hypercube.one_le_weight_of_solvable {n : ℕ} {D : Pebbling (HypercubeVertex n)} (hsolv : Pebbling.Solvable (graph n) D) (target : HypercubeVertex n) : 1 ≤ Pebbling.weight dist D target

A solvable distribution has target weight at least one for every target.

theorem PebblingLean.Hypercube.card_le_sum_weight_of_solvable {n : ℕ} {D : Pebbling (HypercubeVertex n)} (hsolv : Pebbling.Solvable (graph n) D) : ↑(Fintype.card (HypercubeVertex n)) ≤ ∑ target : HypercubeVertex n, Pebbling.weight dist D target

Summing the target-wise lower bound over all targets gives |Q_n| ≤ ∑_t W_t(D).

theorem PebblingLean.Hypercube.sum_invPow_card_finsets (n : ℕ) : ∑ s : Finset (Fin n), 1 / 2 ^ s.card = (3 / 2) ^ n

The finite-subset identity behind the inner hypercube weight sum.

theorem PebblingLean.Hypercube.sum_unitWeight (n : ℕ) (base : HypercubeVertex n) : ∑ target : HypercubeVertex n, Pebbling.unitWeight dist target base = (3 / 2) ^ n

For a fixed hypercube vertex base, the sum of one-pebble weights over all targets is (3/2)^n.

theorem PebblingLean.Hypercube.sum_weight_eq_size_mul {n : ℕ} (D : Pebbling (HypercubeVertex n)) : ∑ target : HypercubeVertex n, Pebbling.weight dist D target = ↑D.size * (3 / 2) ^ n

The double sum of weights factors as |D| * (3/2)^n.

theorem PebblingLean.Hypercube.card_le_size_mul_of_solvable {n : ℕ} {D : Pebbling (HypercubeVertex n)} (hsolv : Pebbling.Solvable (graph n) D) : ↑(Fintype.card (HypercubeVertex n)) ≤ ↑D.size * (3 / 2) ^ n

Formal version of the averaged weight inequality |Q_n| ≤ |D| (3/2)^n for every solvable distribution D.

theorem PebblingLean.Hypercube.lower_bound_size_of_solvable {n : ℕ} {D : Pebbling (HypercubeVertex n)} (hsolv : Pebbling.Solvable (graph n) D) : (4 / 3) ^ n ≤ ↑D.size

The lower bound in the paper's usual rational form: every solvable distribution on Q_n has at least (4/3)^n pebbles.

theorem PebblingLean.Hypercube.lower_bound_of_hasSolvableSize {n k : ℕ} (h : Pebbling.HasSolvableSize (graph n) k) : (4 / 3) ^ n ≤ ↑k

Lower bound for any specified solvable size.

theorem PebblingLean.Hypercube.lower_bound_of_isOptimalNumber {n k : ℕ} (hopt : Pebbling.IsOptimalNumber (graph n) k) : (4 / 3) ^ n ≤ ↑k

Lower bound for any k certified as the optimal pebbling number.