Exceptional anchors from singular points

Definition

Esgk_SelfCurveExceptionalAnchors

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

This selects first-sample anchors that are singular points of the polynomial chosen for the second supporting curve. It then adjoins a separately specified set of exceptional axis anchors.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_AuxiliaryCircleNoncontainment
import Definitions.Def_Esgk_AuxiliaryIncidenceDeletion
import Definitions.Def_Esgk_PachDeZeeuwQuadraticDegree
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Definitions.Def_LeanFormalizations_PachDeZeeuw_Basic
import Definitions.Def_LeanFormalizations_PachDeZeeuw_Bezout
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CurveInterface
import Mathlib

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


namespace Esgk

open EuclideanGeometry PachDeZeeuw PachDeZeeuw.Algebraic

 
noncomputable def selfCurveSingularAnchors {d : ℕ}
    (X : PreparedBipartiteInput d) : Finset X.P₁ := by
  classical
  exact Finset.univ.filter fun p ↦
    (p : PachDeZeeuw.Algebraic.Point2) ∈
      SingularPointSet (preparedSecondCurvePolynomial X)


noncomputable def selfCurveExceptionalAnchors {d : ℕ}
    (X : PreparedBipartiteInput d) (axisAnchors : Finset X.P₁) : Finset X.P₁ := by
  classical
  exact selfCurveSingularAnchors X ∪ axisAnchors


end Esgk

View graph