Adjacent simple vertices of a polyhedron share exactly d-1 tight rows

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_simple_vertex

/-!
# Adjacent simple vertices share exactly `d - 1` tight facets

Source: `hirsch-campaign/route1/flagship_actual_distance/attempt.md` §3.1 and
`route1/flagship_simple_general/attempt.md` §3 (common rank-jump inequality,
specialized to simple vertices). Triage report Part A3, `PROVED-GENERAL`,
recommended `PUBLISH-AS-THEOREM-STATEMENT` + `ATTEMPT-LEAN-PROOF-NOW`.

**Exact source derivation** (`flagship_actual_distance` §3.1). For adjacent
finite vertices `v, w`, with `k(v) = |T(v)|` the number of tight rows, the
predecessor's general rank-jump inequality is `k(w) - k(v) ≤ e(w) + 1` where
`e(x) = |R(x)| + |T(x)| - D` is the excess-tight-row count (`R(x)` old rows,
`T(x)` new rows in the local-model framing; in the single-polyhedron framing
used here `e(x) = |T(x)| - D` reduces to 0 exactly at a **simple** vertex).
"In a simple local model `e = 0` everywhere. Applying (3) in both directions
gives `|k(w) - k(v)| ≤ 1`, even on unrestricted edges." Since a simple vertex
has *exactly* `d` tight rows (`IsSimpleVertex`'s cardinality conjunct) and
`|k(w) - k(v)| ≤ 1` with `k(v) = k(w) = d`, the shared tight-row count
`|T(v) ∩ T(w)|` is pinned to exactly `d - 1` (it cannot be less, since a
common `(D-1)`-rank tight subspace is needed for the edge to have the correct
dimension, and it cannot be `d` since that would force `T(v) = T(w)`, making
`v = w` a full-rank coincidence, contradicting `v ≠ w`'s two distinct
adjacent-vertex assumption) — this is exactly the standard "adjacent vertices
of a simple polytope differ in exactly one tight facet" fact.

**Frame audit.** Only `IsSimpleVertex a b v` and `IsSimpleVertex a b w`
(*not* the global `IsSimplePolyhedron a b`) are required: the source's
derivation only uses `e(v) = 0` and `e(w) = 0`, i.e. simplicity at the two
specific endpoints of the edge, not at every vertex of the polyhedron. This
is the more general (weaker-hypothesis), and more precisely source-matching,
choice — see `Thm_Hirsch_simple_polyhedron_target_distance_lower_bound.lean`
for the companion corollary, which genuinely does need the global hypothesis
because its argument walks an entire path of possibly many vertices. -/

open scoped RealInnerProductSpace

namespace Hirsch

/-- If `v` and `w` are both simple vertices of `Hpoly a b` and are adjacent,
they share exactly `d - 1` tight rows (equivalently: each has exactly one
tight row the other lacks). -/
theorem simple_vertex_adjacent_tight_inter_card
    {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (v w : EuclideanSpace ℝ (Fin d))
    (hv : IsSimpleVertex a b v) (hw : IsSimpleVertex a b w)
    (hadj : Adj (Hpoly a b) v w) :
    (TightSet a b v ∩ TightSet a b w).ncard = d - 1 := by sorry

end Hirsch