Finite-nine N4 cap containment

Proved

Erdos9796FiniteNine.cap_containment

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

discrete-geometryerdos-97finite-nineproof-transfer

The nine escaped-form exclusions force every relevant four-point distance fiber into the corresponding endpoint cap.

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_N8Interface

/-! Statement-only transfer node for finite-nine N4 cap containment.

SKETCH — NOT PROMOTABLE. The source project already proves this result; the proof
solution will be transferred separately after this public theorem node exists.
-/

open scoped EuclideanGeometry

Formal statement

theorem Erdos9796FiniteNine.cap_containment {A : Finset ℝ²}
    (S : Batch3N9.Problem97.FiniteEndpointShell A)
    (hA1 : S.N4dExcludesFormA_v1) (hB1 : S.N4dExcludesFormB_v1)
    (hC1 : S.N4dExcludesFormC_v1) (hB2 : S.N4dExcludesFormB_v2)
    (hcyclic : S.N4dExcludesFormA_v2 ∧ S.N4dExcludesFormC_v2 ∧
      S.N4dExcludesFormA_v3 ∧ S.N4dExcludesFormB_v3 ∧ S.N4dExcludesFormC_v3) :
    S.N4eCapContainment := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/tree/6e3e2a849c67f518d75fd45a09a201a6c8f4cd8f/lean/Erdos9796Proof/P97/N9Endpoint

View graph