The step inequality for chip descent

For a fine winning script, the height difference across one coarse step, corrected by the signed rounding cost of the chips inside that step, is bounded by N times the first and last fine slopes adjusted by the numbers of chips rounded to either end. With a common rounding offset absorbing the costs, the same bounds hold for the coarse slopes of the rounded script. See Utilities/Subdivision/SubdivisionChipDescent.lean for the definitions and the overall argument.

Fine vertices strictly inside a coarse step

A fine interior vertex at a fine offset that is not a multiple of N is not in the image of the coarse graph, and the chips sitting on it are exactly the chips of the corresponding coarse step with the corresponding offset.

The three bounds

theorem Utilities.Certificate.SubdivisionGraph.Spec.sum_abs_stepCost_le {n p : ℕ} (spec : Spec n p) (N : ℕ) {ι : Type u_1} [Fintype ι] (chips : ι → spec.Chip N) : ∑ step : spec.Step, |spec.stepCost N chips step| ≤ ∑ i : ι, ↑(chips i).distance

The total signed rounding cost over all steps is bounded by the total rounding distance.

theorem Utilities.Certificate.SubdivisionGraph.Spec.step_bounds {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) σ)) (step : spec.Step) : ↑N * (spec.fineSlope N hN σ step.fst (N * ↑step.snd) - spec.leftCount N chips step) ≤ spec.fineValue N hN σ step.fst (N * (↑step.snd + 1)) + spec.stepCost N chips step - spec.fineValue N hN σ step.fst (N * ↑step.snd) ∧ spec.fineValue N hN σ step.fst (N * (↑step.snd + 1)) + spec.stepCost N chips step - spec.fineValue N hN σ step.fst (N * ↑step.snd) ≤ ↑N * (spec.fineSlope N hN σ step.fst (N * (↑step.snd + 1) - 1) + spec.rightCount N chips step)

The step inequality. For a fine winning script, the height difference across a coarse step, corrected by the signed rounding cost of its chips, lies between N times (first fine slope minus the left count) and N times (last fine slope plus the right count).

theorem Utilities.Certificate.SubdivisionGraph.Spec.roundedSlope_bounds {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)))) (step : spec.Step) : spec.fineSlope N hN σ step.fst (N * ↑step.snd) - spec.leftCount N chips step ≤ spec.roundedSlope N hN κ σ step.fst ↑step.snd ∧ spec.roundedSlope N hN κ σ step.fst ↑step.snd ≤ spec.fineSlope N hN σ step.fst (N * (↑step.snd + 1) - 1) + spec.rightCount N chips step

With a common offset that absorbs the rounding costs, every coarse slope of the rounded script is bounded by the corresponding fine endpoint slopes and chip counts.