Properly separated polytope gluing (cap onto a simple vertex)

Definition

Hirsch_properly_separated_gluing

by elmismisimoxhunca · Sep 19, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-geometryhirsch-conjecturepolytopes

For a polyhedron $P=\mathrm{Hpoly}(a,b)\subseteq\mathbb R^d$ with a vertex $v$ , and a second polyhedron ("cap") $Q=\mathrm{Hpoly}(a',b')\subseteq\mathbb R^d$ , the gluing of $Q$ onto $P$ at $v$ is properly separated ( $\mathrm{ProperlySeparatedGluing}$ ) if all four hold: (1) every facet normal $a'_k$ of $Q$ is a strictly positive combination of exactly the rows of $P$ tight at $v$ (i.e. lies in the interior of $P$ 's normal cone at $v$ , given $v$ simple); (2) every extreme point of $Q$ lies strictly inside $P$ (strictly satisfies every row of $P$ ); (3) every extreme point of $P$ other than $v$ strictly satisfies every facet inequality of $Q$ ; (4) $v\notin Q$ (violates some facet inequality of $Q$ ).

This is the hypothesis bundle for the cap-gluing composition/diameter lemma (cap_gluing_diameter_composition), copied verbatim (clause by clause) from the source's own "Definition — properly separated gluing". $P$ , $Q$ are arbitrary H-presented polyhedra of arbitrary facet counts; nothing Black–Xue-, Goldfarb-, or covering-specific appears in any clause.

Formalization Note This definition does not assume $v$ is a simple vertex of $P$ — that hypothesis ( $\mathrm{IsSimpleVertex}$ ) is supplied separately wherever this definition is used, since condition (1)'s "interior of the normal cone" reading of $\mathrm{IsPositiveCombinationOfTightRows}$ only holds when $v$ is simple.

Definition code

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_simple_vertex

/-!
# Properly separated polytope gluing

Formalizes the hypothesis bundle for the flagship triage report's top-priority general
result, A1 ("Cap-gluing diameter/composition lemma", `PROVED-GENERAL, all D`): gluing a
cap `Q` onto a pointed full-dimensional polyhedron `P` at a simple vertex `v`.

Source (verbatim structure): `route1/shortcut_astra/attempt.md` §2, "Definition —
properly separated gluing": "Let `P` be the current pointed full-dimensional polyhedron,
`v` its simple top, and `Q` the placed cap. Write `R = P ∩ Q`. The gluing is properly
separated if: 1. every cap normal lies in `int N_P(v)`; 2. all finite cap vertices lie
strictly inside `P`; 3. every old vertex other than `v` strictly satisfies every cap
inequality; 4. `v ∉ Q`." Independently re-derived and used unchanged (per the triage
report Part A1) by `shortcut_sol`, `shortcut_kimi`, `flagship_decomposition` §4, and
`flagship_actual_distance` §4 — the "cube cap" / Goldfarb-specific framing used in some
of those files is inessential, since none of the four conditions below mention any
Black–Xue- or Goldfarb-specific structure; `Q` is an arbitrary polyhedron.

`P` and `Q` are both given in H-presentation (`Hpoly`, `Def_Hirsch_model.lean`):
`P = Hpoly a b` with `n` facets, `Q = Hpoly a' b'` with `n'` facets, both in
`EuclideanSpace ℝ (Fin d)`.

Frame-audit note: this definition does **not** assume `v` is a simple vertex of `P` (that
is `IsSimpleVertex a b v` from `Def_Hirsch_simple_vertex.lean`, supplied separately as a
hypothesis wherever this definition is used) — condition 1 below is stated using
`IsPositiveCombinationOfTightRows`, which equals "interior of the normal cone of `P` at
`v`" exactly when `v` is simple. Baking simplicity into this definition would be an
unjustified hidden hypothesis; keeping it external matches this workspace's convention
(cf. `Hpoly`'s docstring: "Boundedness and nonemptiness are not part of the definition;
theorems assume them explicitly").
-/

open scoped RealInnerProductSpace

namespace Hirsch

/-- **Properly separated gluing** of the cap `Q = Hpoly a' b'` onto `P = Hpoly a b` at the
vertex `v`, exactly as defined in `shortcut_astra/attempt.md` §2:

1. every facet normal `a' k` of `Q` is a strictly positive combination of exactly the
   rows of `P` tight at `v` (i.e. lies in the interior of the normal cone of `P` at `v`,
   given `v` is simple);
2. every extreme point (finite vertex) of `Q` lies strictly inside `P`;
3. every extreme point of `P` other than `v` strictly satisfies every facet inequality
   of `Q`;
4. `v` itself violates at least one facet inequality of `Q`, i.e. `v ∉ Q`. -/
def ProperlySeparatedGluing {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)) : Prop :=
  (∀ k, IsPositiveCombinationOfTightRows a b v (a' k)) ∧
  (∀ q ∈ Set.extremePoints ℝ (Hpoly a' b'), ∀ i, ⟪a i, q⟫ < b i) ∧
  (∀ u ∈ Set.extremePoints ℝ (Hpoly a b), u ≠ v → ∀ k, ⟪a' k, u⟫ < b' k) ∧
  v ∉ Hpoly a' b'

end Hirsch

Source

hirsch-campaign/route1/flagship_triage_report.md, Part A1/A2/A3; hirsch-campaign/route1/shortcut_astra/attempt.md §2 (Definition — properly separated gluing, quoted verbatim)

View graph