Finite-nine N4e core support

Proved

Erdos9796FiniteNine.n4e_core

by mysticflounder · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-geometryerdos-97finite-nineproof-transfer

Every finite nine-point endpoint shell has the explicit N4e core-support packet used by the later escaped-form branch proofs.

Preamble

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under GPL-3.0-or-later as described in the file LICENSE.
Authors: Adam McKenna
-/

import Definitions.Def_Erdos9796FiniteNine_N4dPackets

open scoped EuclideanGeometry

/-- The first N4e slice supplies the explicit interface used by later branch proofs. -/

Formal statement

theorem Erdos9796FiniteNine.n4e_core {A : Finset ℝ²}
    (S : Batch3N9.Problem97.FiniteEndpointShell A) :
    Nonempty (Batch3N9.Problem97.FiniteEndpointShell.N4eCoreSupport S) := by
  sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/0707e2c26e2e570e2b56ce656242cf5dec4d2584/lean/Erdos9796Proof/P97/N9Endpoint/N4e.lean

View graph