Auxiliary point-pair and curve-pair incidence

Definition

Esgk_MaximallyCircularAuxiliaryCodegree

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

finite-combinatoricsincidence-geometry

This defines the auxiliary incidence relation between a pair of points and a pair of curve labels in a prepared bipartite configuration.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_AuxiliaryIncidenceDeletion
import Definitions.Def_Esgk_FiniteIncidenceCodegreeBound
import Definitions.Def_Esgk_IrreduciblePlaneFunctionField
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AuxiliaryCurves
import Definitions.Def_LeanFormalizations_PachDeZeeuw_Basic
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.
-/


noncomputable section

open scoped Classical

namespace Esgk

open PachDeZeeuw (PreparedBipartiteInput auxCurve)
open PachDeZeeuw.Algebraic (PlanePoly PlaneCurveZeroSet)
open IrreduciblePlanePolynomial

 
def auxPointPairCurveIncidence {d : ℕ} (X : PreparedBipartiteInput d)
    (pq : X.P₂ × X.P₂) (ij : X.P₁ × X.P₁) : Prop :=
  encodedAuxPoint
      ((pq.1 : PachDeZeeuw.Algebraic.Point2),
        (pq.2 : PachDeZeeuw.Algebraic.Point2)) ∈ auxCurve X ij.1 ij.2


end Esgk

View graph