Diameter composition bound for a properly separated polytope gluing

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

/-!
# Cap-gluing diameter composition lemma

Source: `hirsch-campaign/route1/shortcut_astra/attempt.md` Lemma 16 ("Sol's
diameter overhead, with all seams included"), the top-priority general result
of the flagship triage report (Part A1, "PROVED-GENERAL, all D — TOP
PRIORITY"), independently re-derived by five lanes (`shortcut_sol`,
`shortcut_kimi`, `shortcut_astra`, refereed PROVED by `shortcut_astra_review`,
and reconfirmed general-purpose by `flagship_decomposition` §4).

**Exact source statement** (Lemma 16): "For a properly separated gluing, let
`Δ` be the finite graph diameter of the old polyhedron, `b` the finite cap
graph diameter, and `r` an all-seam-to-cap routing bound. Then
`diam(P ∩ Q) ≤ Δ + 2r + b`."

**Frame audit, hypothesis by hypothesis.**

* `v` "its simple top": §2's definition of properly separated gluing opens
  "Let `P` be the current pointed full-dimensional polyhedron, `v` its simple
  top" — `v` being simple (`IsSimpleVertex a b v`) is a *standing* assumption
  of the whole section, not just of the gluing definition itself, and is kept
  as an explicit hypothesis here for that reason (Phase 2's
  `Def_Hirsch_properly_separated_gluing.lean` deliberately does *not* bake
  simplicity into `ProperlySeparatedGluing` itself — its own docstring notes
  "this definition does not assume `v` is a simple vertex of `P`... supplied
  separately as a hypothesis wherever this definition is used" — so Phase 3
  must supply it here, and does).
* "properly separated gluing": `ProperlySeparatedGluing a b a' b' v`, reused
  unchanged from Phase 2 (frame-audited there clause-by-clause against this
  same source file).
* "`Δ` the finite graph diameter of the old polyhedron": `DiamLE (Hpoly a b) Δ`.
* "`b` the finite cap graph diameter": `DiamLE (Hpoly a' b') bcap` (renamed to
  avoid clashing with the ambient RHS-vector variable `b`).
* "`r` an all-seam-to-cap routing bound": Theorem 15 (which supplies `r` in
  every application of Lemma 16 in this corpus) proves the routing bound for
  **every finite local vertex**, i.e. every vertex of `R = P ∩ Q` that is
  *not* a retained old vertex other than `v` — Lemma 4's exact
  characterization is "the entire new finite vertex set is the retained old
  set (old vertices minus `v`) together with `V(W)`" (the local model). This
  is intentionally **not** strengthened to "every vertex of `R`": that
  stronger statement is false in general (a retained old vertex arbitrarily
  far from `v` inside a large `P` need not be within `r` steps of the cap,
  and indeed Lemma 16's own conclusion `Δ + 2r + b` only makes sense because
  `Δ` — not `r` — accounts for old-to-old travel). The hypothesis `hr` below
  is exactly this scope: it quantifies only over `x ∈ extremePoints R` with
  `x ∉ extremePoints (Hpoly a b)` (a "new" vertex of `R`), matching Lemma
  4/Theorem 15's scope precisely, and represented via `Hirsch.Reach` from
  `Def_Hirsch_walk.lean` (a length-`r` walk in `R`'s own vertex-edge graph),
  reusing existing vocabulary rather than introducing a new access predicate.
-/

open scoped RealInnerProductSpace

namespace Hirsch

/-- Composing a properly separated gluing: if `P = Hpoly a b` has diameter at
most `Δ`, the cap `Q = Hpoly a' b'` has diameter at most `bcap`, and every
"new" vertex of `R = P ∩ Q` (one that is not a retained old vertex of `P`)
reaches some vertex of `Q` within `r` steps inside `R`'s own graph, then
`R`'s diameter is at most `Δ + 2r + bcap`. -/
theorem cap_gluing_diameter_composition
    {d n n' : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (a' : Fin n' → EuclideanSpace ℝ (Fin d)) (b' : Fin n' → ℝ)
    (v : EuclideanSpace ℝ (Fin d))
    (hv : IsSimpleVertex a b v)
    (hglue : ProperlySeparatedGluing a b a' b' v)
    (Δ bcap r : ℕ)
    (hΔ : DiamLE (Hpoly a b) Δ)
    (hbcap : DiamLE (Hpoly a' b') bcap)
    (hr : ∀ x ∈ Set.extremePoints ℝ (Hpoly a b ∩ Hpoly a' b'),
            x ∉ Set.extremePoints ℝ (Hpoly a b) →
            ∃ q ∈ Set.extremePoints ℝ (Hpoly a' b'),
              Reach (Hpoly a b ∩ Hpoly a' b') r x q) :
    DiamLE (Hpoly a b ∩ Hpoly a' b') (Δ + 2 * r + bcap) := by sorry

end Hirsch