A shared-scalar subspace obstructs cone-covering by invertible linear images

Proved

Hirsch.cone_covering_shared_subspace_obstruction

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

convex-geometryhirsch-conjecturelinear-algebra

Let $C\subseteq E$ be a salient cone (contains no line through the origin — the classical convex-geometry meaning of "pointed cone"; not Mathlib's unrelated ConvexCone.Pointed, which only asserts $0\in C$ ), $U\ne0$ a subspace, and $S:\iota\to E\simeq_{\mathbb R}E$ a family of invertible linear maps over an arbitrary index type $\iota$ with a distinguished basepoint $i_0$ , such that every $S_i$ agrees with $S_{i_0}$ up to a positive scalar $\sigma_i$ on all of $U$ : $S_i(u)=\sigma_i\,S_{i_0}(u)$ for $u\in U$ . Then

\Bigl(\bigcup_i S_i(C)\Bigr)\cap S_{i_0}(U)=S_{i_0}(C\cap U)\subsetneq S_{i_0}(U).

In words: the union of the copies $S_i(C)$ can never cover the image of the shared axis $U$ under $S_{i_0}$ — it only reaches the (proper) sub-cone $S_{i_0}(C\cap U)$ . This is a general, elementary, four-line linear-algebra obstruction: it is the exact mathematical reason a "shared-axis rotation family" construction (as used to realize an explicit one-column Black–Xue-style diameter bound) can never satisfy a genuine cone-covering hypothesis such as Black–Xue's Theorem 3.14, for any number of copies $\iota$ and any ambient dimension.

Formalization Note Stated over an arbitrary index type $\iota$ (not Fin m), so it needs no artificial finiteness or nonemptiness side-condition on the number of copies beyond having the distinguished basepoint $i_0$ ; this generalization is exactly the content of the source's proof, which uses nothing about the specific rotations beyond the stated hypotheses.

Preamble

import Mathlib

/-!
# Shared-subspace obstruction to cone covering (Black–Xue campaign "Lemma R2")

Source: `hirsch-campaign/route1/covering_referee_kimi/review.md` §4, Lemma R2
(independently re-derived and referee-verified there; a four-line general
argument in elementary linear algebra, needing no Black–Xue construction).

If invertible linear maps `S i` all agree with a fixed one `S i₀` up to a
positive per-copy scalar on a common nonzero subspace `U`, then the union of
the images `S i '' C` of any *salient* cone `C` (one containing no line
through the origin — Mathlib's `ConvexCone.Salient`, the standard convex-
geometry meaning of "pointed cone") can never cover all of `S i₀ '' U`: its
intersection with that image is exactly `S i₀ '' (C ∩ U)`, a proper subset of
`S i₀ '' U`. This is the exact mathematical reason a "shared axis" rotation
family (Astra's Lemma 10 in the one-column Black–Xue realization) is
incompatible with Theorem 3.14's genuine full-dimensional cone-covering
hypothesis, for any number of copies and any dimension `d ≥ 2`.
-/

Formal statement

namespace Hirsch

theorem cone_covering_shared_subspace_obstruction
    {E : Type*} [AddCommGroup E] [Module ℝ E] {ι : Type*}
    (C : ConvexCone ℝ E) (hC : C.Salient)
    (U : Submodule ℝ E) (hU : U ≠ ⊥)
    (S : ι → E ≃ₗ[ℝ] E) (i₀ : ι) (σ : ι → ℝ) (hσ : ∀ i, 0 < σ i)
    (hSU : ∀ i, ∀ u ∈ U, S i u = σ i • S i₀ u) :
    (⋃ i, (S i : E → E) '' (C : Set E)) ∩ ((S i₀ : E → E) '' (U : Set E))
        = (S i₀ : E → E) '' ((C : Set E) ∩ (U : Set E))
      ∧ (S i₀ : E → E) '' ((C : Set E) ∩ (U : Set E)) ⊂ (S i₀ : E → E) '' (U : Set E) := by
  sorry

end Hirsch

Source

hirsch-campaign/route1/covering_referee_kimi/review.md §4 (Black-Xue covering-family repair campaign, 2026-09-13) (Lemma R2, independently re-derived and referee-verified there)

View graph