Lemma 4, proof — noninterior cone point has a separating normal

Proved

McFadden1974.QPTest.noninterior_gives_separator

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

conditional-logitconvex-geometrylinear-optimizationp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $C$ be the cone generated by all $w_{nij}$ . If zero is outside its interior, a nonzero vector $\gamma$ separates zero from the cone:

\exists\gamma\ne0\quad\forall n,i,j,\quad w_{nij}\cdot\gamma\leq0.

Consequently Axiom 6 fails. This is the separation step used to complete Lemma 4.

Formalization Note Interiority is taken in the ambient Euclidean space $\mathbb R^K$ .

Preamble

import Definitions.Def_McFadden1974_QPTest_ChoiceData

set_option autoImplicit false

Formal statement

namespace McFadden1974.QPTest

/-- McFadden (1974), p. 117 (PDF 13), Lemma 4, proof, final paragraph.
Failure of interiority gives a nonzero separating normal, so Axiom 6 fails.
The cone uses every ordered index triple in equation (22). -/
theorem noninterior_gives_separator {N K : ℕ} (d : ChoiceData N K)
    (h : (0 : EuclideanSpace ℝ (Fin K)) ∉ interior d.coneSet) :
    (∃ γ : EuclideanSpace ℝ (Fin K), γ ≠ 0 ∧
      ∀ n i j, inner ℝ (d.w n i j) γ ≤ 0) ∧ ¬ d.Axiom6 := by sorry

end McFadden1974.QPTest

Source

McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press (1974), p. 117, Lemma 4, proof, final paragraph (PDF p. 13)

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph