Auxiliary incidence bound at every scale
ProvedEsgk.maximally_circular_raw_auxiliary_incidence_boundThere is an absolute positive integer with the following property.
Let be an irreducible and absolutely irreducible real plane polynomial of degree , with real zero set . Assume that is not a circle factor and is maximally circular: its local order at each of the two complex circular points at infinity is . Let be finite and put .
Take any incidence configuration whose two carrier sets are both , each represented by an irreducible real polynomial of degree at most . Its finite point sets are subsets of and form a disjoint split . The carrier is neither a line nor a circle: in particular neither copy is a vertical line, the pair is neither parallel lines, perpendicular lines, nor concentric circles, and the conditional restrictions on line or circle carriers hold automatically. Assume
Let count ordered pairs of a label and a target satisfying . For every integer ,
The constant is independent of the polynomial, sample, incidence configuration, and scale. The balanced cell-cover construction supplies such a configuration for every sample with .
import Definitions.Def_Esgk_MaximallyCircularQuarticFromIncidence open Esgk
theorem Esgk.maximally_circular_raw_auxiliary_incidence_bound :
MaximallyCircularRawAuxiliaryIncidenceStatement := by sorry