Descent of winnability and rank along a regular subdivision

The vertex inequalities for the rounded script, and the descent theorems winnable_of_winnable_scale and rank_ge_of_rank_scale_ge. See Utilities/Subdivision/SubdivisionChipDescent.lean for the definitions and the overall argument.

Counting the rounded chips at a coarse vertex

The rounded chip divisor coarseChips is a sum of one-chip divisors, and the counters leftCount/rightCount are cardinalities of filters of the chip index type. Both are rewritten as sums of indicators, after which every vertex identity reduces to a single statement about one chip.

The two per-chip identities

The two vertex counts

The vertex inequalities and the descent theorem

theorem Utilities.Certificate.SubdivisionGraph.Spec.prin_roundedScript_ge {n p : ℕ} (spec : Spec n p) (N : ℕ) (hN : 0 < N) {ι : Type u_1} [Fintype ι] (chips : ι → spec.Chip N) (D₀ : CFDiv spec.graph) (σ : firingScript (spec.scale N hN).graph) (hσ : effective (spec.embed N hN D₀ + spec.fineChips N hN chips + (prin (spec.scale N hN).graph) σ)) (κ : Fin N) (hκ : ∀ (step : spec.Step), CommonOffsetRounding.round N κ (spec.fineValue N hN σ step.fst (N * (↑step.snd + 1)) + spec.stepCost N chips step) = CommonOffsetRounding.round N κ (spec.fineValue N hN σ step.fst (N * (↑step.snd + 1)))) (v : spec.Vertex) : (prin (spec.scale N hN).graph) σ (spec.fineOf N hN v) - spec.coarseChips N chips v ≤ (prin spec.graph) (spec.roundedScript N hN κ σ) v

At every coarse vertex, the rounded script loses at most the number of chips rounded to that vertex relative to the fine script at its image.

theorem Utilities.Certificate.SubdivisionGraph.Spec.winnable_of_winnable_scale_cost {n p : ℕ} (spec : Spec n p) (N : ℕ) (hN : 0 < N) {ι : Type u_1} [Fintype ι] (chips : ι → spec.Chip N) (D₀ : CFDiv spec.graph) (hcost : ∑ step : spec.Step, |spec.stepCost N chips step| < ↑N) (hwin : winnable (spec.scale N hN).graph (spec.embed N hN D₀ + spec.fineChips N hN chips)) : winnable spec.graph (D₀ + spec.coarseChips N chips)

Descent of winnability, signed-budget form. If the sum over coarse steps of the absolute signed rounding cost of the chips in that step is less than N, winnability on the N-fold refinement of the embedded divisor plus the chips implies winnability on the coarse graph of the divisor plus the rounded chips. Chips on one step rounded in opposite directions cancel: at N = 3, chips at offsets 1 and 2 of one edge, rounded left and right, cost nothing.

theorem Utilities.Certificate.SubdivisionGraph.Spec.winnable_of_winnable_scale {n p : ℕ} (spec : Spec n p) (N : ℕ) (hN : 0 < N) {ι : Type u_1} [Fintype ι] (chips : ι → spec.Chip N) (D₀ : CFDiv spec.graph) (hbudget : ∑ i : ι, ↑(chips i).distance < ↑N) (hwin : winnable (spec.scale N hN).graph (spec.embed N hN D₀ + spec.fineChips N hN chips)) : winnable spec.graph (D₀ + spec.coarseChips N chips)

Descent of winnability, distance form. If the total rounding distance of the chips is less than N, winnability on the N-fold refinement of the embedded divisor plus the chips implies winnability on the coarse graph of the divisor plus the rounded chips. This is the special case of the signed budget in which every chip is charged its full distance.

theorem Utilities.Certificate.SubdivisionGraph.Spec.rank_ge_of_rank_scale_ge_cost {n p : ℕ} (spec : Spec n p) (N : ℕ) (hN : 0 < N) {ι : Type u_1} [Fintype ι] (chips : ι → spec.Chip N) (D₀ : CFDiv spec.graph) (r : ℤ) (hcost : ∑ step : spec.Step, |spec.stepCost N chips step| < ↑N) (hrank : rank (spec.scale N hN).graph (spec.embed N hN D₀ + spec.fineChips N hN chips) ≥ r) : rank spec.graph (D₀ + spec.coarseChips N chips) ≥ r

Descent of rank, signed-budget form. Coarse rank tests embed into fine rank tests, so the descent of winnability upgrades to every rank lower bound. The hypothesis charges each coarse step only the absolute value of the signed sum of its chips' rounding costs, so chips on one step rounded in opposite directions cancel.

theorem Utilities.Certificate.SubdivisionGraph.Spec.rank_ge_of_rank_scale_ge {n p : ℕ} (spec : Spec n p) (N : ℕ) (hN : 0 < N) {ι : Type u_1} [Fintype ι] (chips : ι → spec.Chip N) (D₀ : CFDiv spec.graph) (r : ℤ) (hbudget : ∑ i : ι, ↑(chips i).distance < ↑N) (hrank : rank (spec.scale N hN).graph (spec.embed N hN D₀ + spec.fineChips N hN chips) ≥ r) : rank spec.graph (D₀ + spec.coarseChips N chips) ≥ r

Descent of rank, distance form. The special case of the signed budget in which every chip is charged its full rounding distance.