Graph-distance to a target vertex in a simple polyhedron is at least d minus the shared tight-row count

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_simple_vertex
import Definitions.Def_Hirsch_walk

/-!
# Simple-polyhedron target-distance lower bound

Source: `hirsch-campaign/route1/flagship_actual_distance/attempt.md` §3.1,
synthesized in the flagship triage report Part A3: "for a fixed target
[vertex] and a vertex `v`, the graph-distance from `v` to [that target] is at
least `D − |tight(v) ∩ S|`... In particular, a vertex sharing only one facet
of a `D`-facet-defined target (a 'portal') is at distance at least `D − 1`
from that target." `PROVED-GENERAL`, recommended `PUBLISH-AS-THEOREM-STATEMENT`
+ `ATTEMPT-LEAN-PROOF-NOW`.

**Frame-audit correction made during this drafting pass (recorded per this
campaign's mandatory audit discipline).** The triage report's own prose
states the bound for an arbitrary "fixed target facet subset `S`", not
necessarily the full tight set of a specific target vertex. Checking this
literally against the source before committing to a Lean statement: **the
arbitrary-`S` form is false.** Counterexample: take `w = v` (so `L = 0`,
walk-length zero) and any `S ⊊ TightSet a b w` with `|S| < d` (e.g. `S = ∅`).
Then `S ⊆ TightSet a b w` holds trivially, but the claimed bound
`d - |TightSet a b v ∩ S| ≤ L = 0` becomes `d ≤ |S| < d`, which is false for
`d ≥ 1`. Re-reading `flagship_actual_distance/attempt.md` §3.1 directly (not
the triage's paraphrase) confirms the actual proved statement is about a
**specific target vertex** `w` (`"a rank-k source therefore requires at least
D−k edges to the cap"`, `"a simple portal has D−1 old facets and rank 1"` —
`w`'s own full tight set, of size exactly `d` since `w` is simple, is the
comparison set throughout, not an arbitrary smaller subset). This statement
therefore fixes `S := TightSet a b w` for an explicit simple target vertex
`w`, rather than quantifying over an arbitrary `S ⊆ TightSet a b w` as an
overly loose paraphrase might suggest — this is exactly the class of
dropped/loosened-hypothesis error this campaign's operating discipline exists
to catch, caught here before compilation rather than after publication.

**Frame audit, remaining hypotheses.** Global `IsSimplePolyhedron a b` is
required (not just `IsSimpleVertex` at `v` and `w`) because the argument
walks the entire path from `v` to `w`: at every `Adj`-step of the walk, the
per-edge invariant `simple_vertex_adjacent_tight_inter_card` is invoked, and
that requires *both* endpoints of *that* edge to be simple, for every edge of
the path, i.e. simplicity at every vertex visited — exactly `IsSimplePolyhedron`. -/

open scoped RealInnerProductSpace

namespace Hirsch

/-- In a simple polyhedron, the graph-distance from a vertex `v` to a specific
target vertex `w` is at least `d` minus the number of tight rows they share.
In particular (`|TightSet v ∩ TightSet w| = 1`, a "portal"), the distance is
at least `d - 1`. -/
theorem simple_polyhedron_target_distance_lower_bound
    {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hP : IsSimplePolyhedron a b)
    (v w : EuclideanSpace ℝ (Fin d))
    (hv : v ∈ Set.extremePoints ℝ (Hpoly a b))
    (hw : w ∈ Set.extremePoints ℝ (Hpoly a b))
    (L : ℕ) (hreach : Reach (Hpoly a b) L v w) :
    d - (TightSet a b v ∩ TightSet a b w).ncard ≤ L := by sorry

end Hirsch