Counting divisors with a given tangent pattern

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Blowup.Directions7import SurfaceBlowup.Measure.AdicTransport8import SurfaceBlowup.Formula.FiniteFieldCounts9import SurfaceBlowup.Formula.StateCombinatorics10 11/-!12# Counting divisors with a given tangent pattern13 14Over a finite field `k`, the exceptional divisors realizing a tangent pattern `P` of a state15`s` are in bijection with tuples of colorings of the nonboundary closed directions (one16coloring per degree), which yields the closed formula `#patternDivisors = tangentCount(q)`17with `q = #k`. Consequences: tangent counts and state-law coefficients are nonnegative at18prime powers. The file also records the count of nonboundary closed directions of each degree19and a continuity criterion for congruence-compatible maps.20 21## Main results22 23* `SurfaceBlowup.nonboundary_direction_count`: number of nonboundary directions of degree `δ`.24* `SurfaceBlowup.patternDivisors_equiv_colorings`: divisors with pattern `P` ≃ colorings.25* `SurfaceBlowup.pattern_divisor_count`: `#patternDivisors k s P = tangentCount s P (#k)`.26* `SurfaceBlowup.tangent_count_nonneg`, `SurfaceBlowup.state_law_coeff_nonneg`.27* `SurfaceBlowup.continuousOn_of_congruence_compatible`.28 29Provenance: `Thm_SurfaceBlowupV2_{nonboundary_direction_count,30pattern_divisors_equiv_colorings_v2, pattern_divisor_count, tangent_count_nonneg,31state_law_coeff_nonneg, continuousOn_of_congruence_compatible}` (the second inlines the proof32of `divisor_degree_pattern_weight`).33-/34 35open scoped BigOperators ENNReal36 37namespace SurfaceBlowup38 39/-- Over a finite field `k`, the number of nonboundary closed directions of degree `δ > 0` is40the value at `q = #k` of `availablePoints` (with offset `-1` at a crossing state, where the41zero direction is also boundary). -/42theorem nonboundary_direction_count (k : Type) [Field k] [Finite k] (s : State) (δ : ℕ)(6.3)43    (hδ : 0 < δ) :44    ((Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧45        directionDegree k Q = δ} : ℕ) : ℚ) =46      (availablePoints47        (match s with | State.single _ _ => (0 : ℤ) | State.crossing _ _ _ _ => (-1 : ℤ))48        δ).eval (Nat.card k) := by49  have hN := finite_field_irreducible_count k δ hδ50  have hp1 : (pointCount 1).eval (Nat.card k) = (Nat.card k : ℚ) := by51    simp [pointCount, Expr.sum, Expr.eval, Expr.pow]52  set C : Prop := ((s matches State.crossing _ _ _ _) = true) with hC53  set T : Set (Polynomial k) :=54    {g | (g.Monic ∧ Irreducible g ∧ g.natDegree = δ) ∧ (C → g ≠ Polynomial.X)} with hT55  have hcard : Nat.card {Q : ClosedDirection k //56      Q ∉ boundaryDirections k s ∧ directionDegree k Q = δ} = Set.ncard T := by57    rw [← Nat.card_coe_set_eq]58    let f : T → {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧ directionDegree k Q = δ} :=59      fun g ↦ ⟨some ⟨g.1, g.2.1.1, g.2.1.2.1⟩, by60        obtain ⟨g, ⟨hm, hi, hd⟩, hx⟩ := g61        refine ⟨?_, hd⟩62        cases s <;> simp_all [boundaryDirections, infinityDirection, zeroDirection, C]⟩63    refine (Nat.card_congr (Equiv.ofBijective f ⟨?_, ?_⟩)).symm64    · rintro ⟨g, hg⟩ ⟨g', hg'⟩ h65      simp only [f, Subtype.mk.injEq, Option.some.injEq] at h66      exact Subtype.ext h67    · rintro ⟨Q, hQ, hd⟩68      cases Q with69      | none => cases s <;> simp [boundaryDirections, infinityDirection] at hQ70      | some φ =>71        refine ⟨⟨φ.1, ⟨φ.2.1, φ.2.2, hd⟩, fun hc h ↦ hQ ?_⟩, rfl⟩72        cases s73        · simp [C] at hc74        · exact Or.inr (congrArg some (Subtype.ext h))75  rw [hcard]76  set A : Set (Polynomial k) := {g | g.Monic ∧ Irreducible g ∧ g.natDegree = δ} with hA77  have hNA : ((Set.ncard A : ℕ) : ℚ) = (pointCount δ).eval (Nat.card k) := by78    rw [← Nat.card_coe_set_eq]; exact hN79  by_cases h1 : δ = 180  · subst h181    have hq : ((Set.ncard A : ℕ) : ℚ) = Nat.card k := by rw [hNA, hp1]82    cases s with83    | single a c =>84      have : T = A := by ext g; simp [T, A, C]85      rw [this, hq]; simp [availablePoints, Expr.eval]86    | crossing a b c h =>87      have hTA : T = A \ {Polynomial.X} := by ext g; simp [T, A, C]88      have hXA : Polynomial.X ∈ A :=89        ⟨Polynomial.monic_X, Polynomial.irreducible_X, Polynomial.natDegree_X⟩90      have hfin : A.Finite := Set.finite_of_ncard_pos (by91        have : (0 : ℚ) < (Set.ncard A : ℕ) := by rw [hq]; exact_mod_cast Nat.card_pos92        exact_mod_cast this)93      have := Set.ncard_sdiff_singleton_add_one hXA hfin94      have h2 : ((Set.ncard (A \ {Polynomial.X}) : ℕ) : ℚ) + 1 = Nat.card k := by95        rw [← hq]; exact_mod_cast this96      rw [hTA]97      simp [availablePoints, Expr.eval]; linarith98  · have : T = A := by99      ext g100      simp only [T, A, Set.mem_ofPred_eq, and_iff_left_iff_imp]101      rintro ⟨-, -, hd⟩ - rfl102      exact h1 (hd ▸ Polynomial.natDegree_X)103    rw [this, hNA]; simp [availablePoints, h1]104 105/-! ### Divisors with a given pattern and colorings106 107The statement `patternDivisors_equiv_colorings` carries the extra hypothesis `hrx`108(`P.rx = 0` at a single state), the clause of `Allowed s P` that `HasPattern` does not carry;109without it the bijection fails. -/110 111section Colorings112 113variable (k : Type) [Field k]114 115/-- Every closed direction has positive degree. -/116theorem directionDegree_pos (Q : ClosedDirection k) : 0 < directionDegree k Q := by117  cases Q with118  | none => simp [directionDegree]119  | some φ => exact φ.property.2.natDegree_pos120 121private theorem inf_mem_bdry (s : State) : infinityDirection k ∈ boundaryDirections k s := by122  cases s <;> simp [boundaryDirections]123 124private theorem zero_ne_inf : zeroDirection k ≠ infinityDirection k := by125  simp [zeroDirection, infinityDirection]126 127private theorem mem_bdry_single (a c : ℕ) (Q : ClosedDirection k) :128    Q ∈ boundaryDirections k (State.single a c) ↔ Q = infinityDirection k := by129  simp [boundaryDirections]130 131private theorem mem_bdry_crossing (a b c h : ℕ) (Q : ClosedDirection k) :132    Q ∈ boundaryDirections k (State.crossing a b c h) ↔133      Q = infinityDirection k ∨ Q = zeroDirection k := by134  simp [boundaryDirections]135 136private theorem deg_of_mem_bdry (s : State) (Q : ClosedDirection k)137    (hQ : Q ∈ boundaryDirections k s) : directionDegree k Q = 1 := by138  cases s with139  | single a c =>140    rw [mem_bdry_single] at hQ141    subst hQ; rfl142  | crossing a b c h =>143    rcases (mem_bdry_crossing k a b c h Q).1 hQ with rfl | rfl144    · rfl145    · simp [directionDegree, zeroDirection]146 147/-- Closed directions of bounded degree over a finite field are finite. -/148private theorem finite_directionDegree_le [Finite k] (n : ℕ) :149    Finite {Q : ClosedDirection k // directionDegree k Q ≤ n} := by150  let f : {Q : ClosedDirection k // directionDegree k Q ≤ n} → Option (Fin (n+1) → k) :=151    fun Q ↦ Option.map (fun φ : AffineDirection k ↦ fun i : Fin (n+1) ↦ φ.val.coeff i) Q.1152  refine Finite.of_injective f ?_153  rintro ⟨Q, hQ⟩ ⟨Q', hQ'⟩ h154  apply Subtype.ext155  simp only [f] at h156  cases Q with157  | none =>158    cases Q' with159    | none => rfl160    | some _ => simp at h161  | some φ =>162    cases Q' with163    | none => simp at h164    | some ψ =>165      simp only [Option.map_some, Option.some.injEq] at h166      refine congrArg some (Subtype.ext (Polynomial.ext fun i ↦ ?_))167      by_cases hi : i < n + 1168      · exact congrFun h ⟨i, hi⟩169      · have h1 : φ.val.natDegree < i := by simp [directionDegree] at hQ; omega170        have h2 : ψ.val.natDegree < i := by simp [directionDegree] at hQ'; omega171        rw [Polynomial.coeff_eq_zero_of_natDegree_lt h1,172          Polynomial.coeff_eq_zero_of_natDegree_lt h2]173 174/-- The nonboundary points of degree `i + 1`. -/175private abbrev Pt (s : State) (i : Fin s.degree) : Type :=176  {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧ directionDegree k Q = i.val + 1}177 178/-- Colorings of the degree-`(i + 1)` nonboundary points with the prescribed counts. -/179private abbrev Col (s : State) (P : TangentPattern s.degree) (i : Fin s.degree) : Type :=180  {f : Pt k s i → Option (Fin s.degree) //181    ∀ j : Fin s.degree, Nat.card {Q // f Q = some j} = (P.other (i, j)).val}182 183private theorem card_fiber_eq (s : State) (D : ExceptionalDivisor k) (i j : Fin s.degree)184    (f : Pt k s i → Option (Fin s.degree))185    (hf : ∀ Q : Pt k s i, f Q = some j ↔ D Q.1 = j.val + 1) :186    Nat.card {Q : Pt k s i // f Q = some j} =187      Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧188        directionDegree k Q = i.val + 1 ∧ D Q = j.val + 1} :=189  Nat.card_congr190    { toFun := fun Q ↦ ⟨Q.1.1, Q.1.2.1, Q.1.2.2, (hf Q.1).1 Q.2⟩191      invFun := fun Q ↦ ⟨⟨Q.1, Q.2.1, Q.2.2.1⟩, (hf _).2 Q.2.2.2⟩192      left_inv := fun _ ↦ rfl193      right_inv := fun _ ↦ rfl }194 195/-! #### Forward direction: divisor → colorings -/196 197private theorem deg_mul_mult_le (s : State) (P : TangentPattern s.degree)198    (D : patternDivisors k s P) (Q : ClosedDirection k) :199    directionDegree k Q * D.1 Q ≤ s.degree := by200  have hdeg : exceptionalDegree k D.1 = P.d.val := D.2.1201  have h3 : P.d.val ≤ s.degree := Nat.lt_succ_iff.mp P.d.isLt202  by_cases hQ : D.1 Q = 0203  · simp [hQ]204  · have h1 : directionDegree k Q * D.1 Q ≤ exceptionalDegree k D.1 :=205      Finset.single_le_sum (f := fun P ↦ directionDegree k P * D.1 P)206        (fun _ _ ↦ Nat.zero_le _) (Finsupp.mem_support_iff.mpr hQ)207    omega208 209private theorem mult_le (s : State) (P : TangentPattern s.degree) (D : patternDivisors k s P)210    (Q : ClosedDirection k) : D.1 Q ≤ s.degree :=211  (Nat.le_mul_of_pos_left _ (directionDegree_pos k Q)).trans (deg_mul_mult_le k s P D Q)212 213private def toColFun (s : State) (P : TangentPattern s.degree) (D : patternDivisors k s P)214    (i : Fin s.degree) : Pt k s i → Option (Fin s.degree) :=215  fun Q ↦ if D.1 Q.1 = 0 then none216    else some ⟨D.1 Q.1 - 1, by have := mult_le k s P D Q.1; omega⟩217 218private theorem toColFun_eq_some_iff (s : State) (P : TangentPattern s.degree)219    (D : patternDivisors k s P) (i j : Fin s.degree) (Q : Pt k s i) :220    toColFun k s P D i Q = some j ↔ D.1 Q.1 = j.val + 1 := by221  unfold toColFun222  split_ifs with h223  · simp only [false_iff]; omega224  · simp only [Option.some.injEq, Fin.ext_iff]; omega225 226private def toCol (s : State) (P : TangentPattern s.degree) (D : patternDivisors k s P) :227    ∀ i : Fin s.degree, Col k s P i :=228  fun i ↦ ⟨toColFun k s P D i, fun j ↦ by229    rw [card_fiber_eq k s D.1 i j _ (toColFun_eq_some_iff k s P D i j)]230    exact D.2.2.2.2 (i, j)⟩231 232/-! #### Backward direction: colorings → divisor -/233 234private theorem coloring_congr (s : State) (P : TangentPattern s.degree)235    (F : ∀ i : Fin s.degree, Col k s P i) (i i' : Fin s.degree) (hii : i = i')236    (Q : ClosedDirection k) (hb : Q ∉ boundaryDirections k s)237    (h1 : directionDegree k Q = i.val + 1) (h2 : directionDegree k Q = i'.val + 1) :238    (F i).1 ⟨Q, hb, h1⟩ = (F i').1 ⟨Q, hb, h2⟩ := by239  subst hii; rfl240 241private theorem elim_le (n : ℕ) (o : Option (Fin n)) :242    Option.elim o 0 (fun j ↦ j.val + 1) ≤ n := by243  cases o with244  | none => exact Nat.zero_le _245  | some j => exact j.isLt246 247open scoped Classical in248/-- The multiplicity at `Q` of the divisor attached to a tuple of colorings. -/249private noncomputable def mult (s : State) (P : TangentPattern s.degree)250    (F : ∀ i : Fin s.degree, Col k s P i) (Q : ClosedDirection k) : ℕ :=251  if Q = infinityDirection k then P.rt.val252  else if hb : Q ∈ boundaryDirections k s then P.rx.val253  else if h : directionDegree k Q ≤ s.degree then254    Option.elim ((F ⟨directionDegree k Q - 1, by have := directionDegree_pos k Q; omega⟩).1255      ⟨Q, hb, (by have := directionDegree_pos k Q; omega :256        directionDegree k Q = directionDegree k Q - 1 + 1)⟩) 0 (fun j ↦ j.val + 1)257  else 0258 259private theorem mult_inf (s : State) (P : TangentPattern s.degree)260    (F : ∀ i : Fin s.degree, Col k s P i) :261    mult k s P F (infinityDirection k) = P.rt.val := by262  unfold mult; rw [if_pos rfl]263 264private theorem mult_zero_crossing (a b c h : ℕ)265    (P : TangentPattern (State.crossing a b c h).degree)266    (F : ∀ i : Fin (State.crossing a b c h).degree, Col k (State.crossing a b c h) P i) :267    mult k (State.crossing a b c h) P F (zeroDirection k) = P.rx.val := by268  unfold mult269  rw [if_neg (zero_ne_inf k), dif_pos ((mem_bdry_crossing k a b c h _).2 (Or.inr rfl))]270 271private theorem mult_nonbdry (s : State) (P : TangentPattern s.degree)272    (F : ∀ i : Fin s.degree, Col k s P i) (i : Fin s.degree) (Q : Pt k s i) :273    mult k s P F Q.1 = Option.elim ((F i).1 Q) 0 (fun j ↦ j.val + 1) := by274  obtain ⟨Q, hb, hQ⟩ := Q275  have hinf : Q ≠ infinityDirection k := fun h ↦ hb (h ▸ inf_mem_bdry k s)276  have hle : directionDegree k Q ≤ s.degree := by omega277  have hpos := directionDegree_pos k Q278  change mult k s P F Q = Option.elim ((F i).1 ⟨Q, hb, hQ⟩) 0 (fun j ↦ j.val + 1)279  unfold mult280  rw [if_neg hinf, dif_neg hb, dif_pos hle]281  congr 1282  exact coloring_congr k s P F ⟨directionDegree k Q - 1, by omega⟩ i283    (Fin.ext (by change directionDegree k Q - 1 = i.val; omega)) Q hb284    (by omega : directionDegree k Q = directionDegree k Q - 1 + 1) hQ285 286private theorem mult_support_finite [Finite k] (s : State) (P : TangentPattern s.degree)287    (F : ∀ i : Fin s.degree, Col k s P i) : (Function.support (mult k s P F)).Finite := by288  have hfin : Set.Finite {Q : ClosedDirection k | directionDegree k Q ≤ max 1 s.degree} :=289    Set.finite_coe_iff.mp (finite_directionDegree_le k (max 1 s.degree))290  refine hfin.subset fun Q hQ ↦ ?_291  rw [Function.mem_support] at hQ292  change directionDegree k Q ≤ max 1 s.degree293  unfold mult at hQ294  split_ifs at hQ with h1 h2 h3295  · subst h1; exact le_max_left _ _296  · rw [deg_of_mem_bdry k s Q h2]; exact le_max_left _ _297  · exact le_trans h3 (le_max_right _ _)298  · exact absurd rfl hQ299 300/-- The exceptional divisor attached to a tuple of colorings. -/301private noncomputable def toDiv [Finite k] (s : State) (P : TangentPattern s.degree)302    (F : ∀ i : Fin s.degree, Col k s P i) : ExceptionalDivisor k :=303  Finsupp.ofSupportFinite (mult k s P F) (mult_support_finite k s P F)304 305private theorem toDiv_apply [Finite k] (s : State) (P : TangentPattern s.degree)306    (F : ∀ i : Fin s.degree, Col k s P i) (Q : ClosedDirection k) :307    toDiv k s P F Q = mult k s P F Q := rfl308 309private theorem toDiv_some_iff [Finite k] (s : State) (P : TangentPattern s.degree)310    (F : ∀ i : Fin s.degree, Col k s P i) (i j : Fin s.degree) (Q : Pt k s i) :311    (F i).1 Q = some j ↔ toDiv k s P F Q.1 = j.val + 1 := by312  rw [toDiv_apply, mult_nonbdry k s P F i Q]313  cases (F i).1 Q with314  | none => simp315  | some j' => simp [Fin.ext_iff]316 317private theorem toDiv_card [Finite k] (s : State) (P : TangentPattern s.degree)318    (F : ∀ i : Fin s.degree, Col k s P i) (ij : Fin s.degree × Fin s.degree) :319    Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧320      directionDegree k Q = ij.1.val + 1 ∧ toDiv k s P F Q = ij.2.val + 1} =321        (P.other ij).val := by322  rw [← card_fiber_eq k s (toDiv k s P F) ij.1 ij.2 (F ij.1).1 (toDiv_some_iff k s P F ij.1 ij.2)]323  exact (F ij.1).2 ij.2324 325/-- Degree of an exceptional divisor of bounded degrees and multiplicities, split into the326boundary part and the pattern weight of its nonboundary part (the proof of the node327`divisor_degree_pattern_weight`). -/328private theorem degree_formula [Finite k] (s : State) (Dv : ExceptionalDivisor k) (n : ℕ)329    (hdeg : ∀ Q, 0 < Dv Q → directionDegree k Q ≤ n) (hmult : ∀ Q, Dv Q ≤ n) :330    exceptionalDegree k Dv = Dv (infinityDirection k) + (match s with331      | State.single _ _ => (0 : ℕ) | State.crossing _ _ _ _ => Dv (zeroDirection k)) +332      ∑ ij : Fin n × Fin n, (ij.1.val + 1) * (ij.2.val + 1) *333        Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧334          directionDegree k Q = ij.1.val + 1 ∧ Dv Q = ij.2.val + 1} := by335  classical336  obtain ⟨B, hB, hBsum⟩ : ∃ B : Finset (ClosedDirection k),337      (∀ Q, Q ∈ boundaryDirections k s ↔ Q ∈ B) ∧338      ∑ Q ∈ B, directionDegree k Q * Dv Q = Dv (infinityDirection k) +339        (match s with340          | State.single _ _ => (0 : ℕ) | State.crossing _ _ _ _ => Dv (zeroDirection k)) := by341    cases s with342    | single _ _ =>343      exact ⟨{infinityDirection k}, fun Q ↦ by simp [boundaryDirections],344        by simp [infinityDirection, directionDegree]⟩345    | crossing _ _ _ _ =>346      refine ⟨{infinityDirection k, zeroDirection k}, fun Q ↦ by simp [boundaryDirections], ?_⟩347      rw [Finset.sum_pair (by simp [infinityDirection, zeroDirection])]348      simp [infinityDirection, zeroDirection, directionDegree]349  set f : ClosedDirection k → ℕ := fun Q ↦ directionDegree k Q * Dv Q with hf350  change ∑ Q ∈ Dv.support, f Q = _351  rw [← Finset.sum_filter_add_sum_filter_not Dv.support (fun Q ↦ Q ∈ B)]352  congr 1353  · rw [← hBsum]354    refine Finset.sum_subset (fun Q hQ ↦ (Finset.mem_filter.1 hQ).2) fun Q hQB hQ ↦ ?_355    have : Dv Q = 0 := by356      by_contra h357      exact hQ (Finset.mem_filter.2 ⟨Finsupp.mem_support_iff.2 h, hQB⟩)358    simp [f, this]359  · rcases n with _ | m360    · simp [fun Q ↦ Nat.le_zero.1 (hmult Q)]361    · set g : ClosedDirection k → Fin (m+1) × Fin (m+1) :=362        fun Q ↦ (⟨(directionDegree k Q - 1) % (m+1), Nat.mod_lt _ (Nat.succ_pos _)⟩,363          ⟨(Dv Q - 1) % (m+1), Nat.mod_lt _ (Nat.succ_pos _)⟩)364      rw [← Finset.sum_fiberwise_of_maps_to (s := Dv.support.filter (fun Q ↦ Q ∉ B))365        (t := Finset.univ) (g := g) (fun _ _ ↦ Finset.mem_univ _)]366      refine Finset.sum_congr rfl fun ij _ ↦ ?_367      have hmem : ∀ Q, Q ∈ (Dv.support.filter (fun Q ↦ Q ∉ B)).filter (fun Q ↦ g Q = ij) ↔368          (Q ∉ boundaryDirections k s ∧ directionDegree k Q = ij.1.val + 1 ∧369            Dv Q = ij.2.val + 1) := by370        intro Q371        simp only [Finset.mem_filter, Finsupp.mem_support_iff, hB, g, Prod.ext_iff, Fin.ext_iff]372        have h1 := directionDegree_pos k Q373        constructor374        · rintro ⟨⟨hne, hnb⟩, ha, hb⟩375          have hd := hdeg Q (Nat.pos_of_ne_zero hne)376          have hm := hmult Q377          rw [Nat.mod_eq_of_lt (by omega)] at ha hb378          exact ⟨hnb, by omega, by omega⟩379        · rintro ⟨hnb, ha, hb⟩380          refine ⟨⟨by omega, hnb⟩, ?_, ?_⟩381          · rw [ha, Nat.add_sub_cancel, Nat.mod_eq_of_lt ij.1.2]382          · rw [hb, Nat.add_sub_cancel, Nat.mod_eq_of_lt ij.2.2]383      rw [Nat.card_congr (Equiv.subtypeEquivRight (fun Q ↦ (hmem Q).symm)),384        Nat.card_eq_finsetCard,385        Finset.sum_congr rfl (g := fun _ ↦ (ij.1.val + 1) * (ij.2.val + 1)),386        Finset.sum_const, smul_eq_mul, mul_comm]387      intro Q hQ388      obtain ⟨_, ha, hb⟩ := (hmem Q).1 hQ389      simp [f, ha, hb]390 391private theorem toDiv_hasPattern [Finite k] (s : State) (P : TangentPattern s.degree)392    (hP : P.rt.val + P.rx.val + patternWeight P.other = P.d.val)393    (hrx : ∀ a c, s = State.single a c → P.rx.val = 0)394    (F : ∀ i : Fin s.degree, Col k s P i) : HasPattern k s (toDiv k s P F) P := by395  have hdeg : ∀ Q, 0 < toDiv k s P F Q → directionDegree k Q ≤ s.degree := by396    intro Q hQ397    rw [toDiv_apply] at hQ398    unfold mult at hQ399    split_ifs at hQ with h1 h2 h3400    · subst h1401      change 1 ≤ s.degree402      have := P.rt.isLt; omega403    · rw [deg_of_mem_bdry k s Q h2]; have := P.rx.isLt; omega404    · exact h3405    · exact absurd hQ (lt_irrefl 0)406  have hmult : ∀ Q, toDiv k s P F Q ≤ s.degree := by407    intro Q408    rw [toDiv_apply]409    unfold mult410    split_ifs with h1 h2 h3411    · exact Nat.lt_succ_iff.mp P.rt.isLt412    · exact Nat.lt_succ_iff.mp P.rx.isLt413    · exact elim_le _ _414    · exact Nat.zero_le _415  have hsum : ∑ ij : Fin s.degree × Fin s.degree, (ij.1.val + 1) * (ij.2.val + 1) *416      Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧417        directionDegree k Q = ij.1.val + 1 ∧ toDiv k s P F Q = ij.2.val + 1} =418      patternWeight P.other :=419    Finset.sum_congr rfl fun ij _ ↦ by rw [toDiv_card k s P F ij]420  refine ⟨?_, mult_inf k s P F, ?_, toDiv_card k s P F⟩421  · rw [degree_formula k s (toDiv k s P F) s.degree hdeg hmult, hsum, toDiv_apply, mult_inf]422    cases s with423    | single a c =>424      have := hrx a c rfl425      change P.rt.val + 0 + patternWeight P.other = P.d.val426      omega427    | crossing a b c h =>428      change P.rt.val + toDiv k _ P F (zeroDirection k) + patternWeight P.other = P.d.val429      rwa [toDiv_apply, mult_zero_crossing]430  · cases s with431    | single a c => trivial432    | crossing a b c h =>433      change toDiv k _ P F (zeroDirection k) = P.rx.val434      rw [toDiv_apply, mult_zero_crossing]435 436/-! #### Round trips -/437 438private theorem toDiv_toCol [Finite k] (s : State) (P : TangentPattern s.degree)439    (D : patternDivisors k s P) : toDiv k s P (toCol k s P D) = D.1 := by440  ext Q441  rw [toDiv_apply]442  by_cases h1 : Q = infinityDirection k443  · subst h1; rw [mult_inf]; exact D.2.2.1.symm444  by_cases h2 : Q ∈ boundaryDirections k s445  · cases s with446    | single a c => exact absurd ((mem_bdry_single k a c Q).1 h2) h1447    | crossing a b c h =>448      rcases (mem_bdry_crossing k a b c h Q).1 h2 with rfl | rfl449      · exact absurd rfl h1450      · rw [mult_zero_crossing]451        exact D.2.2.2.1.symm452  by_cases h3 : directionDegree k Q ≤ s.degree453  · have hpos := directionDegree_pos k Q454    rw [mult_nonbdry k s P (toCol k s P D) ⟨directionDegree k Q - 1, by omega⟩455      ⟨Q, h2, (by omega : directionDegree k Q = directionDegree k Q - 1 + 1)⟩]456    unfold toCol toColFun457    dsimp only458    split_ifs with hz459    · simp only [Option.elim]; omega460    · simp only [Option.elim]461      change D.1 Q - 1 + 1 = D.1 Q462      omega463  · unfold mult464    rw [if_neg h1, dif_neg h2, dif_neg h3]465    by_contra hne466    have h4 := deg_mul_mult_le k s P D Q467    have h5 : directionDegree k Q ≤ directionDegree k Q * D.1 Q :=468      Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero (Ne.symm hne))469    omega470 471private theorem toCol_toDiv [Finite k] (s : State) (P : TangentPattern s.degree)472    (hP : P.rt.val + P.rx.val + patternWeight P.other = P.d.val)473    (hrx : ∀ a c, s = State.single a c → P.rx.val = 0)474    (F : ∀ i : Fin s.degree, Col k s P i) :475    toCol k s P ⟨toDiv k s P F, toDiv_hasPattern k s P hP hrx F⟩ = F := by476  funext i477  refine Subtype.ext (funext fun Q ↦ ?_)478  change toColFun k s P ⟨toDiv k s P F, toDiv_hasPattern k s P hP hrx F⟩ i Q = (F i).1 Q479  have hm : toDiv k s P F Q.1 = Option.elim ((F i).1 Q) 0 (fun j ↦ j.val + 1) :=480    mult_nonbdry k s P F i Q481  unfold toColFun482  cases hFQ : (F i).1 Q with483  | none =>484    rw [hFQ] at hm485    exact if_pos hm486  | some j =>487    rw [hFQ] at hm488    simp only [Option.elim] at hm489    rw [if_neg (by change toDiv k s P F Q.1 ≠ 0; omega)]490    exact congrArg some (Fin.ext (by change toDiv k s P F Q.1 - 1 = j.val; omega))491 492end Colorings493 494/-- Over a finite field, the exceptional divisors with tangent pattern `P` are in bijection495with tuples, indexed by degrees `i + 1`, of colorings of the nonboundary directions of that496degree by `Fin s.degree ⊕ none` with color counts `P.other (i, j)`. -/497theorem patternDivisors_equiv_colorings (k : Type) [Field k] [Finite k] (s : State)(6.3)498    (P : TangentPattern s.degree) (hP : P.rt.val + P.rx.val + patternWeight P.other = P.d.val)499    (hrx : ∀ a c, s = State.single a c → P.rx.val = 0) :500    Nonempty (patternDivisors k s P ≃ ∀ i : Fin s.degree,501      {f : {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧502          directionDegree k Q = i.val + 1} → Option (Fin s.degree) //503        ∀ j : Fin s.degree, Nat.card {Q // f Q = some j} = (P.other (i, j)).val}) :=504  ⟨{ toFun := toCol k s P505     invFun := fun F ↦ ⟨toDiv k s P F, toDiv_hasPattern k s P hP hrx F⟩506     left_inv := fun D ↦ Subtype.ext (toDiv_toCol k s P D)507     right_inv := fun F ↦ toCol_toDiv k s P hP hrx F }⟩508 509/-! ### Counting pattern divisors -/510 511/-- Number of colorings of a finite set `T` by `Fin r ⊕ none` with prescribed color counts512`m j`: a falling factorial over a product of factorials. -/513private theorem card_colorings (T : Type) [Finite T] (r : ℕ) (m : Fin r → ℕ) :514    ((Nat.card {f : T → Option (Fin r) // ∀ j : Fin r, Nat.card {x // f x = some j} = m j} :515        ℕ) : ℚ)516      = ((List.range (∑ i : Fin r, m i)).map fun j ↦ (Nat.card T : ℚ) - j).prod517          / ∏ i : Fin r, (Nat.factorial (m i) : ℚ) := by518  obtain e := Finite.equivFin T519  have hequiv : {f : T → Option (Fin r) // ∀ j : Fin r, Nat.card {x // f x = some j} = m j} ≃520      {f : Fin (Nat.card T) → Option (Fin r) //521        ∀ i : Fin r, Nat.card {x : Fin (Nat.card T) // f x = some i} = m i} := by522    refine Equiv.subtypeEquiv (Equiv.arrowCongr e (Equiv.refl _)) fun f ↦ forall_congr' fun j ↦ ?_523    rw [Nat.card_congr (e.subtypeEquiv (p := fun x ↦ f x = some j)524      (q := fun x ↦ (Equiv.arrowCongr e (Equiv.refl _) f) x = some j)525      fun x ↦ by simp [Equiv.arrowCongr_apply])]526  rw [Nat.card_congr hequiv, colored_subset_count]527 528/-- For an allowed pattern over a finite field `k`, there are finitely many divisors with529pattern `P`, and their number is `tangentCount s P` evaluated at `#k`. -/530theorem pattern_divisor_count (k : Type) [Field k] [Finite k] (s : State)(6.3)531    (P : TangentPattern s.degree) (hP : Allowed s P) :532    Finite (patternDivisors k s P) ∧533      ((Nat.card (patternDivisors k s P) : ℕ) : ℚ) = (tangentCount s P).eval (Nat.card k) := by534  obtain ⟨e⟩ := patternDivisors_equiv_colorings k s P hP.2.1535    (fun a c hs ↦ by subst hs; exact hP.2.2.2.1)536  have hfin : ∀ i : Fin s.degree, Finite537      {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧ directionDegree k Q = i.val + 1} :=538    fun i ↦ have := finite_directionDegree_le k (i.val + 1)539      Finite.of_injective (fun Q ↦ (⟨Q.1, Q.2.2.le⟩ : {Q // directionDegree k Q ≤ i.val + 1}))540        fun _ _ h ↦ Subtype.ext (Subtype.mk.inj h)541  refine ⟨Finite.of_equiv _ e.symm, ?_⟩542  rw [Nat.card_congr e, Nat.card_pi, Nat.cast_prod]543  unfold tangentCount divisorCount544  rw [expression_prod_eval, List.map_map, Finset.prod_map_toList]545  refine Finset.prod_congr rfl fun i _ ↦ ?_546  have := hfin i547  rw [card_colorings]548  simp only [Function.comp, Expr.eval, falling, expression_prod_eval, List.map_map]549  rw [nonboundary_direction_count k s (i.val + 1) (Nat.succ_pos _), div_eq_mul_one_div]550  congr 2551  refine List.map_congr_left fun j _ ↦ ?_552  cases s <;> simp [Expr.sub, Expr.neg, Expr.eval, sub_eq_add_neg]553 554/-- Tangent counts are nonnegative at prime powers (they count divisors over `GF(p, e)`). -/555theorem tangent_count_nonneg (Q : ℕ) (hQ : PrimePower Q) (s : State)556    (P : TangentPattern s.degree) (hP : Allowed s P) :557    0 ≤ (tangentCount s P).eval Q := by558  obtain ⟨p, e, hp, he, rfl⟩ := hQ559  have : Fact p.Prime := ⟨hp⟩560  have : Finite (GaloisField p e) := Module.finite_of_finite (ZMod p)561  have h := (pattern_divisor_count (GaloisField p e) s P hP).2562  rw [GaloisField.card p e he.ne'] at h563  exact h ▸ Nat.cast_nonneg _564 565/-! ### Nonnegativity of state-law coefficients -/566 567private theorem primePower_pow (Q : ℕ) (hQ : PrimePower Q) (δ : ℕ) (hδ : 0 < δ) :568    PrimePower (Q ^ δ) := by569  obtain ⟨p, r, hp, hr, rfl⟩ := hQ570  exact ⟨p, r * δ, hp, Nat.mul_pos hr hδ, (pow_mul p r δ).symm⟩571 572private theorem stateLawFuel_coeff_nonneg (k : ℕ) :573    ∀ (s : State), s.Valid → ∀ Q : ℕ, PrimePower Q → ∀ σ : FactorType,574      0 ≤ (lawCoeff (stateLawFuel k s) σ).eval Q := by575  classical576  induction k with577  | zero =>578    intro s _ Q _ σ579    simp only [stateLawFuel]580    exact le_of_eq ((law_coeff_nonneg_closure (Q : ℚ)).2.2.2.2.2.2.2 σ).symm581  | succ k ih =>582    intro s hs Q hQ σ583    obtain ⟨hScale, -, hProd, hFlat, hDesc, hAtom, -, hNil⟩ := law_coeff_nonneg_closure (Q : ℚ)584    have hQ2 : 2 ≤ Q := prime_power_ge_two Q hQ585    have hterms : ∀ σ : FactorType, 0 ≤ (lawCoeff ((allowedPatterns s).toList.flatMap fun P ↦586        if SelfPattern s P then [] else587          lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))588            (lawProd ((children s P).map fun z ↦ lawDescend z.1 (stateLawFuel k z.2)))) σ).eval589              Q := by590      refine hFlat _ _ _ fun P hPmem σ ↦ ?_591      have hP : Allowed s P := by592        rw [Finset.mem_toList, allowedPatterns, Finset.mem_filter] at hPmem593        exact hPmem.2594      split_ifs595      · exact le_of_eq (hNil σ).symm596      · refine hScale _ _ (by597          simpa only [Expr.eval] using mul_nonneg (tangent_count_nonneg Q hQ s P hP)598            (divisor_probability_pos Q hQ2 s P.d.val 2 le_rfl).1.le) (hProd _ ?_) σ599        simp only [List.mem_map]600        rintro _ ⟨z, hz, rfl⟩601        have hz1 := children_residue_degree_pos s P z hz602        refine hDesc z.1 hz1 _ fun σ ↦ ?_603        exact_mod_cast ih z.2 (children_valid s hs P hP z hz) (Q ^ z.1)604          (primePower_pow Q hQ z.1 hz1) σ605    cases s with606    | single a c =>607      rcases c with _ | _ | c608      · exact absurd hs.2 (lt_irrefl 0)609      · exact hAtom a 1 σ610      · exact hScale _ _611          (divisor_probability_pos Q hQ2 (State.single a 0) 0 (c + 2) (by omega)).2.le hterms σ612    | crossing a b c h => exact hterms σ613 614/-- At a prime power `Q`, the coefficients of the law of a valid state, and of all its615descents, are nonnegative. -/616theorem state_law_coeff_nonneg (Q : ℕ) (hQ : PrimePower Q) (s : State) (hs : s.Valid)617    (σ : FactorType) :618    0 ≤ (lawCoeff (stateLaw s) σ).eval Q ∧619      ∀ δ : ℕ, 0 < δ → 0 ≤ (lawCoeff (lawDescend δ (stateLaw s)) σ).eval Q := by620  refine ⟨stateLawFuel_coeff_nonneg _ s hs Q hQ σ, fun δ hδ ↦ ?_⟩621  refine (law_coeff_nonneg_closure (Q : ℚ)).2.2.2.2.1 δ hδ _ (fun σ ↦ ?_) σ622  exact_mod_cast stateLawFuel_coeff_nonneg (s.rank + 1) s hs (Q ^ δ) (primePower_pow Q hQ δ hδ) σ623 624/-! ### Continuity of congruence-compatible maps -/625 626/-- A map between finite products of adic rings that preserves congruence modulo `I₁ ^ L`627(sending it to congruence modulo `I₂ ^ L`) on a set `C` is continuous on `C`. -/628theorem continuousOn_of_congruence_compatible (O₁ O₂ : Type) [CommRing O₁] [TopologicalSpace O₁]629    [IsTopologicalRing O₁] (I₁ : Ideal O₁) (h₁ : IsAdic I₁) [CommRing O₂] [TopologicalSpace O₂]630    [IsTopologicalRing O₂] (I₂ : Ideal O₂) (h₂ : IsAdic I₂) (ι : Type) [Finite ι] (d : ι → ℕ)631    (n₂ : ℕ) (C : Set (∀ i, Fin (d i) → O₁)) (f : (∀ i, Fin (d i) → O₁) → (Fin n₂ → O₂))632    (hf : ∀ (L : ℕ), ∀ a ∈ C, ∀ a' ∈ C, (∀ i j, a i j - a' i j ∈ I₁ ^ L) →633      ∀ j, f a j - f a' j ∈ I₂ ^ L) :634    ContinuousOn f C := by635  have := Fintype.ofFinite ι636  intro a ha s hs637  obtain ⟨t, ht, hat, hts⟩ := ((finite_coordinate_cylinder_basis O₂ I₂ h₂ n₂).mem_nhds_iff).1 hs638  rcases ht with rfl | ⟨L, x, rfl⟩639  · exact absurd hat (Set.notMem_empty _)640  have hU : {a' : ∀ i, Fin (d i) → O₁ | ∀ i j, a' i j - a i j ∈ I₁ ^ L} ∈ nhds a := by641    have : {a' : ∀ i, Fin (d i) → O₁ | ∀ i j, a' i j - a i j ∈ I₁ ^ L}642        = ⋂ i, (fun a' ↦ a' i) ⁻¹' {b : Fin (d i) → O₁ | ∀ j, b j - a i j ∈ I₁ ^ L} := by643      ext a'; simp644    refine IsOpen.mem_nhds ?_ (by simp)645    rw [this]646    exact isOpen_iInter_of_finite fun i ↦647      ((coordinate_cylinder_clopen O₁ I₁ h₁ L).1 (d i) (a i)).1.preimage (continuous_apply i)648  have hmem : {a' | ∀ i j, a' i j - a i j ∈ I₁ ^ L} ∩ C ∈ nhdsWithin a C :=649    Filter.inter_mem (mem_nhdsWithin_of_mem_nhds hU) self_mem_nhdsWithin650  rw [Filter.mem_map]651  refine Filter.mem_of_superset hmem fun a' ⟨h1, h2'⟩ ↦ hts ?_652  change adicCongr I₂ L (f a') x653  have hc : adicCongr I₂ L (f a') (f a) := by654    rw [finite_coordinate_adic_congruence]655    intro j656    have := (I₂ ^ L).neg_mem (hf L a ha a' h2' (fun i j ↦ by657      simpa using (Ideal.neg_mem_iff _).2 (h1 i j)) j)658    simpa using this659  exact (adic_congruence_rules O₂ (Fin n₂ → O₂) I₂).2.2.1 L _ _ _ hc hat660 661end SurfaceBlowup