Finite-nine N4d Form B branch contradictions

Proved

Erdos9796FiniteNine.n4d_formb_branch

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

discrete-geometryerdos-97finite-nineproof-transfer

For every nine-point endpoint configuration in which each cap interior contains exactly two points, eight geometric contradictions rule out the interior-point/opposite-vertex witness pattern.

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_N4dFormBBranchSupport

open scoped EuclideanGeometry

/-- The middle N4e slice supplies the branch conclusions used by the final Form B proof. -/

Formal statement

theorem Erdos9796FiniteNine.n4d_formb_branch {A : Finset ℝ²}
    (S : Batch3N9.Problem97.FiniteEndpointShell A)
    (Z : Batch3N9.Problem97.FiniteEndpointShell.ZeroDefectCapLayout S) :
    Nonempty
      (Batch3N9.Problem97.FiniteEndpointShell.N4dFormBBranchSupport S Z) := by
  sorry

Source

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

View graph