A quantity ranging over k+1 values cannot certify a strictly-decreasing walk longer than k

import Mathlib

/-!
# Obstruction Lemma: a bounded-range descent quantity cannot certify unbounded length

Source: `hirsch-campaign/route1/intrinsic_sonnet/attempt.md` §5 ("Obstruction
Lemma"), refined and reused by `route1/flagship_prep/report.md` §4. Triage
report Part A2, `PROVED-GENERAL`, recommended `PUBLISH-AS-THEOREM-STATEMENT`
and `ATTEMPT-LEAN-PROOF-NOW`.

**Exact source statement:** "Let `Φ : V(P) → {0,…,k}` be any quantity (in
particular, any function of the facet-tight-set data alone) taking at most
`k+1` distinct values, where `k` may depend on the ambient dimension `D` but
*not* on the number of facets `n`. Suppose, for contradiction, `Φ` strictly
decreases along every step of a shortest path to a fixed target, for every
member of a family of polytopes of fixed dimension `D` whose diameter is
unbounded as `n → ∞`. Then for `n` large enough that `diam(P) > k`, no
shortest path of that length can have `Φ` strictly decrease at every step (a
strictly decreasing sequence of integers valued in a set of size `k+1` has
length at most `k`) — contradiction."

**Frame audit / extraction.** The triage report's own Part C explicitly
recommends stating this "abstractly as a fact about strictly decreasing
ℕ-valued (or `Fin k`-valued) sequences along paths in a graph with unbounded
diameter, decoupled entirely from 'tight facet sets'" — the polytope framing
(vertices, shortest paths, facet-tight-set data) is only the motivating
instance, not part of the proved content. The proved core fact, isolated from
that motivating instance, is exactly: a walk `w` in an arbitrary type `V`
along which a quantity `Φ` valued in a `(k+1)`-element set strictly decreases
at every one of `L` consecutive steps must have `L ≤ k` — this is what the
source itself identifies as the load-bearing content ("essentially: an
injective — actually just strictly-monotone — integer sequence into a finite
set has bounded length"). No polytope vocabulary (`Hpoly`, `Adj`, `TightSet`,
etc.) appears in this statement, exactly as the triage report specifies; `V`
is an arbitrary type so that this same fact applies uniformly to vertex
graphs of any fixed dimension `D` (via `Fin (k+1)`-valued tight-set data) or
to any other combinatorial walk. The convex `n`-gon witness (`D = 2` fixed,
diameter `⌊n/2⌋ → ∞`) used in the source to show this bound has real force
against unbounded-diameter families is an *application* of this lemma, not
part of its statement, and is not encoded here. -/

namespace Hirsch

/-- If a quantity `Φ : V → Fin (k + 1)` (taking at most `k + 1` distinct
values) strictly decreases at every one of `L` consecutive steps of a walk
`w : ℕ → V`, then `L ≤ k`. This is the general, polytope-independent content
of the Obstruction Lemma: no quantity ranging over a set of size `k + 1` can
certify a strictly-decreasing walk longer than `k`. -/
theorem bounded_range_descent_bound
    {V : Type*} {k L : ℕ} (Φ : V → Fin (k + 1)) (w : ℕ → V)
    (hdec : ∀ i < L, Φ (w (i + 1)) < Φ (w i)) :
    L ≤ k := by sorry

end Hirsch