The root cell law

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.Assembly.MonicCells7import SurfaceBlowup.Blowup.FixedTangentCellBijection8import SurfaceBlowup.Measure.MemberBoxes9import SurfaceBlowup.Recursion.Events10 11/-!12# The root cell law13 14The *root cell law* (`RootCellLaw`) computes the measure of the set of `π`-scaled monic15polynomials `monicPolynomial O (π • z)`, `z ∈ O^r`, with a given factorization type `σ`. This16file proves it unconditionally by building a concrete surface universe: every concrete member is17decomposed into cells, each cell ideal is sent to its strict transforms on the children, and the18termination hypotheses (child types exist, order defect decreases) are verified via the index map19of a cell.20 21## Main results22 23* `root_cell_law_at_universe_member`: the root cell law at a single universe member.24* `cell_member_index_map`: the index map `R ⧸ J → ∏ B j` of a cell, with cokernel length `d(d-1)/2`.25* `cell_child_bijOn`, `concrete_member_cells_cover`: cells and their children.26* `concrete_universe_exists`: a surface universe indexed by concrete members exists.27* `root_cell_law`: the root cell law.28* `monic_type_event_measurable_of_root_cell_law`: measurability of monic type events.29 30Provenance: `Thm_SurfaceBlowupV2_{algebra_type_ascent, etale_children_types_exist,31etale_recursion_data_abstract, concrete_termination_data_of_index_map,32monic_type_event_measurable_of_root_cell_law, root_cell_law_at_universe_member,33root_cell_law_of_universe, cell_child_bijOn, cell_datum_multiplicities_pos, cell_member_index_map,34cell_child_termination_data, cell_child_type_add, state_ideal_has_multiplicity,35state_ideal_multiplicity_le_contacts, concrete_member_cells_cover,36concrete_universe_of_cell_measure, concrete_universe_exists, root_cell_law}`.37-/38 39noncomputable section40 41namespace SurfaceBlowup42 43open scoped BigOperators ENNReal44 45/-! ### Algebra types along unramified extensions -/46 47/-- **Type ascent.** If `O → Oδ` is a finite free unramified extension of rank `δ` of complete DVRs48and the `Oδ`-algebra `B` has `O`-algebra type `σ`, then `B` has some `Oδ`-algebra type `τ` with49`σ = scaleType δ τ`. -/50private theorem algebra_type_ascent (O Oδ : Type) [CommRing O] [IsDomain O]51    [IsDiscreteValuationRing O]52    [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ] [Algebra O Oδ] [Module.Finite O Oδ]53    [Module.Free O Oδ] (δ : ℕ) (hrank : Module.finrank O Oδ = δ) (pi : O) (hpi : Irreducible pi)54    (hpiδ : Irreducible (algebraMap O Oδ pi)) [IsAdicComplete (IsLocalRing.maximalIdeal O) O]55    [Finite (IsLocalRing.ResidueField O)] (B : Type) [CommRing B] [Algebra O B] [Algebra Oδ B]56    [IsScalarTower O Oδ B] (σ : FactorType) (h : HasAlgebraType O B σ) :57    ∃ τ : FactorType, HasAlgebraType Oδ B τ ∧ σ = scaleType δ τ := by58  have ⟨ι, hι, L, hF, _, _, _, _, e, _, hfinL⟩ := h59  obtain ⟨a1, a2, a3, a4, E, hc⟩ :=60    unramified_generic_fibre_ascent O Oδ δ hrank pi hpi hpiδ B ι L e61  -- closure finiteness over `Oδ` follows from finiteness over `O` (same fields `L i`)62  have hfinδ (i) : Module.Finite Oδ (integralClosure Oδ (L i)) :=63    have : IsScalarTower O Oδ (L i) := .of_algebraMap_eq fun c => by64      rw [hc i c, ← IsScalarTower.algebraMap_apply]65    closure_finite_ascent O Oδ (L i) (hfinL i)66  have hτ : HasAlgebraType Oδ B (∑ i, ({fieldInvariant Oδ (L i)} : FactorType)) :=67    ⟨ι, hι, L, hF, a1, a2, a3, a4, E, rfl, hfinδ⟩68  exact ⟨_, hτ, algebra_type_unique O B σ _ h69    (algebra_type_unramified_descent O Oδ δ hrank pi hpi hpiδ B _ hτ)⟩70 71/-- If `A` has an algebra type and `ψ : A → ∏ B j` is injective with finite-length cokernel, where72each `B j` is an algebra over an unramified extension `O_j` of `O`, then every `B j` has an73`O_j`-algebra type. -/74private theorem etale_children_types_exist (O : Type) [CommRing O] [IsDomain O]75    [IsDiscreteValuationRing O]76    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (n : ℕ)77    (Oj : Fin n → Type) [∀ j, CommRing (Oj j)] [∀ j, IsDomain (Oj j)]78    [∀ j, IsDiscreteValuationRing (Oj j)] [∀ j, Algebra O (Oj j)] [∀ j, Module.Finite O (Oj j)]79    [∀ j, Module.Free O (Oj j)] (δ : Fin n → ℕ) (hrank : ∀ j, Module.finrank O (Oj j) = δ j)80    (pi : O) (hpi : Irreducible pi) (hpiδ : ∀ j, Irreducible (algebraMap O (Oj j) pi)) (A : Type)81    [CommRing A] [Algebra O A] (B : Fin n → Type) [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)]82    [∀ j, Algebra (Oj j) (B j)] [∀ j, IsScalarTower O (Oj j) (B j)] (ψ : A →ₐ[O] ∀ j, B j)83    (hinj : Function.Injective ψ) (ℓ : ℕ) (hℓ : Module.length O84    ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = ℓ) (σ : FactorType) (hσ : HasAlgebraType O A σ) :85    ∀ j, ∃ τ : FactorType, HasAlgebraType (Oj j) (B j) τ := by86  intro j87  obtain ⟨τ₀, h₀⟩ := algebra_type_children_exists O A n B ψ hinj ℓ hℓ σ hσ j88  obtain ⟨τ, hτ, -⟩ := algebra_type_ascent O (Oj j) (δ j) (hrank j) pi hpi (hpiδ j) (B j) τ₀ h₀89  exact ⟨τ, hτ⟩90 91/-- The abstract étale recursion data: in the situation of `etale_children_types_exist`, every92child `B j` has an algebra type, its order defect is at most that of `A`, and strictly smaller93when the cokernel of `ψ` is nonzero. -/94private theorem etale_recursion_data_abstract (O : Type) [CommRing O] [IsDomain O]95    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]96    [Finite (IsLocalRing.ResidueField O)] (n : ℕ) (Oj : Fin n → Type) [∀ j, CommRing (Oj j)]97    [∀ j, IsDomain (Oj j)] [∀ j, IsDiscreteValuationRing (Oj j)] [∀ j, Algebra O (Oj j)]98    [∀ j, Module.Finite O (Oj j)] [∀ j, Module.Free O (Oj j)] (δ : Fin n → ℕ)99    (hrank : ∀ j, Module.finrank O (Oj j) = δ j) (pi : O) (hpi : Irreducible pi)100    (hpiδ : ∀ j, Irreducible (algebraMap O (Oj j) pi)) (A : Type) [CommRing A] [Algebra O A]101    [Module.Finite O A] [Module.Free O A] (B : Fin n → Type) [∀ j, CommRing (B j)]102    [∀ j, Algebra O (B j)] [∀ j, Module.Finite O (B j)] [∀ j, Module.Free O (B j)]103    [∀ j, Algebra (Oj j) (B j)] [∀ j, IsScalarTower O (Oj j) (B j)] (ψ : A →ₐ[O] ∀ j, B j)104    (hinj : Function.Injective ψ) (ℓ : ℕ) (hℓ : Module.length O105    ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = ℓ) (σ : FactorType) (hσ : HasAlgebraType O A σ) :106    ∀ j, (∃ τ : FactorType, HasAlgebraType (Oj j) (B j) τ) ∧ (orderDefect (Oj j) (B j)).toNat ≤107        (orderDefect O A).toNat ∧ (1 ≤ ℓ → (orderDefect (Oj j) (B j)).toNat <108        (orderDefect O A).toNat) := fun j ↦109  ⟨etale_children_types_exist O n Oj δ hrank pi hpi hpiδ A B ψ hinj ℓ hℓ σ hσ j,110    etale_invariant_children O n Oj δ hrank pi hpi hpiδ A B ψ hinj ℓ hℓ σ hσ j⟩111 112/-- `etale_recursion_data_abstract` specialised to a concrete member `m`, a cell ideal `J` and113child members `mc j`: the quotient `R ⧸ J` plays the role of `A`. -/114private theorem concrete_termination_data_of_index_map (m : ConcreteMember) (n : ℕ)115    (mc : Fin n → ConcreteMember) [∀ j, Algebra m.O (mc j).O] [∀ j, Module.Finite m.O (mc j).O]116    [∀ j, Module.Free m.O (mc j).O] (δ : Fin n → ℕ)117    (hrank : ∀ j, Module.finrank m.O (mc j).O = δ j)118    (hpi : ∀ j, Irreducible (algebraMap m.O (mc j).O m.pi)) (J : Ideal m.R) (B : Fin n → Type)119    [∀ j, CommRing (B j)] [∀ j, Algebra m.O (B j)] [∀ j, Algebra (mc j).O (B j)]120    [∀ j, IsScalarTower m.O (mc j).O (B j)] [∀ j, Module.Finite (mc j).O (B j)]121    [∀ j, Module.Free (mc j).O (B j)] (ψ : (m.R ⧸ J) →ₐ[m.O] ∀ j, B j) (hψ : Function.Injective ψ)122    (ℓ : ℕ) (hlen : Module.length m.O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = (ℓ : ℕ∞))123    [Module.Finite m.O (m.R ⧸ J)] [Module.Free m.O (m.R ⧸ J)] (σ : FactorType)124    (hσ : HasAlgebraType m.O (m.R ⧸ J) σ) :125    ∀ j, (∃ τ : FactorType, HasAlgebraType (mc j).O (B j) τ) ∧ (orderDefect (mc j).O (B j)).toNat ≤126        (orderDefect m.O (m.R ⧸ J)).toNat ∧ (1 ≤ ℓ → (orderDefect (mc j).O (B j)).toNat <127        (orderDefect m.O (m.R ⧸ J)).toNat) := by128  have : ∀ j, Module.Finite m.O (B j) := fun j => Module.Finite.trans (mc j).O (B j)129  have : ∀ j, Module.Free m.O (B j) := fun j => Module.Free.trans (S := (mc j).O)130  have h := etale_recursion_data_abstract m.O n (fun j => (mc j).O) δ hrank m.pi m.hpi hpi131    (m.R ⧸ J) B132  exact h ψ hψ ℓ hlen σ hσ133 134/-- Assuming the root cell law, the set of monic polynomials of degree `n` over `O` with135factorization type `σ` is measurable. -/136theorem monic_type_event_measurable_of_root_cell_law (hroot : RootCellLaw) (O : Type) [CommRing O]137    [IsDomain O] [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]138    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]139    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]140    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :141    MeasurableSet {a : Fin n→O | HasPolynomialTypeF O (monicPolynomial O a) σ} := by142  obtain ⟨⟨S, hS⟩, hcov, -⟩ := monic_cells_partition O htop n143  have key : {a : Fin n→O | HasPolynomialTypeF O (monicPolynomial O a) σ} =144      ⋃ D ∈ S, (residueCell O n (divisorAffinePolynomial (IsLocalRing.ResidueField O) D) ∩145          typeEvent O n σ) := by146    ext a147    simp only [Set.mem_ofPred_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_prop]148    refine ⟨fun h ↦ ?_, fun ⟨_, _, _, h⟩ ↦ h⟩149    obtain ⟨D, ⟨hD, ha⟩, -⟩ := hcov a150    exact ⟨D, (hS D).2 hD, ha, h⟩151  rw [key]152  refine Finset.measurableSet_biUnion _ fun D hD => ?_153  have hD' := (hS D).1 hD154  obtain ⟨⟨m, hm, -⟩, -⟩ := divisor_array_exists_unique (IsLocalRing.ResidueField O) n D hD'.2155  exact (monic_cell_law hroot O htop n D hD' m hm σ).1156 157/-! ### The root cell law from a concrete universe -/158 159/-- A surface universe indexed by all concrete members, satisfying the termination hypotheses. -/160private def ConcreteUniverse : Prop :=161  ∃ U : SurfaceUniverse, ∃ eι : U.ι ≃ ConcreteMember, (∀ i, U.M i = (eι i).toMeasured) ∧162    U.ChildTypesExist ∧163      U.InvariantDecreases fun i J ↦ (orderDefect (U.M i).O ((U.M i).R ⧸ J)).toNat164 165/-- **Root cell law at a universe member.** Let `i` be a member of a surface universe satisfying166the termination hypotheses, whose state is the single state `(1, r)` and whose measure is the167pushforward of the coefficient measure along a coordinate chart `z ↦ (f, b)(π z)` matching168algebra types with polynomial types. Then the type-`σ` event of `π`-scaled monic polynomials is169measurable and has mass `densityValue (lawCoeff (stateLaw (single 1 r)) σ) q`. -/170theorem root_cell_law_at_universe_member (U : SurfaceUniverse)171    (hE1 : U.ChildTypesExist)172    (hE2 : U.InvariantDecreases fun i J ↦ (orderDefect (U.M i).O ((U.M i).R ⧸ J)).toNat)173    (i : U.ι) (r : ℕ) (hr : 0 < r)174    (hs : (U.M i).s = State.single 1 r) (f : (U.M i).R)175    (b : Fin (State.single 1 r).degree → (U.M i).R)176    (hmeas : Measurable (coordinateIdeal (U.M i).S.pi f b))177    (hμ : (U.M i).μ = (((U.M i).q : ℝ≥0∞)⁻¹ ^ (State.single 1 r).degree) •178    (coefficientMeasure (U.M i).O (State.single 1 r).degree).map179    (coordinateIdeal (U.M i).S.pi f b)) (hcell : ∀ z : Fin (State.single 1 r).degree → (U.M i).O,180    (coordinateIdeal (U.M i).S.pi f b) z ∈ (U.M i).stateSet)181    (htype : ∀ (z : Fin (State.single 1 r).degree → (U.M i).O) (σ : FactorType), HasAlgebraType182    (U.M i).O ((U.M i).R ⧸ (coordinateIdeal (U.M i).S.pi f b) z) σ ↔ HasPolynomialTypeF (U.M i).O183    (monicPolynomial (U.M i).O ((U.M i).S.pi • z)) σ) (σ : FactorType) :184    MeasurableSet {z : Fin (State.single 1 r).degree → (U.M i).O | HasPolynomialTypeF (U.M i).O185        (monicPolynomial (U.M i).O ((U.M i).S.pi • z)) σ} ∧ coefficientMeasure (U.M i).O186        (State.single 1 r).degree {z : Fin (State.single 1 r).degree → (U.M i).O |187        HasPolynomialTypeF (U.M i).O (monicPolynomial (U.M i).O ((U.M i).S.pi • z)) σ} =188        densityValue (lawCoeff (stateLaw (State.single 1 r)) σ) (U.M i).q := by189  have hpre : coordinateIdeal (U.M i).S.pi f b ⁻¹' U.typeEvent i σ =190      {z : Fin (State.single 1 r).degree → (U.M i).O | HasPolynomialTypeF (U.M i).O191          (monicPolynomial (U.M i).O ((U.M i).S.pi • z)) σ} := by192    ext z193    simp only [Set.mem_preimage, SurfaceUniverse.typeEvent, Set.mem_ofPred_eq]194    exact ⟨fun h => (htype z σ).1 h.2, fun h => ⟨hcell z, (htype z σ).2 h⟩⟩195  refine ⟨?_, ?_⟩196  · rw [← hpre]197    exact hmeas (etale_type_event_measurable U hE1198      (fun i J => (orderDefect (U.M i).O ((U.M i).R ⧸ J)).toNat) hE2 i σ)199  · have hd : (State.single 1 r).degree = r := by simp [State.degree]200    have hdpos : 0 < (State.single 1 r).degree := by rw [hd]; exact hr201    obtain ⟨hFm, hFE, hEF, hN⟩ := type_event_null_difference U i σ202    have hL := ((universal_law_statement U i).1 σ).2.2203    rw [hs] at hL204    have e : stateLaw (State.single 1 (State.single 1 r).degree) = stateLaw (State.single 1 r) := by205      rw [hd]206    have key := chart_cell_law_generic (U.M i).O (U.M i).htop (U.M i).S.pi207      (U.M i).R (State.single 1 r).degree f b hmeas208      (U.M i).stateSet hcell (U.M i).μ hμ htype σ (U.termTypeEvent i σ) (U.nonterminatingSet i)209      hFm hFE hEF hN (by rw [e]; exact hL)210    rw [e] at key211    exact key.1212 213/-- The root cell law follows from the existence of a concrete surface universe: the one-chart214member with state `(1, r)` realises the root cell, and the universal law computes its mass. -/215private theorem root_cell_law_of_universe (hU : ConcreteUniverse) : RootCellLaw := by216  obtain ⟨U, eι, hM, hE1, hE2⟩ := hU217  intro O _ _ _ _ _ _ _ _ _ _ _ _ htop pi hpi r hr σ218  obtain ⟨hD, hReg, S, hSpi, hSt, hSx, -, hSa, hSb⟩ :=219    concrete_surface_data_exists_unconditional O pi hpi 1 1 0 one_pos220  obtain ⟨A, i₀, hi₀, hf, hb, hμA⟩ :=221    repeated_root_one_chart_atlas O pi hpi S hSpi hSt hSa hSb r hr222  have hshape : StateShape 1 0 (State.single 1 r) := ⟨rfl, rfl, hr⟩223  let m₀ : ConcreteMember :=224    { O := O, htop := htop, pi := pi, hpi := hpi, u := 1, a := 1, b := 0, ha := one_pos,225      S := S, hS_pi := hSpi, hS_t := hSt, hS_x := hSx, hS_a := hSa, hS_b := hSb,226      s := State.single 1 r, shape := hshape, atlas := A }227  set i := eι.symm m₀228  have hMi : U.M i = m₀.toMeasured := by rw [hM i]; simp [i]229  have hdeg : 0 < (State.single 1 r).degree := by simpa [State.degree] using hr230  have key : ∀ M : MeasuredSurface, M = m₀.toMeasured →231      (M.s = State.single 1 r) ∧ ∃ (f : M.R) (b : Fin (State.single 1 r).degree → M.R),232        Measurable (coordinateIdeal M.S.pi f b) ∧233        M.μ = ((M.q : ℝ≥0∞)⁻¹ ^ (State.single 1 r).degree) •234          (coefficientMeasure M.O (State.single 1 r).degree).map (coordinateIdeal M.S.pi f b) ∧235        (∀ z : Fin (State.single 1 r).degree → M.O, (coordinateIdeal M.S.pi f b) z ∈ M.stateSet) ∧236        (∀ (z : Fin (State.single 1 r).degree → M.O) (σ : FactorType),237          HasAlgebraType M.O (M.R ⧸ (coordinateIdeal M.S.pi f b) z) σ ↔238            HasPolynomialTypeF M.O (monicPolynomial M.O (M.S.pi • z)) σ) := by239    intro M hM'240    subst hM'241    have hch := concrete_member_charts m₀ i₀242    refine ⟨rfl, (A.chart i₀).f, (A.chart i₀).b, hch.2.2, ?_, ?_, ?_⟩243    · let _ : MeasurableSpace (Ideal (ConcreteSurface O pi 1 1 0)) :=244        idealChartSigma O (ConcreteSurface O pi 1 1 0) S.pi245      change stateMeasure O (ConcreteSurface O pi 1 1 0) S.pi (State.single 1 r).degree246        (Nat.card (IsLocalRing.ResidueField O)) A = _247      rw [hμA]248      change _ = _ • (coefficientMeasure O (State.single 1 r).degree).map249        (coordinateIdeal S.pi (A.chart i₀).f (A.chart i₀).b)250      rw [hf, hb]251      rfl252    · intro z253      have hz : coordinateIdeal m₀.S.pi (m₀.atlas.chart i₀).f (m₀.atlas.chart i₀).b z ∈254          residueIdealCell (algebraMap m₀.O m₀.R m₀.S.pi) (m₀.atlas.chart i₀).f := by255        rw [← hch.2.1]; exact ⟨z, rfl⟩256      exact (Set.ext_iff.1 A.cover _).2 (Set.mem_iUnion.2 ⟨i₀, hz⟩)257    · intro z τ258      have e : ∀ z' : Fin (State.single 1 r).degree → O,259          HasAlgebraType O (ConcreteSurface O pi 1 1 0 ⧸260            coordinateIdeal S.pi (A.chart i₀).f (A.chart i₀).b z') τ ↔261          HasPolynomialTypeF O (monicPolynomial O (S.pi • z')) τ := by262        intro z'263        rw [hf, hb, hSpi]264        exact repeated_root_chart_type O pi hpi _ hdeg z' τ265      exact e z266  have back : ∀ M : MeasuredSurface, M = m₀.toMeasured →267      (MeasurableSet {z : Fin (State.single 1 r).degree → M.O | HasPolynomialTypeF M.O268          (monicPolynomial M.O (M.S.pi • z)) σ} ∧ coefficientMeasure M.O (State.single 1 r).degree269          {z : Fin (State.single 1 r).degree → M.O | HasPolynomialTypeF M.O270          (monicPolynomial M.O (M.S.pi • z)) σ} = densityValue271          (lawCoeff (stateLaw (State.single 1 r)) σ) M.q) →272      MeasurableSet {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} ∧273      coefficientMeasure O r {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} =274        densityValue (lawCoeff (stateLaw (State.single 1 r)) σ)275            (Nat.card (IsLocalRing.ResidueField O)) := by276    intro M hM' h277    subst hM'278    have hpi' : m₀.toMeasured.S.pi = pi := hSpi279    rw [hpi'] at h280    exact root_cell_clauses_reindex O pi σ _ _ r (Nat.one_mul r) h281  obtain ⟨hs, f, b, hmeas, hμ, hcell, htype⟩ := key (U.M i) hMi282  exact back (U.M i) hMi (root_cell_law_at_universe_member U hE1 hE2 i r hr hs f b hmeas hμ hcell283      htype σ)284 285private theorem pattern_degree_facts_of_hasPattern (k : Type) [Field k] (a b : ℕ) (s : State)286    (hsh : StateShape a b s)287    (P : TangentPattern s.degree) (hP : Allowed s P) (Dv : ExceptionalDivisor k)288        (hD : HasPattern k s Dv P) :289    0 < P.d.val ∧290    ((∃ c : ℕ, s = State.single a c ∧ b = 0) ∨ (∃ c h : ℕ, s = State.crossing a b c h ∧ 0 < b)) ∧291    P.d.val ≤ stateContactT s ∧ (∀ h : ℕ, stateContactX s = some h → P.d.val ≤ h) ∧292    (0 < Dv none ↔ P.d.val < stateContactT s) ∧293    (∀ h : ℕ, stateContactX s = some h → (0 < Dv (zeroDirection k) ↔ P.d.val < h)) ∧294    exceptionalDegree k Dv = P.d.val := by295  obtain ⟨hdeg, hinf, hz, -⟩ := hD296  have hinf' : Dv none = P.rt.val := hinf297  cases s with298  | single a' c =>299    obtain ⟨rfl, hb, -⟩ := hsh300    obtain ⟨h0, -, h1, -, h3⟩ := hP301    refine ⟨h0, Or.inl ⟨c, rfl, hb⟩, h1, fun h hh => by simp [stateContactX] at hh, ?_,302      fun h hh => by simp [stateContactX] at hh, hdeg⟩303    rw [hinf']; exact h3304  | crossing a' b' c h =>305    obtain ⟨rfl, rfl, hb, -, -⟩ := hsh306    obtain ⟨h0, -, h1, h2, h3, h4⟩ := hP307    have hz' : Dv (zeroDirection k) = P.rx.val := hz308    refine ⟨h0, Or.inr ⟨c, h, rfl, hb⟩, h1, fun h' hh => ?_, ?_, fun h' hh => ?_, hdeg⟩309    · simp only [stateContactX, Option.some.injEq] at hh; subst hh; exact h2310    · rw [hinf']; exact h3311    · simp only [stateContactX, Option.some.injEq] at hh; subst hh; rw [hz']; exact h4312 313private theorem divisorStrictTransform_bijOn (m : ConcreteMember) (t x : m.R)314    (ht : t = surfaceT m.O m.pi m.u m.a m.b) (hx : x = surfaceX m.O m.pi m.u m.a m.b)315    (e : (BlowupChart m.R t x ⧸ chartExceptional m.R t x) ≃+* Polynomial316        (IsLocalRing.ResidueField m.R))317    (he : ∀ r : m.R, e (Ideal.Quotient.mk (chartExceptional m.R t x) (chartBase m.R t x r)) =318      Polynomial.C (IsLocalRing.residue m.R r))319    (heZ : e (Ideal.Quotient.mk (chartExceptional m.R t x) (chartSlope m.R t x)) = Polynomial.X)320    (hinf : (infinityPoint m.R t x).IsPrime)321    (P : TangentPattern m.s.degree) (hP : Allowed m.s P)322    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField m.R))323    (hD : HasPattern (IsLocalRing.ResidueField m.R) m.s Dv P) :324    Set.BijOn (fun J Q => divisorStrictTransform m.R t x e Dv hinf P.d.val J Q)325      (fixedTangentCell m.O m.R m.S m.s P.d.val Dv)326      (Set.pi Set.univ (childIdealSet m.R t x e Dv hinf m.s P.d.val)) := by327  subst ht hx328  obtain ⟨h1, h2, h3, h4, h5, h6, h7⟩ :=329    pattern_degree_facts_of_hasPattern (IsLocalRing.ResidueField m.R) m.a m.b m.s m.shape P hP Dv hD330  exact strict_transform_bijOn_child_ideals m.O m.pi m.hpi m.u m.a m.b m.ha m.S ⟨m.hS_t, m.hS_x,331      m.hS_a, m.hS_b⟩ e he332      heZ Dv hinf333    m.s P.d.val h1 h2 h3 h4 h5 h6 h7334 335/-! ### Cells and their children -/336 337/-- The child map `J ↦ (Φ J j)_j` is a bijection from the cell `c` of a concrete member onto the338product of the children's state sets. -/339theorem cell_child_bijOn (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c) :340    Set.BijOn (fun J j => D.Φ J j) (m.toMeasured.cell c)341        (Set.pi Set.univ fun j => (D.mc j).toMeasured.stateSet) := by342  have hF := divisorStrictTransform_bijOn m m.S.t m.S.x m.hS_t m.hS_x D.e D.he D.heZ D.hinf c.1.1343      c.1.2 c.2.1344      c.2.2345  set d := m.toMeasured.cellDegree c346  let T : (∀ Q, Ideal (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf Q)) →347      ∀ j : m.toMeasured.childIdx c, Ideal (D.mc j).R :=348    fun u j => Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j)349        →+* (D.mc j).R)350      (u (D.point j))351  have hmapmap : ∀ j (I : Ideal (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j))),352      Ideal.map ((D.Eq j).symm : (D.mc j).R →+* divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf353          (D.point j)) (Ideal.map354          (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) →+* (D.mc j).R)355          I) = I := fun j _ ↦ Ideal.map_of_equiv (D.Eq j)356  have hmapmap' : ∀ j (I : Ideal (D.mc j).R),357      Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) →+*358          (D.mc j).R) (Ideal.map359          ((D.Eq j).symm : (D.mc j).R →+* divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf360          (D.point j)) I) = I := fun j _ ↦ Ideal.map_of_equiv (D.Eq j).symm361  have hsurjpt : ∀ Q : divisorSupport c.2.1, ∃ j, D.point j = Q := by362    intro Q363    obtain ⟨j, hj⟩ := (D.asg.supp Q.1).mp Q.2364    exact ⟨j, Subtype.ext hj⟩365  have hbij : Function.Bijective (fun j => D.point j) :=366    ⟨fun i j h => D.asg.inj (congrArg Subtype.val h), hsurjpt⟩367  let σ := Equiv.ofBijective _ hbij368  have hT : Set.BijOn T (Set.pi Set.univ (childIdealSet m.R m.S.t m.S.x D.e c.2.1 D.hinf m.s d))369      (Set.pi Set.univ fun j => (D.mc j).toMeasured.stateSet) := by370    refine ⟨?_, ?_, ?_⟩371    · intro u hu j _372      exact (child_ideal_set_map_iff_stateSet m c D j (u (D.point j))).mp (hu _ (Set.mem_univ _))373    · intro u _ v _ huv374      funext Q375      obtain ⟨j, rfl⟩ := hsurjpt Q376      have := congrFun huv j377      rw [← hmapmap j (u (D.point j)), ← hmapmap j (v (D.point j))]378      exact congrArg _ this379    · intro w hw380      let v : ∀ j : m.toMeasured.childIdx c, Ideal381          (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j)) :=382        fun j => Ideal.map ((D.Eq j).symm : (D.mc j).R →+* divisorLocalRing m.R m.S.t m.S.x D.e383            c.2.1 D.hinf (D.point j)) (w j)384      let u := Equiv.piCongrLeft (fun Q => Ideal385          (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf Q)) σ v386      have hu : ∀ j, u (D.point j) = v j := fun j => Equiv.piCongrLeft_apply_apply387          (fun Q => Ideal (divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf Q)) σ v j388      refine ⟨u, ?_, ?_⟩389      · intro Q _390        obtain ⟨j, rfl⟩ := hsurjpt Q391        rw [hu]392        apply (child_ideal_set_map_iff_stateSet m c D j _).mpr393        exact (hmapmap' j (w j)).symm ▸ hw j (Set.mem_univ _)394      · funext j395        change Ideal.map _ (u (D.point j)) = w j396        rw [hu]397        exact hmapmap' j (w j)398  have hcomp : (fun J j => D.Φ J j) =399      T ∘ (fun J Q => divisorStrictTransform m.R m.S.t m.S.x D.e c.2.1 D.hinf d J Q) := by400    funext J j401    exact cell_child_Phi_eq_map m c D J j402  rw [hcomp]403  exact hT.comp hF404 405/-- The residue polynomial `H = ∑ᵢ c̄ᵢ Xⁱ` of a family `c` has coefficients `c̄ᵢ`. -/406private theorem residue_sum_coeff {R : Type} [CommRing R] [IsLocalRing R] (d : ℕ)407    (c : Fin (d + 1) → R) (i : Fin (d + 1)) :408    (∑ j : Fin (d + 1), Polynomial.C (IsLocalRing.residue R (c j)) * Polynomial.X ^ j.val).coeff i =409      IsLocalRing.residue R (c i) := by410  simp only [Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow]411  rw [Finset.sum_eq_single i (fun j _ hj ↦ if_neg fun h ↦ hj (Fin.ext h.symm)) (by simp)]412  simp413 414/-- The residue polynomial `H = ∑ᵢ c̄ᵢ Xⁱ` of a curve `∑ cᵢ tᵈ⁻ⁱ xⁱ` of multiplicity `d` on a415concrete surface is nonzero. -/416private theorem residue_sum_ne_zero (O : Type) [CommRing O] [IsDomain O]417    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)418    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)419    [IsLocalRing (ConcreteSurface O pi u a b)] (d : ℕ)420    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))421    (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {(surfaceT O pi u a b), (surfaceX O pi u a b)}) :422    ∑ j : Fin (d + 1), Polynomial.C (IsLocalRing.residue _ (c j)) * Polynomial.X ^ j.val ≠ 0 := by423  obtain ⟨i, hi⟩ := hne424  intro h0425  have := residue_sum_coeff d c i426  rw [h0, Polynomial.coeff_zero, eq_comm, IsLocalRing.residue_eq_zero_iff,427    concrete_surface_maximalIdeal_eq O pi hpi u a b ha] at this428  exact hi this429 430/-- For a curve `f = ∑ cᵢ tᵈ⁻ⁱ xⁱ` of multiplicity `d` on a concrete surface and two-chart curve431data `D` of its strict transform, all point multiplicities in the `t`-chart are positive. -/432private theorem cell_datum_left_multiplicity_pos (O : Type) [CommRing O] [IsDomain O]433    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]434    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)435    (a b : ℕ) (ha : 0 < a) [IsLocalRing (ConcreteSurface O pi u a b)] (d : ℕ)436    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))437    (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span438    {(surfaceT O pi u a b), (surfaceX O pi u a b)})439    (e : ((BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ⧸440    chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ≃+*441    Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))442    (he : ∀ r : (ConcreteSurface O pi u a b), e (Ideal.Quotient.mk443    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))444    ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) r)) =445    Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))446    (heZ : e (Ideal.Quotient.mk447    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))448    (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))) =449    Polynomial.X) (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)450    (surfaceX O pi u a b)) (D : TwoChartCurveData (ConcreteSurface O pi u a b)451    (surfaceT O pi u a b) (surfaceX O pi u a b) beta)452    (hl : ∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap453    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))454    (leftPoint D s) (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)455    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) (c i) *456    (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))^i.val) ∧457    (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)458    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) (c i) *459    (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))^i.val) ∈460    leftPoint D s) (s : D.ι ⊕ D.ι0) :461    0 < leftMultiplicity D s := by462  classical463  -- the point is a direction point `φ` dividing the residue polynomial `H`464  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set465      (ConcreteSurface O pi u a b))).IsMaximal :=466    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha467  obtain ⟨hPmax, -, hPt⟩ := two_chart_left_points_maximal (ConcreteSurface O pi u a b) _ _468    beta D469  have := hPmax s470  obtain ⟨φ, hPφ, hmap, -⟩ := chart_point_eq_directionPoint _ _ _ e he heZ _ (hPt s)471  have hdvd : φ.val ∣ ∑ i : Fin (d + 1),472      Polynomial.C (IsLocalRing.residue _ (c i)) * Polynomial.X ^ i.val := by473    have hmem := (hl s).2474    rw [hPφ] at hmem475    unfold directionPoint at hmem476    rw [Ideal.mem_comap, Ideal.mem_span_singleton] at hmem477    convert hmem using 1478    simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, map_sum,479      map_mul, map_pow, heZ]480    exact Finset.sum_congr rfl fun i _ ↦ congrArg (· * _) (he (c i)).symm481  unfold leftMultiplicity leftLevelIdeal finiteLocalCurveIdeal482  rw [(hl s).1, pow_one, concrete_strict_transform_multiplicity O pi hpi u a b ha d c hne483    (leftPoint D s) (hPt s) e he heZ φ.val φ.property hmap, ENat.toNat_natCast]484  exact Multiset.count_pos.mpr ((UniqueFactorizationMonoid.mem_normalizedFactors_iff'485    (residue_sum_ne_zero O pi hpi u a b ha d c hne)).mpr486    ⟨φ.2.2, φ.2.1.normalize_eq_self, hdvd⟩)487 488/-- For a curve `f = ∑ cᵢ tᵈ⁻ⁱ xⁱ` of multiplicity `d` on a concrete surface and two-chart curve489data `D` of its strict transform, the multiplicities at the points of the `x`-chart away from the490`t`-chart are positive. -/491private theorem cell_datum_right_multiplicity_pos (O : Type) [CommRing O] [IsDomain O]492    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]493    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)494    (a b : ℕ) (ha : 0 < a) [IsLocalRing (ConcreteSurface O pi u a b)] (d : ℕ)495    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))496    (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span497    {(surfaceT O pi u a b), (surfaceX O pi u a b)})498    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)499    (surfaceX O pi u a b)) (D : TwoChartCurveData (ConcreteSurface O pi u a b)500    (surfaceT O pi u a b) (surfaceX O pi u a b) beta)501    (hr : ∀ s : D.ι ⊕ D.ιinf, Ideal.span {rightData D s} = Ideal.span502    {completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b)503    (surfaceT O pi u a b)) (rightPoint D s) (∑ i : Fin (d+1), algebraMap504    (ConcreteSurface O pi u a b) (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b)505    (surfaceT O pi u a b)) (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b)506    (surfaceT O pi u a b))^(d - i.val))} ∧ (∑ i : Fin (d+1), algebraMap507    (ConcreteSurface O pi u a b) (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b)508    (surfaceT O pi u a b)) (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b)509    (surfaceT O pi u a b))^(d - i.val)) ∈ rightPoint D s) (l : D.ιinf) :510    0 < rightMultiplicity D (Sum.inr l) := by511  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set512      (ConcreteSurface O pi u a b))).IsMaximal :=513    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha514  set H : Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) :=515    ∑ i : Fin (d+1), Polynomial.C (IsLocalRing.residue _ (c i)) * Polynomial.X ^ i.val with hH516  obtain ⟨hPmax, -, hPx⟩ := two_chart_right_points_maximal (ConcreteSurface O pi u a b) _ _517    beta D518  have hW := D.slopeinf l519  -- the top coefficient lies in the maximal ideal, so `H` has degree `< d`520  have hcd : c (Fin.last d) ∈ IsLocalRing.maximalIdeal _ := by521    by_contra hnot522    have hmem := (hr (Sum.inr l)).2523    rw [Fin.sum_univ_castSucc] at hmem524    simp only [Fin.val_last, Nat.sub_self, pow_zero, mul_one] at hmem525    refine (hPmax (Sum.inr l)).ne_top (Ideal.eq_top_of_isUnit_mem _526      ((Ideal.add_mem_iff_right _ (Ideal.sum_mem _ fun i _ ↦ ?_)).1 hmem)527      ((IsLocalRing.notMem_maximalIdeal.mp hnot).map _))528    have := i.isLt529    obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero530      (by simp only [Fin.val_castSucc]; omega : d - (Fin.castSucc i).val ≠ 0)531    rw [hk, pow_succ]532    exact Ideal.mul_mem_left _ _ (Ideal.mul_mem_left _ _ hW)533  have hlt : H.natDegree < d := by534    refine (Polynomial.natDegree_sum_le_of_forall_le _ _ fun i _ ↦535      (Polynomial.natDegree_C_mul_X_pow_le _ _).trans (Nat.lt_succ_iff.mp i.isLt)).lt_of_ne536      fun h ↦ residue_sum_ne_zero O pi hpi u a b ha d c hne ?_537    rw [← Polynomial.leadingCoeff_eq_zero, Polynomial.leadingCoeff, h]538    simpa [IsLocalRing.residue_eq_zero_iff] using (residue_sum_coeff d c (Fin.last d)).trans539      ((IsLocalRing.residue_eq_zero_iff _).2 hcd)540  unfold rightMultiplicity rightLevelIdeal finiteLocalCurveIdeal541  rw [pow_one, Ideal.span_insert, (hr (Sum.inr l)).1, ← Ideal.span_insert,542    concrete_infinity_strict_transform_multiplicity O pi hpi u a b ha d c hne543      (rightPoint D (Sum.inr l)) (hPx _) hW, ENat.toNat_natCast, ← hH]544  omega545 546private theorem concrete_index_map_reindexed_of_eq (O : Type) [CommRing O] [IsDomain O]547    [IsDiscreteValuationRing O]548    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)549    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)550    (t x : ConcreteSurface O pi u a b) (ht : t = surfaceT O pi u a b)551    (hx : x = surfaceX O pi u a b) (beta : BlowupRestriction (ConcreteSurface O pi u a b) t x)552    (D : TwoChartCurveData (ConcreteSurface O pi u a b) t x beta) (f : ConcreteSurface O pi u a b)553    (G : GluedGenerators (ConcreteSurface O pi u a b) t x beta (curveDataDegree D))554    (hf : ∀ j : ℕ, surfaceToCechInput (ConcreteSurface O pi u a b) t x j f =555    (cechInputLattice (ConcreteSurface O pi u a b) t x j).mkQ556    (gluedFunctionPair (ConcreteSurface O pi u a b) t x G j))557    (hG : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk558    ((chartExceptional (ConcreteSurface O pi u a b) t x)^j) (G.left j)} = leftLevelKernel D j ∧559    Ideal.span {Ideal.Quotient.mk ((chartExceptional (ConcreteSurface O pi u a b) x t)^j)560    (G.right j)} = rightLevelKernel D j) (n : ℕ) (e : Fin n ≃ AllPoints D) (B : Fin n → Type)561    [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)] (eB : ∀ j, B j ≃+*562    (localRing D (e j) ⧸ Ideal.span {localCurve D (e j)}))563    (hB : ∀ (j : Fin n) (c : O), (eB j) (algebraMap O (B j) c) = Ideal.Quotient.mk564    (Ideal.span {localCurve D (e j)}) (localFromSurface D (e j)565    (algebraMap O (ConcreteSurface O pi u a b) c))) :566    ∃ ψ : ((ConcreteSurface O pi u a b) ⧸ Ideal.span {f}) →ₐ[O] ∀ j, B j, Function.Injective ψ ∧567        Module.length O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) =568        (chooseTwo (curveDataDegree D) : ℕ∞) ∧ ∀ (r : (ConcreteSurface O pi u a b)) (j : Fin n),569        (eB j) (ψ (Ideal.Quotient.mk (Ideal.span {f}) r) j) = Ideal.Quotient.mk570        (Ideal.span {localCurve D (e j)}) (localFromSurface D (e j) r) := by571  subst ht hx572  exact concrete_index_map_reindexed O pi hpi u a b ha beta D f G hf hG n e B eB hB573 574/-- All common, left-only and right-only point multiplicities of two-chart curve data of a curve575of multiplicity `d` are positive, with the chart parameters given up to equality. -/576private theorem cell_datum_multiplicities_pos_of_eq (O : Type) [CommRing O] [IsDomain O]577    [IsDiscreteValuationRing O]578    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)579    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)580    (t x : ConcreteSurface O pi u a b) (ht : t = surfaceT O pi u a b)581    (hx : x = surfaceX O pi u a b) [IsLocalRing (ConcreteSurface O pi u a b)] (d : ℕ)582    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))583    (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {t, x})584    (e : ((BlowupChart (ConcreteSurface O pi u a b) t x) ⧸ chartExceptional585    (ConcreteSurface O pi u a b) t x) ≃+* Polynomial586    (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))587    (he : ∀ r : (ConcreteSurface O pi u a b), e (Ideal.Quotient.mk588    (chartExceptional (ConcreteSurface O pi u a b) t x)589    ((chartBase (ConcreteSurface O pi u a b) t x) r)) = Polynomial.C590    (IsLocalRing.residue (ConcreteSurface O pi u a b) r))591    (heZ : e (Ideal.Quotient.mk (chartExceptional (ConcreteSurface O pi u a b) t x)592    (chartSlope (ConcreteSurface O pi u a b) t x)) = Polynomial.X)593    (beta : BlowupRestriction (ConcreteSurface O pi u a b) t x)594    (D : TwoChartCurveData (ConcreteSurface O pi u a b) t x beta)595    (hl : ∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap596    (BlowupChart (ConcreteSurface O pi u a b) t x) (leftPoint D s)597    (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)598    (BlowupChart (ConcreteSurface O pi u a b) t x) (c i) *599    (chartSlope (ConcreteSurface O pi u a b) t x)^i.val) ∧600    (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)601    (BlowupChart (ConcreteSurface O pi u a b) t x) (c i) *602    (chartSlope (ConcreteSurface O pi u a b) t x)^i.val) ∈ leftPoint D s)603    (hr : ∀ s : D.ι ⊕ D.ιinf, Ideal.span {rightData D s} = Ideal.span604    {completedPointMap (BlowupChart (ConcreteSurface O pi u a b) x t) (rightPoint D s)605    (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)606    (BlowupChart (ConcreteSurface O pi u a b) x t) (c i) *607    (chartSlope (ConcreteSurface O pi u a b) x t)^(d - i.val))} ∧608    (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)609    (BlowupChart (ConcreteSurface O pi u a b) x t) (c i) *610    (chartSlope (ConcreteSurface O pi u a b) x t)^(d - i.val)) ∈ rightPoint D s) :611    (∀ i : D.ι, 0 < commonMultiplicity D i) ∧ (∀ k : D.ι0, 0 < leftMultiplicity D (Sum.inr k)) ∧ ∀612        l : D.ιinf, 0 < rightMultiplicity D (Sum.inr l) := by613  subst ht hx614  refine ⟨fun i ↦ ?_, fun k ↦ cell_datum_left_multiplicity_pos O pi hpi u a b ha d c hne e he heZ615    beta D hl (Sum.inr k), cell_datum_right_multiplicity_pos O pi hpi u a b ha d c hne beta D hr⟩616  rw [← (two_chart_common_multiplicity_eq (ConcreteSurface O pi u a b) _ _ beta D i).1]617  exact cell_datum_left_multiplicity_pos O pi hpi u a b ha d c hne e he heZ beta D hl (Sum.inl i)618 619private theorem two_chart_datum_concrete_instances_of_eq (O : Type) [CommRing O] [IsDomain O]620    [IsDiscreteValuationRing O]621    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)622    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)623    (t x : ConcreteSurface O pi u a b) (ht : t = surfaceT O pi u a b)624    (hx : x = surfaceX O pi u a b) (beta : BlowupRestriction (ConcreteSurface O pi u a b) t x)625    (D : TwoChartCurveData (ConcreteSurface O pi u a b) t x beta) :626    (∀ s : D.ι ⊕ D.ι0, IsNoetherianRing (CompletedLocalAt627        (BlowupChart (ConcreteSurface O pi u a b) t x) (leftPoint D s)) ∧ Function.Injective628        (fun y : (CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b) t x)629        (leftPoint D s)) => (completedPointMap (BlowupChart (ConcreteSurface O pi u a b) t x)630        (leftPoint D s)) ((chartBase (ConcreteSurface O pi u a b) t x) t) * y)) ∧631        (∀ s : D.ι ⊕ D.ιinf, IsNoetherianRing (CompletedLocalAt632        (BlowupChart (ConcreteSurface O pi u a b) x t) (rightPoint D s)) ∧ Function.Injective633        (fun y : (CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b) x t)634        (rightPoint D s)) => (completedPointMap (BlowupChart (ConcreteSurface O pi u a b) x t)635        (rightPoint D s)) ((chartBase (ConcreteSurface O pi u a b) x t) x) * y)) ∧ ∀ p : AllPoints636        D, IsNoetherianRing (localRing D p) ∧ ∃ _ : IsLocalRing (localRing D p), IsAdicComplete637        (IsLocalRing.maximalIdeal (localRing D p)) (localRing D p) ∧ localException D p ∈638        IsLocalRing.maximalIdeal (localRing D p) := by639  subst ht hx640  exact two_chart_datum_concrete_instances O pi hpi u a b ha beta D641 642private theorem concrete_two_chart_glued_generators_exist_of_eq (O : Type) [CommRing O] [IsDomain O]643    [IsDiscreteValuationRing O]644    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)645    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)646    (t x : ConcreteSurface O pi u a b) (ht : t = surfaceT O pi u a b)647    (hx : x = surfaceX O pi u a b) (beta : BlowupRestriction (ConcreteSurface O pi u a b) t x)648    (D : TwoChartCurveData (ConcreteSurface O pi u a b) t x beta) :649    ∃ f : ConcreteSurface O pi u a b, ∃ G : GluedGenerators (ConcreteSurface O pi u a b) t x beta650        (curveDataDegree D), (∀ j : ℕ, surfaceToCechInput (ConcreteSurface O pi u a b) t x j f =651        (cechInputLattice (ConcreteSurface O pi u a b) t x j).mkQ652        (gluedFunctionPair (ConcreteSurface O pi u a b) t x G j)) ∧ ∀ j : ℕ, Ideal.span653        {Ideal.Quotient.mk ((chartExceptional (ConcreteSurface O pi u a b) t x)^j) (G.left j)} =654        leftLevelKernel D j ∧ Ideal.span {Ideal.Quotient.mk655        ((chartExceptional (ConcreteSurface O pi u a b) x t)^j) (G.right j)} = rightLevelKernel D656        j := by657  subst ht hx658  exact concrete_two_chart_glued_generators_exist O pi hpi u a b ha beta D659 660private theorem fixed_tangent_cell_curve_datum_of_eq (O : Type) [CommRing O] [IsDomain O]661    [IsDiscreteValuationRing O]662    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)663    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)664    (t x : ConcreteSurface O pi u a b) (ht : t = surfaceT O pi u a b)665    (hx : x = surfaceX O pi u a b) [IsDomain (ConcreteSurface O pi u a b)]666    [IsRegularLocalRing (ConcreteSurface O pi u a b)]667    (S : SurfaceData O (ConcreteSurface O pi u a b)) (hS : S.t = t ∧ S.x = x)668    (e : ((BlowupChart (ConcreteSurface O pi u a b) t x) ⧸ chartExceptional669    (ConcreteSurface O pi u a b) t x) ≃+* Polynomial670    (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))671    (he : ∀ r : (ConcreteSurface O pi u a b), e (Ideal.Quotient.mk672    (chartExceptional (ConcreteSurface O pi u a b) t x)673    ((chartBase (ConcreteSurface O pi u a b) t x) r)) = Polynomial.C674    (IsLocalRing.residue (ConcreteSurface O pi u a b) r))675    (heZ : e (Ideal.Quotient.mk (chartExceptional (ConcreteSurface O pi u a b) t x)676    (chartSlope (ConcreteSurface O pi u a b) t x)) = Polynomial.X)677    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) (s : State)678    (d : ℕ) (J : Ideal (ConcreteSurface O pi u a b))679    (hJ : J ∈ fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv)680    (beta : BlowupRestriction (ConcreteSurface O pi u a b) t x) :681    ∃ (f : (ConcreteSurface O pi u a b)) (c : Fin (d+1) → (ConcreteSurface O pi u a b))682        (D : TwoChartCurveData (ConcreteSurface O pi u a b) t x beta), J = Ideal.span {f} ∧ f = ∑ i683        : Fin (d+1), c i * t^(d - i.val) * x^i.val ∧684        (∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap685        (BlowupChart (ConcreteSurface O pi u a b) t x) (leftPoint D s)686        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)687        (BlowupChart (ConcreteSurface O pi u a b) t x) (c i) *688        (chartSlope (ConcreteSurface O pi u a b) t x)^i.val) ∧689        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)690        (BlowupChart (ConcreteSurface O pi u a b) t x) (c i) *691        (chartSlope (ConcreteSurface O pi u a b) t x)^i.val) ∈ leftPoint D s) ∧692        (∀ s : D.ι ⊕ D.ιinf, Ideal.span {rightData D s} = Ideal.span693        {completedPointMap (BlowupChart (ConcreteSurface O pi u a b) x t) (rightPoint D s)694        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)695        (BlowupChart (ConcreteSurface O pi u a b) x t) (c i) *696        (chartSlope (ConcreteSurface O pi u a b) x t)^(d - i.val))} ∧697        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)698        (BlowupChart (ConcreteSurface O pi u a b) x t) (c i) *699        (chartSlope (ConcreteSurface O pi u a b) x t)^(d - i.val)) ∈ rightPoint D s) ∧700        (∀ s : D.ι ⊕ D.ι0, strictTransformAt (ConcreteSurface O pi u a b) t x (leftPoint D s) d J =701        Ideal.span {leftData D s}) ∧ (∀ s : D.ι ⊕ D.ιinf, strictTransformAt702        (ConcreteSurface O pi u a b) x t (rightPoint D s) d J = Ideal.span {rightData D s}) ∧703        MatchesDivisor e D Dv ∧ curveDataDegree D = exceptionalDegree704        (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) Dv := by705  subst ht hx706  exact fixed_tangent_cell_curve_datum O pi hpi u a b ha S hS e he heZ Dv s d J hJ beta707 708/-- If a form `∑ᵢ cᵢ tᵈ⁻ⁱ xⁱ` of degree `d` does not lie in `(t, x)ᵈ⁺¹`, then some coefficient709`cᵢ` does not lie in `(t, x)`. -/710private theorem exists_coeff_notMem_span_of_notMem_pow {R : Type} [CommRing R] (t x : R) (d : ℕ)711    (c : Fin (d + 1) → R)712    (h : ∑ i : Fin (d + 1), c i * t ^ (d - i.val) * x ^ i.val ∉ Ideal.span {t, x} ^ (d + 1)) :713    ∃ i : Fin (d + 1), c i ∉ Ideal.span {t, x} := by714  by_contra! hc715  refine h (Ideal.sum_mem _ fun i _ ↦ ?_)716  have := Ideal.mul_mem_mul (hc i) (Ideal.mul_mem_mul717    (Ideal.pow_mem_pow (Ideal.subset_span (by simp) : t ∈ Ideal.span ({t, x} : Set R)) (d - i.val))718    (Ideal.pow_mem_pow (Ideal.subset_span (by simp) : x ∈ Ideal.span ({t, x} : Set R)) i.val))719  rw [← Ideal.IsTwoSided.pow_add, Nat.sub_add_cancel (Nat.lt_succ_iff.mp i.isLt)] at this720  rwa [mul_assoc, Ideal.IsTwoSided.pow_succ]721 722/-- **The index map of a cell.** For a cell ideal `J` of a concrete member and child quotients723`B j ≅ R_j ⧸ Φ J j`, there is an injective `O`-algebra map `R ⧸ J → ∏ B j` with cokernel of length724`d(d-1)/2` (`d` the cell degree), compatible with the child maps `α j`. -/725theorem cell_member_index_map (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)Proposition 4.4726    (J : Ideal m.R) (hJ : J ∈ m.toMeasured.cell c) (B : m.toMeasured.childIdx c → Type)727    [∀ j, CommRing (B j)] [∀ j, Algebra m.O (B j)] (eB : ∀ j, B j ≃+* (D.mc j).R ⧸ D.Φ J j)728    (hB : ∀ (j : m.toMeasured.childIdx c) (r : m.O), eB j (algebraMap m.O (B j) r) =729    Ideal.Quotient.mk (D.Φ J j) (algebraMap m.O (D.mc j).R r)) :730    ∃ ψ : (m.R ⧸ J) →ₐ[m.O] ∀ j, B j, Function.Injective ψ ∧ Module.length m.O731        ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = (chooseTwo (m.toMeasured.cellDegree c) : ℕ∞)732        ∧ ∀ (r : m.R) (j : m.toMeasured.childIdx c), eB j (ψ (Ideal.Quotient.mk J r) j) =733        Ideal.Quotient.mk (D.Φ J j) (D.alpha j r) := by734  set d := m.toMeasured.cellDegree c735  obtain ⟨beta⟩ := actual_blowup_restriction_exists m.R m.S.t m.S.x736  obtain ⟨f, cf, Df, hJf, hcf, hl, hr, hstl, hstr, hmatch, hdeg⟩ :=737    fixed_tangent_cell_curve_datum_of_eq m.O m.pi m.hpi m.u m.a m.b m.ha m.S.t m.S.x m.hS_t m.hS_x738      m.S ⟨rfl, rfl⟩ D.e D.he D.heZ c.2.1 m.s d J hJ beta739  have hdeg' : curveDataDegree Df = d := hdeg.trans c.2.2.1740  have hreg : RegularParameterPair m.R m.S.t m.S.x := by741    rw [m.hS_t, m.hS_x]742    exact concrete_surface_regular_pair_tx m.O m.pi m.hpi.ne_zero m.u m.a m.b m.ha743  have hregSwap : RegularParameterPair m.R m.S.x m.S.t := by744    rw [m.hS_t, m.hS_x]745    exact concrete_surface_regular_pair_xt m.O m.pi m.hpi.ne_zero m.u m.a m.b m.ha746  have hmultJ := has_tangent_divisor_multiplicity m.O m.R m.S hreg J d c.2.1 hJ.2747  have hmax : IsLocalRing.maximalIdeal m.R = Ideal.span {m.S.t, m.S.x} := by748    rw [concrete_surface_maximalIdeal_eq m.O m.pi m.hpi m.u m.a m.b m.ha, surfaceParameterIdeal,749        m.hS_t, m.hS_x]750  have hd : f ∈ (Ideal.span {m.S.t, m.S.x})^d := by751    have := hmultJ.1; rwa [hJf, Ideal.span_singleton_le_iff_mem, hmax] at this752  have hmult : f ∉ (Ideal.span {m.S.t, m.S.x})^(d+1) := by753    have := hmultJ.2; rwa [hJf, Ideal.span_singleton_le_iff_mem, hmax] at this754  have hne : ∃ i : Fin (d+1), cf i ∉ Ideal.span {m.S.t, m.S.x} :=755    exists_coeff_notMem_span_of_notMem_pow m.S.t m.S.x d cf (hcf ▸ hmult)756  have hpos := cell_datum_multiplicities_pos_of_eq m.O m.pi m.hpi m.u m.a m.b m.ha m.S.t m.S.x757    m.hS_t m.hS_x d cf hne D.e D.he D.heZ beta Df hl hr758  obtain ⟨ee, hee⟩ := cell_datum_point_equiv m c D J beta Df ⟨hstl, hstr⟩ hmatch hpos759  choose ι hι1 hι2 using hee760  obtain ⟨f', G, hf', hG⟩ := concrete_two_chart_glued_generators_exist_of_eq m.O m.pi m.hpi m.u m.a761    m.b m.ha m.S.t m.S.x m.hS_t m.hS_x beta Df762  have : (Ideal.span ({m.S.t, m.S.x} : Set m.R)).IsMaximal := by763    rw [m.hS_t, m.hS_x]764    exact concrete_surface_parameterIdeal_isMaximal m.O m.pi m.hpi m.u m.a m.b m.ha765  have : IsNoetherianRing m.R := concrete_surface_isNoetherianRing m.O m.pi m.u m.a m.b766  have : IsNoetherianRing (BlowupChart m.R m.S.t m.S.x) :=767    blowupChart_concrete_isNoetherianRing m.O m.pi m.u m.a m.b _ _768  have : IsNoetherianRing (BlowupChart m.R m.S.x m.S.t) :=769    blowupChart_concrete_isNoetherianRing m.O m.pi m.u m.a m.b _ _770  have hregF := fun j ↦ two_chart_left_generators_regular_on_overlap m.R m.S.t m.S.x beta Df _ G771    hG hreg hregSwap j772  have h910 := two_chart_datum_concrete_instances_of_eq m.O m.pi m.hpi m.u m.a m.b m.ha m.S.t m.S.x773    m.hS_t m.hS_x beta Df774  have hmem := strict_transforms_give_level_lattice_membership m.R m.S.t m.S.x beta Df775    (curveDataDegree Df) G hG f (hdeg' ▸ hd) (fun s ↦ by rw [hdeg', ← hJf]; exact hstl s)776    (fun s ↦ by rw [hdeg', ← hJf]; exact hstr s)777  have hJf' : J = Ideal.span {f'} := hJf.trans <| parent_ideal_unique_of_level_lattice m.R m.S.t778    m.S.x hreg hregSwap beta _ G hregF f' hf' f hmem (hdeg' ▸ hmult)779  have hmapΦ : ∀ j, Ideal.span {localCurve Df (ee j)} =780      (D.Φ J j).map (((D.Eq j).symm.trans (ι j) : (D.mc j).R ≃+* localRing Df (ee j)) :781        (D.mc j).R →+* localRing Df (ee j)) := by782    intro j783    rw [cell_child_Phi_eq_map m c D J j, Ideal.map_map, ← hι2 j]784    congr 1785    ext y786    simp787  let qE : ∀ j, (D.mc j).R ⧸ D.Φ J j ≃+* localRing Df (ee j) ⧸ Ideal.span {localCurve Df (ee j)} :=788    fun j => Ideal.quotientEquiv _ _ ((D.Eq j).symm.trans (ι j)) (hmapΦ j)789  have hqE : ∀ j (r : m.R), qE j (Ideal.Quotient.mk (D.Φ J j) (D.alpha j r)) =790      Ideal.Quotient.mk _ (localFromSurface Df (ee j) r) := by791    intro j r792    change Ideal.Quotient.mk _ (ι j793        ((D.Eq j).symm (D.Eq j (divisorFromSurface m.R m.S.t m.S.x D.e c.2.1 D.hinf794      (D.point j) r)))) = _795    rw [RingEquiv.symm_apply_apply, hι1]796  let eB' : ∀ j, B j ≃+* localRing Df (ee j) ⧸ Ideal.span {localCurve Df (ee j)} :=797    fun j => (eB j).trans (qE j)798  have hB' : ∀ (j : m.toMeasured.childIdx c) (r : m.O), eB' j (algebraMap m.O (B j) r) =799      Ideal.Quotient.mk (Ideal.span {localCurve Df (ee j)})800          (localFromSurface Df (ee j) (algebraMap m.O m.R r)) := by801    intro j r802    change qE j (eB j (algebraMap m.O (B j) r)) = _803    rw [hB, ← (D.alpha j).commutes r, hqE]804  obtain ⟨ψ', hinj, hlen, hform⟩ := concrete_index_map_reindexed_of_eq m.O m.pi m.hpi m.u m.a m.b805    m.ha m.S.t m.S.x m.hS_t m.hS_x beta Df f' G hf' hG _ ee B eB' hB'806  let E := Ideal.quotientEquivAlgOfEq m.O hJf'807  refine ⟨ψ'.comp E.toAlgHom, hinj.comp E.injective, ?_, fun r j ↦ (qE j).injective ?_⟩808  · rw [AlgHom.comp_toLinearMap, LinearMap.range_comp_of_range_eq_top _809      (LinearMap.range_eq_top.mpr E.surjective), hlen, hdeg']810  · rw [hqE]811    exact hform r j812 813private theorem one_le_chooseTwo_of_selfPattern (s : State) (hv : s.Valid)814    (hnt : s.terminal = false)815    (P : TangentPattern s.degree)816    (hA : Allowed s P) (hs : SelfPattern s P) : 1 ≤ chooseTwo P.d.val := by817  cases s with818  | crossing a b c h =>819    obtain ⟨a', c', h', -⟩ := hs820    cases h'821  | single a c₀ =>822    obtain ⟨a', c', h', hch⟩ := hs823    cases h'824    have hc : 2 ≤ c₀ := by825      rcases hv with ⟨-, hc0⟩826      by_contra hlt827      have : c₀ = 1 := by omega828      subst this829      simp [State.terminal] at hnt830    have := (self_patterns_of_single_state a c₀ 2 hv.1 hc).1 P hA ⟨a, c₀, rfl, hch⟩831    rw [this.1]832    unfold chooseTwo833    apply Nat.div_pos _ (by norm_num)834    rcases c₀ with _ | _ | k835    · omega836    · omega837    · simp only [Nat.add_sub_cancel]; nlinarith838 839/-- The child quotients `B j ≅ R_j ⧸ Φ J j` of a cell ideal are free and finite over `O_j`. -/840private theorem cellChild_free_finite (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)841    (J : Ideal m.R) (hJ : J ∈ m.toMeasured.cell c) (B : m.toMeasured.childIdx c → Type)842    [∀ j, CommRing (B j)] (eB : ∀ j, B j ≃+* (D.mc j).R ⧸ D.Φ J j)843    [∀ j, Algebra (D.mc j).O (B j)] (hBalg : ∀ (j : m.toMeasured.childIdx c)844    (o : (D.mc j).O), eB j (algebraMap (D.mc j).O (B j) o) = Ideal.Quotient.mk (D.Φ J j)845    (algebraMap (D.mc j).O (D.mc j).R o)) (j : m.toMeasured.childIdx c) :846    Module.Free (D.mc j).O (B j) ∧ Module.Finite (D.mc j).O (B j) := by847  have hmem : D.Φ J j ∈ (D.mc j).toMeasured.stateSet :=848    (cell_child_bijOn m c D).mapsTo hJ j (Set.mem_univ j)849  obtain ⟨_, _, -⟩ := concrete_member_curve_order_free (D.mc j) _ hmem850  let e : B j ≃ₐ[(D.mc j).O] (D.mc j).R ⧸ D.Φ J j :=851    AlgEquiv.ofRingEquiv (f := eB j) fun o ↦ by rw [hBalg j o]; rfl852  exact ⟨.of_equiv e.symm.toLinearEquiv, .equiv e.symm.toLinearEquiv⟩853 854/-- Termination data for the children of a cell ideal with algebra type `σ`: each child has an855algebra type, and its order defect is at most that of `R ⧸ J`, strictly smaller on self cells. -/856private theorem cell_child_termination_data (m : ConcreteMember) (c : m.cellIndex)857    (hnt : m.s.terminal = false) (D : CellChildData m c) (J : Ideal m.R)858    (hJ : J ∈ m.toMeasured.cell c) (B : m.toMeasured.childIdx c → Type) [∀ j, CommRing (B j)]859    [∀ j, Algebra m.O (B j)] (eB : ∀ j, B j ≃+* (D.mc j).R ⧸ D.Φ J j)860    (hB : ∀ (j : m.toMeasured.childIdx c) (r : m.O), eB j (algebraMap m.O (B j) r) =861    Ideal.Quotient.mk (D.Φ J j) (algebraMap m.O (D.mc j).R r)) [∀ j, Algebra (D.mc j).O (B j)]862    [∀ j, IsScalarTower m.O (D.mc j).O (B j)] (hBalg : ∀ (j : m.toMeasured.childIdx c)863    (o : (D.mc j).O), eB j (algebraMap (D.mc j).O (B j) o) = Ideal.Quotient.mk (D.Φ J j)864    (algebraMap (D.mc j).O (D.mc j).R o)) (σ : FactorType) (hσ : HasAlgebraType m.O (m.R ⧸ J) σ) :865    ∀ j, (∃ τ : FactorType, HasAlgebraType (D.mc j).O (B j) τ) ∧866        (orderDefect (D.mc j).O (B j)).toNat ≤ (orderDefect m.O (m.R ⧸ J)).toNat ∧867        (m.toMeasured.IsSelfCell c → (orderDefect (D.mc j).O (B j)).toNat <868        (orderDefect m.O (m.R ⧸ J)).toNat) := by869  obtain ⟨ψ, hψi, hlen, -⟩ := cell_member_index_map m c D J hJ B eB hB870  obtain ⟨hfree, hfin, -⟩ := concrete_member_curve_order_free m J hJ.1871  have hfr := cellChild_free_finite m c D J hJ B eB hBalg872  have key := @concrete_termination_data_of_index_map m _ (fun j => D.mc j) _ _ _873    (fun j => m.toMeasured.childDelta c j) (fun j => (D.child j).hrank)874    (fun j => by rw [← (D.child j).hpi]; exact (D.mc j).hpi) J B _ _ _ _ (fun j => (hfr j).2)875    (fun j => (hfr j).1) ψ hψi (chooseTwo (m.toMeasured.cellDegree c)) hlen hfin hfree σ hσ876  intro j877  obtain ⟨h1, h2, h3⟩ := key j878  exact ⟨h1, h2, fun hs ↦879    h3 (one_le_chooseTwo_of_selfPattern m.s m.toMeasured.valid hnt c.1.1 c.1.2 hs)⟩880 881/-- **Type additivity.** If the children `B j` of a cell ideal `J` have algebra types `τ j`, then882`R ⧸ J` has algebra type `∑ j, scaleType δ_j (τ j)`. -/883private theorem cell_child_type_add (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)884    (J : Ideal m.R) (hJ : J ∈ m.toMeasured.cell c) (B : m.toMeasured.childIdx c → Type)885    [∀ j, CommRing (B j)] [∀ j, Algebra m.O (B j)] (eB : ∀ j, B j ≃+* (D.mc j).R ⧸ D.Φ J j)886    (hB : ∀ (j : m.toMeasured.childIdx c) (r : m.O), eB j (algebraMap m.O (B j) r) =887    Ideal.Quotient.mk (D.Φ J j) (algebraMap m.O (D.mc j).R r)) [∀ j, Algebra (D.mc j).O (B j)]888    [∀ j, IsScalarTower m.O (D.mc j).O (B j)] (hBalg : ∀ (j : m.toMeasured.childIdx c)889    (o : (D.mc j).O), eB j (algebraMap (D.mc j).O (B j) o) = Ideal.Quotient.mk (D.Φ J j)890    (algebraMap (D.mc j).O (D.mc j).R o)) (τ : m.toMeasured.childIdx c → FactorType)891    (hτ : ∀ j, HasAlgebraType (D.mc j).O (B j) (τ j)) :892    HasAlgebraType m.O (m.R ⧸ J) (∑ j, scaleType (m.toMeasured.childDelta c j) (τ j)) := by893  obtain ⟨ψ, hψ, hlen, -⟩ := cell_member_index_map m c D J hJ B eB hB894  have hfr := cellChild_free_finite m c D J hJ B eB hBalg895  have : ∀ j, Module.Free (D.mc j).O (B j) := fun j ↦ (hfr j).1896  have : ∀ j, Module.Finite (D.mc j).O (B j) := fun j ↦ (hfr j).2897  exact concrete_type_add_of_index_map m _ D.mc (m.toMeasured.childDelta c)898    (fun j => (D.child j).hrank) (fun j => by rw [← (D.child j).hpi]; exact (D.mc j).hpi) J B ψ hψ899        _ hlen τ hτ900 901/-! ### Every state ideal lies in a cell -/902 903/-- Every ideal in a state set of a concrete surface has a positive multiplicity `d`. -/904private theorem state_ideal_has_multiplicity (O : Type) [CommRing O] [IsDomain O]905    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]906    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)907    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]908    [IsRegularLocalRing (ConcreteSurface O pi u a b)]909    (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSt : S.t = surfaceT O pi u a b) (s : State)910    (J : Ideal (ConcreteSurface O pi u a b))911    (hJ : J ∈ surfaceStateSet O (ConcreteSurface O pi u a b) S s) :912    ∃ d : ℕ, 0 < d ∧ HasMultiplicity (ConcreteSurface O pi u a b) J d := by913  classical914  set R := ConcreteSurface O pi u a b915  obtain ⟨f, hf⟩ := hJ.1916  have hfm : f ∈ IsLocalRing.maximalIdeal R :=917    surface_state_generator_mem_maximal O R S s J hJ f hf918  -- contact is finite919  have hfin : ∃ c : ℕ, idealContact R J S.t = c := by920    have h2 := hJ.2.2921    cases s with922    | single a' c => exact ⟨c, h2.2.2⟩923    | crossing a' b' c h => exact ⟨c, h2.2.2.1⟩924  have hf0 : f ≠ 0 := by925    intro h0926    obtain ⟨c, hc⟩ := hfin927    have hJ0 : J = ⊥ := by rw [hf, h0]; simp928    unfold idealContact at hc929    rw [hJ0, hSt] at hc930    obtain ⟨q, -⟩ := concrete_surface_quotient_T_equiv O pi hpi u a b ha931    let e : (R ⧸ (⊥ ⊔ Ideal.span {surfaceT O pi u a b})) ≃+*932        (PowerSeries (IsLocalRing.ResidueField O) ⧸933          Ideal.span {(0 : PowerSeries (IsLocalRing.ResidueField O))}) :=934      (Ideal.quotEquivOfEq (by simp)).trans935        (q.trans ((RingEquiv.quotientBot _).symm.trans936          (Ideal.quotEquivOfEq (by simp)).symm))937    have := quotient_ring_length_intrinsic _ _ _ _ e938    have h3 := (powerSeries_quotient_length_eq_order (IsLocalRing.ResidueField O) 0).1939    rw [hc] at this940    rw [← this] at h3941    simp at h3942  have hne : IsLocalRing.maximalIdeal R ≠ ⊤ := IsLocalRing.maximalIdeal.isMaximal R |>.ne_top943  have hK := iInf_sup_pow_eq_of_isLocalRing R (IsLocalRing.maximalIdeal R) ⊥ hne944  have hex : ∃ n : ℕ, f ∉ (IsLocalRing.maximalIdeal R)^(n+1) := by945    by_contra hcon946    push Not at hcon947    have : f ∈ (⨅ n : ℕ, ⊥ ⊔ (IsLocalRing.maximalIdeal R)^n) := by948      rw [Ideal.mem_iInf]949      intro n950      rcases n with _ | n951      · simp952      · simpa using hcon n953    rw [hK] at this954    exact hf0 (by simpa using this)955  have hpos : Nat.find hex ≠ 0 := fun h0 ↦ by956    have := Nat.find_spec hex957    rw [h0] at this958    exact this (by simpa using hfm)959  refine ⟨Nat.find hex, Nat.pos_of_ne_zero hpos, ?_,960    fun hle ↦ Nat.find_spec hex (hle (hf ▸ Ideal.mem_span_singleton_self f))⟩961  rw [hf, Ideal.span_le, Set.singleton_subset_iff]962  obtain ⟨k, hk⟩ : ∃ k, Nat.find hex = k + 1 := ⟨Nat.find hex - 1, by omega⟩963  rw [hk]964  exact not_not.mp (Nat.find_min hex (show k < Nat.find hex by omega))965 966private theorem le_and_lt_iff_of_natCast_eq_add (d c : ℕ) (ℓ : ℕ∞) (h : (c : ℕ∞) = (d : ℕ∞) + ℓ) :967    d ≤ c ∧ (d < c ↔ ℓ ≠ 0) := by968  induction ℓ using ENat.recTopCoe with969  | top => simp at h970  | coe n =>971    obtain rfl : c = d + n := by exact_mod_cast h972    exact ⟨by omega, by simp; omega⟩973 974/-- For a state ideal `J = (f)` with `f = ∑ cᵢ tᵈ⁻ⁱ xⁱ` of multiplicity `d`, the multiplicity is975bounded by the contact orders of the state, with strict inequality exactly when the corresponding976boundary coefficient lies in the maximal ideal. -/977private theorem state_ideal_multiplicity_le_contacts (O : Type) [CommRing O] [IsDomain O]978    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]979    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)980    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]981    [IsRegularLocalRing (ConcreteSurface O pi u a b)]982    (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSt : S.t = surfaceT O pi u a b)983    (hSx : S.x = surfaceX O pi u a b) (s : State) (J : Ideal (ConcreteSurface O pi u a b))984    (hJ : J ∈ surfaceStateSet O (ConcreteSurface O pi u a b) S s) (d : ℕ)985    (f : (ConcreteSurface O pi u a b)) (hf : J = Ideal.span {f})986    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))987    (hc : f = (∑ i : Fin (d + 1), c i * (surfaceT O pi u a b) ^ (d - i.val) *988    (surfaceX O pi u a b) ^ i.val)) :989    match s with990    | State.single _ c₀ =>991      d ≤ c₀ ∧ (d < c₀ ↔ c (Fin.last d) ∈ IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b))992    | State.crossing _ _ c₀ h₀ =>993      d ≤ c₀ ∧ (d < c₀ ↔ c (Fin.last d) ∈ IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b)) ∧994        d ≤ h₀ ∧ (d < h₀ ↔ c 0 ∈ IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b)) := by995  set t := surfaceT O pi u a b996  set x := surfaceX O pi u a b997  have hpi0 : pi ≠ 0 := hpi.ne_zero998  have hmax : IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b) = Ideal.span {t, x} := by999    rw [← S.parameters, hSt, hSx]1000  have hmax' : IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b) = Ideal.span {x, t} := by1001    rw [hmax, Ideal.span_pair_comm]1002  have : (Ideal.span ({t, x} : Set (ConcreteSurface O pi u a b))).IsMaximal := by1003    rw [← hmax]; exact IsLocalRing.maximalIdeal.isMaximal (ConcreteSurface O pi u a b)1004  have : (Ideal.span ({x, t} : Set (ConcreteSurface O pi u a b))).IsMaximal := by1005    rw [← hmax']; exact IsLocalRing.maximalIdeal.isMaximal (ConcreteSurface O pi u a b)1006  -- t-contact1007  have ht := (boundary_contact_of_twisted_generator (ConcreteSurface O pi u a b) t x1008    (concrete_surface_regular_pair_tx O pi hpi0 u a b ha) d f c hc).21009  have htn := boundary_contact_length_ne_zero_iff (ConcreteSurface O pi u a b) t x hmax d c1010  -- x-contact1011  have hc' : f = ∑ j : Fin (d+1), c (Fin.rev j) * x^(d - j.val) * t^j.val := by1012    rw [hc, ← Equiv.sum_comp Fin.revPerm]1013    refine Finset.sum_congr rfl fun j _ => ?_1014    simp only [Fin.revPerm_apply, Fin.val_rev]1015    have hj := j.isLt1016    rw [show d - (d + 1 - (j.val + 1)) = j.val by omega,1017      show d + 1 - (j.val + 1) = d - j.val by omega]1018    ring1019  have hx := (boundary_contact_of_twisted_generator (ConcreteSurface O pi u a b) x t1020    (concrete_surface_regular_pair_xt O pi hpi0 u a b ha) d f (fun j => c (Fin.rev j)) hc').21021  have hxn := boundary_contact_length_ne_zero_iff (ConcreteSurface O pi u a b) x t hmax' d1022      (fun j => c (Fin.rev j))1023  simp only [Fin.rev_last] at hxn1024  obtain ⟨-, -, hs⟩ := hJ1025  rw [hf] at hs1026  cases s with1027  | single a' c₀ =>1028    obtain ⟨-, -, h1⟩ := hs1029    unfold idealContact at h11030    rw [hSt, ht] at h11031    exact (le_and_lt_iff_of_natCast_eq_add d c₀ _ h1.symm).imp_right (·.trans htn)1032  | crossing a' b' c₀ h₀ =>1033    obtain ⟨-, -, h1, h2⟩ := hs1034    unfold idealContact at h1 h21035    rw [hSt, ht] at h11036    rw [hSx, hx] at h21037    have e1 := le_and_lt_iff_of_natCast_eq_add d c₀ _ h1.symm1038    have e2 := le_and_lt_iff_of_natCast_eq_add d h₀ _ h2.symm1039    exact ⟨e1.1, e1.2.trans htn, e2.1, e2.2.trans hxn⟩1040 1041private theorem allowed_pattern_of_cell_ideal (O : Type) [CommRing O] [IsDomain O]1042    [IsDiscreteValuationRing O]1043    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)1044    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)1045    [IsDomain (ConcreteSurface O pi u a b)] [IsRegularLocalRing (ConcreteSurface O pi u a b)]1046    (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSt : S.t = surfaceT O pi u a b)1047    (hSx : S.x = surfaceX O pi u a b) (s : State) (J : Ideal (ConcreteSurface O pi u a b))1048    (hJ : J ∈ surfaceStateSet O (ConcreteSurface O pi u a b) S s) (d : ℕ)1049    (f : (ConcreteSurface O pi u a b)) (hf : J = Ideal.span {f})1050    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))1051    (hc : f = (∑ i : Fin (d + 1), c i * (surfaceT O pi u a b) ^ (d - i.val) *1052        (surfaceX O pi u a b) ^ i.val))1053    {k : Type} [Field k] (Dv : ExceptionalDivisor k)1054    (e1 : 0 < Dv (infinityDirection k) ↔ c (Fin.last d) ∈ IsLocalRing.maximalIdeal1055        (ConcreteSurface O pi u a b))1056    (e0 : 0 < Dv (zeroDirection k) ↔ c 0 ∈ IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b))1057    (hs : s.Valid) [Finite k] (hd : 0 < d) (hdeg : exceptionalDegree k Dv = d)1058    (hQ : ∀ Q, 0 < Dv Q → directionDegree k Q ≤ d) (hmult : ∀ Q, Dv Q ≤ d) :1059    ∃ P : TangentPattern s.degree, P.d.val = d ∧ Allowed s P ∧ HasPattern k s Dv P := by1060  have hcon := state_ideal_multiplicity_le_contacts O pi hpi u a b ha S hSt hSx s J hJ1061    d f hf c hc1062  cases s with1063  | single a' c' =>1064    obtain ⟨h1, h2⟩ := hcon1065    exact allowed_pattern_of_divisor k _ hs Dv d hd hdeg hQ hmult ⟨h1, e1.trans h2.symm⟩1066  | crossing a' b' c' h' =>1067    obtain ⟨h1, h2, h3, h4⟩ := hcon1068    exact allowed_pattern_of_divisor k _ hs Dv d hd hdeg hQ hmult1069      ⟨h1, e1.trans h2.symm, h3, e0.trans h4.symm⟩1070 1071/-- The cells of a concrete member cover its state set. -/1072theorem concrete_member_cells_cover (m : ConcreteMember) :Proposition 6.11073    m.toMeasured.stateSet = ⋃ c : m.toMeasured.cellIndex, m.toMeasured.cell c := by1074  ext J1075  simp only [Set.mem_iUnion]1076  refine ⟨fun hJ ↦ ?_, fun ⟨_, hc⟩ ↦ hc.1⟩1077  change J ∈ surfaceStateSet m.O m.R m.S m.s at hJ1078  obtain ⟨d, hd, hmul⟩ := state_ideal_has_multiplicity m.O m.pi m.hpi m.u m.a m.b m.ha m.S1079    m.hS_t m.s J hJ1080  obtain ⟨f, hf⟩ := hJ.11081  have hf1 : f ∈ (IsLocalRing.maximalIdeal m.R)^d :=1082    hmul.1 (hf ▸ Ideal.subset_span (Set.mem_singleton f))1083  have hf2 : f ∉ (IsLocalRing.maximalIdeal m.R)^(d+1) := fun h ↦1084    hmul.2 (by rw [hf, Ideal.span_le, Set.singleton_subset_iff]; exact h)1085  have hmax : IsLocalRing.maximalIdeal m.R = Ideal.span {surfaceT m.O m.pi m.u m.a m.b,1086      surfaceX m.O m.pi m.u m.a m.b} := by1087    rw [← m.hS_t, ← m.hS_x]; exact m.S.parameters.symm1088  obtain ⟨c, hc, i₀, hi₀⟩ := has_multiplicity_initial_form m.R _ _ hmax d f hf1 hf21089  set H : Polynomial (IsLocalRing.ResidueField m.R) :=1090    ∑ i : Fin (d+1), Polynomial.C (IsLocalRing.residue m.R (c i)) * Polynomial.X^i.val with hH1091  have hcoeff : ∀ n : Fin (d+1), H.coeff n = IsLocalRing.residue m.R (c n) := by1092    intro n1093    rw [hH, Polynomial.finsetSum_coeff]1094    simp only [Polynomial.coeff_C_mul_X_pow, Fin.val_inj]1095    simp1096  have hH0 : H ≠ 0 := by1097    intro h01098    have := hcoeff i₀1099    rw [h0, Polynomial.coeff_zero, eq_comm, IsLocalRing.residue_eq_zero_iff] at this1100    exact hi₀ this1101  have hdeg : H.natDegree ≤ d := by1102    rw [hH]1103    refine Polynomial.natDegree_sum_le_of_forall_le _ _ (fun i _ => ?_)1104    exact (Polynomial.natDegree_C_mul_X_pow_le _ _).trans (Nat.lt_succ_iff.mp i.isLt)1105  obtain ⟨Dv, hDv, hinf, haff, hdegDv⟩ := homogeneous_divisor_of_polynomial _ d H hH0 hdeg1106  have hT := initial_form_has_tangent_divisor m.O m.R m.S d f c1107    (by rw [m.hS_t, m.hS_x]; exact hc) H hH Dv hDv1108  obtain ⟨b1, b2, b3, b4⟩ := homogeneous_divisor_boundary_multiplicities _ d H hH0 hdeg Dv hinf1109      haff1110  have e1 : 0 < Dv (infinityDirection _) ↔ c (Fin.last d) ∈ IsLocalRing.maximalIdeal m.R := by1111    rw [b1, ← IsLocalRing.residue_eq_zero_iff]1112    have := hcoeff (Fin.last d); simp only [Fin.val_last] at this; rw [this]1113  have e0 : 0 < Dv (zeroDirection _) ↔ c 0 ∈ IsLocalRing.maximalIdeal m.R := by1114    rw [b2, ← IsLocalRing.residue_eq_zero_iff]1115    have := hcoeff 0; simp only [Fin.val_zero] at this; rw [this]1116  have : Finite (IsLocalRing.ResidueField m.R) := Finite.of_equiv _ m.S.residueEquiv.toEquiv1117  obtain ⟨P, hPd, hPa, hPD⟩ := allowed_pattern_of_cell_ideal m.O m.pi m.hpi m.u m.a m.b m.ha m.S1118    m.hS_t m.hS_x m.s J hJ d f hf c hc Dv e1 e0 (m.shape.valid m.ha)1119    hd hdegDv b4 b31120  refine ⟨⟨⟨P, hPa⟩, ⟨Dv, hPD⟩⟩, ?_⟩1121  change J ∈ fixedTangentCell m.O m.R m.S m.s P.d.val Dv1122  rw [hPd]1123  exact ⟨hJ, hf ▸ hT⟩1124 1125/-! ### Existence of a concrete universe -/1126 1127/-- A concrete universe exists provided the child maps of all cells are measurable and scale the1128measure by `q^{-tri d}` on boxes. -/1129private theorem concrete_universe_of_cell_measure (hmeas : ∀ (m : ConcreteMember) (c : m.cellIndex)1130    (D : CellChildData m c), m.s.terminal = false → ∀1131    (G : ∀ j : m.toMeasured.childIdx c, Set (Ideal (D.mc j).toMeasured.R)),1132    (∀ j, MeasurableSet (G j)) → MeasurableSet (m.toMeasured.cell c ∩ (fun J j => D.Φ J j) ⁻¹'1133    Set.pi Set.univ G)) (hmass : ∀ (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c),1134    m.s.terminal = false → ∀ (G : ∀ j : m.toMeasured.childIdx c, Set1135    (Ideal (D.mc j).toMeasured.R)), (∀ j, MeasurableSet (G j)) → m.toMeasured.μ1136    (m.toMeasured.cell c ∩ (fun J j => D.Φ J j) ⁻¹' Set.pi Set.univ G) = (m.toMeasured.q : ℝ≥0∞)⁻¹1137    ^ tri (m.toMeasured.cellDegree c) * ∏ j, (D.mc j).toMeasured.μ (G j)) :1138    ConcreteUniverse := by1139  let D : ∀ (m : ConcreteMember) (c : m.cellIndex), CellChildData m c :=1140    fun m c => Classical.choice (cell_child_data_exists m c)1141  let U : SurfaceUniverse :=1142    { ι := ConcreteMember1143      M := ConcreteMember.toMeasured1144      stateSet_measurable := concrete_member_stateSet_measurable1145      volume := concrete_member_volume1146      divisors_finite := fun m => (concrete_member_divisor_count m).11147      divisor_count := fun m => (concrete_member_divisor_count m).21148      cell_measurable := fun m _ c => concrete_member_cell_measurable m c1149      cells_cover := fun m _ => concrete_member_cells_cover m1150      cells_disjoint := fun m _ => concrete_member_cells_disjoint m1151      child := fun m c j => (D m c).mc j1152      child_state := fun m c j => ((D m c).child j).hstate1153      child_residue := fun m c j => ((D m c).child j).hcard1154      Φ := fun m c J j => (D m c).Φ J j1155      Φ_bij := fun m _ c => cell_child_bijOn m c (D m c)1156      Φ_measurable := fun m hnt c G hG => hmeas m c (D m c) hnt G hG1157      Φ_measure := fun m hnt c G hG => hmass m c (D m c) hnt G hG1158      type_add := fun m _ c J hJ τ hτ =>1159        cell_child_type_add m c (D m c) J hJ (fun j => ((D m c).mc j).R ⧸ (D m c).Φ J j)1160          (fun j => RingEquiv.refl _) (fun _ _ => rfl) (fun _ _ => rfl) τ hτ1161      terminal_type := fun m a hs J hJ => concrete_member_terminal_type m a hs J hJ }1162  refine ⟨U, Equiv.refl _, fun _ => rfl, ?_, ?_⟩1163  · intro i hnt c J hJ σ hσ j1164    exact (cell_child_termination_data i c hnt (D i c) J hJ1165        (fun j => ((D i c).mc j).R ⧸ (D i c).Φ J j)1166      (fun j => RingEquiv.refl _) (fun _ _ => rfl) (fun _ _ => rfl) σ hσ j).11167  · rintro i hnt c J hJ ⟨σ, hσ⟩ j1168    exact (cell_child_termination_data i c hnt (D i c) J hJ1169        (fun j => ((D i c).mc j).R ⧸ (D i c).Φ J j)1170      (fun j => RingEquiv.refl _) (fun _ _ => rfl) (fun _ _ => rfl) σ hσ j).21171 1172private theorem firstContact_pointChildState (k : Type) [Field k] (s : State) (d : ℕ)1173    (Dv : ExceptionalDivisor k) (Q : ClosedDirection k) :1174    (pointChildState k s d Dv Q).firstContact = Dv Q := by1175  cases s <;> unfold pointChildState <;> split_ifs <;> rfl1176 1177private theorem cellChild_algebraMap_pi (m : ConcreteMember) (c : m.cellIndex)1178    (D : CellChildData m c) : ∀ j,1179    algebraMap m.O (D.mc j).O m.S.pi = (D.mc j).S.pi := by1180  intro j1181  rw [m.hS_pi, (D.mc j).hS_pi, ← (D.child j).hpi]1182 1183private theorem cellChild_degree_sum (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)1184    : ∑ j,1185    m.toMeasured.childDelta c j * (D.mc j).toMeasured.s.degree = m.toMeasured.s.degree := by1186  rw [← member_children_degree_sum m c]1187  refine Finset.sum_congr rfl fun j _ => ?_1188  change _ * (D.child j).mc.s.degree = _1189  rw [(D.child j).hstate]1190 1191private theorem cellChild_pi_pow_eq (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)1192    : ∀ j, ∃1193    (s : ℕ) (cj : (D.mc j).R), algebraMap m.O (D.mc j).R m.S.pi ^ s = (D.mc j).S.t ^1194    m.toMeasured.cellDegree c * cj := by1195  intro j1196  refine ⟨m.toMeasured.cellDegree c, ((D.mc j).S.unit : (D.mc j).R) ^ m.toMeasured.cellDegree c *1197      (D.mc j).S.t ^ (m.toMeasured.cellDegree c * ((D.mc j).S.a - 1)) * (D.mc j).S.x ^1198      (m.toMeasured.cellDegree c * (D.mc j).S.b), ?_⟩1199  rw [IsScalarTower.algebraMap_apply m.O (D.mc j).O (D.mc j).R, cellChild_algebraMap_pi m c D j,1200    (D.mc j).S.vertical]1201  have ha := (D.mc j).S.a_pos1202  obtain ⟨k, hk⟩ : ∃ k, (D.mc j).S.a = k + 1 := ⟨_, (Nat.succ_pred_eq_of_pos ha).symm⟩1203  rw [hk, Nat.add_sub_cancel]1204  ring1205 1206private theorem cellChild_firstContact_sum (m : ConcreteMember) (c : m.cellIndex)1207    (D : CellChildData m c) : ∑ j,1208    m.toMeasured.childDelta c j * (D.mc j).toMeasured.s.firstContact = m.toMeasured.cellDegree c :=1209    by1210  have h1 : ∀ j, m.toMeasured.childDelta c j * (D.mc j).toMeasured.s.firstContact = directionDegree1211      _ (D.asg.pt j) * c.2.1 (D.asg.pt j) := by1212    intro j1213    change _ * (D.child j).mc.s.firstContact = _1214    rw [(D.child j).hstate]1215    have hd := D.asg.deg j1216    have hs := D.asg.state j1217    change ((children m.s c.1.1).get j).1 * ((children m.s c.1.1).get j).2.firstContact = _1218    rw [← hd, hs]1219    rw [firstContact_pointChildState]1220  rw [Finset.sum_congr rfl fun j _ => h1 j]1221  have h2 := c.2.2.11222  change _ = c.1.1.d.val1223  rw [← h2, exceptionalDegree, Finsupp.sum]1224  refine Finset.sum_bij (fun j _ => D.asg.pt j) ?_ ?_ ?_ ?_1225  · intro j _1226    rw [Finsupp.mem_support_iff]1227    exact Nat.pos_iff_ne_zero.mp ((D.asg.supp _).mpr ⟨j, rfl⟩)1228  · intro a _ b _ h; exact D.asg.inj h1229  · intro Q hQ1230    obtain ⟨j, hj⟩ := (D.asg.supp Q).mp (Nat.pos_of_ne_zero (Finsupp.mem_support_iff.mp hQ))1231    exact ⟨j, Finset.mem_univ _, hj⟩1232  · intro j _; rfl1233 1234private theorem divisorFromSurface_t_x_dvd (R : Type) [CommRing R] (t x : R) [IsLocalRing R]1235  (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))1236  (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) (hinf : (infinityPoint R t x).IsPrime)1237      (Q : divisorSupport Dv) :1238    ∃ a1 a2, divisorFromSurface R t x e Dv hinf Q t = divisorException R t x e Dv hinf Q * a1 ∧1239      divisorFromSurface R t x e Dv hinf Q x = divisorException R t x e Dv hinf Q * a2 := by1240  rcases Q with ⟨_ | φ, hQ⟩1241  · refine ⟨@completedPointMap (BlowupChart R x t) _ (infinityPoint R t x) hinf (chartSlope R x t),1242      (1 : @CompletedLocalAt (BlowupChart R x t) _ (infinityPoint R t x) hinf), ?_, ?_⟩1243    · change (@completedPointMap (BlowupChart R x t) _ (infinityPoint R t x) hinf)1244        (chartBase R x t t) = _1245      rw [chartBase_x_eq, map_mul]; rfl1246    · change (@completedPointMap (BlowupChart R x t) _ (infinityPoint R t x) hinf)1247        (chartBase R x t x) = (@completedPointMap (BlowupChart R x t) _ (infinityPoint R t x) hinf)1248        (chartBase R x t x) * 11249      exact (mul_one _).symm1250  · refine ⟨(1 : CompletedLocalAt (BlowupChart R t x) (directionPoint R t x e φ)),1251      completedPointMap (BlowupChart R t x) (directionPoint R t x e φ) (chartSlope R t x), ?_, ?_⟩1252    · change (completedPointMap (BlowupChart R t x) (directionPoint R t x e φ)) (chartBase R t x t)1253        =1254        (completedPointMap (BlowupChart R t x) (directionPoint R t x e φ)) (chartBase R t x t) * 11255      exact (mul_one _).symm1256    · change (completedPointMap (BlowupChart R t x) (directionPoint R t x e φ)) (chartBase R t x x)1257        =1258        _1259      rw [chartBase_x_eq, map_mul]; rfl1260 1261private theorem cellChild_strict_generator (m : ConcreteMember) (c : m.cellIndex)1262    (D : CellChildData m c) : ∀ f :1263    m.R, Ideal.span {f} ∈ m.toMeasured.cell c → ∃ g : (∀ j, (D.mc j).R), ∀ j, D.alpha j f =1264    (D.mc j).S.t ^ m.toMeasured.cellDegree c * g j := by1265  intro f hf1266  obtain ⟨f', co, H, hspan, hf', -⟩ := fixed_tangent_cell_generator_coefficients m.O m.R m.S m.s1267      (m.toMeasured.cellDegree c) c.2.1 _ hf1268  obtain ⟨r, hr⟩ : ∃ r, f = r * f' := by1269    have : f ∈ Ideal.span {f'} := hspan ▸ Ideal.subset_span rfl1270    obtain ⟨r, hr⟩ := Ideal.mem_span_singleton'.mp this1271    exact ⟨r, hr.symm⟩1272  have hab : ∀ j, ∃ a1 a2, D.alpha j m.S.t = (D.mc j).S.t * a1 ∧ D.alpha j m.S.x = (D.mc j).S.t *1273      a2 := by1274    intro j1275    obtain ⟨a1, a2, h1, h2⟩ := divisorFromSurface_t_x_dvd m.R m.S.t m.S.x D.e c.2.1 D.hinf1276        (D.point j)1277    refine ⟨D.Eq j a1, D.Eq j a2, ?_, ?_⟩1278    · change D.Eq j _ = _1279      rw [h1, map_mul]; exact congrArg (· * _) (D.hEq_e j)1280    · change D.Eq j _ = _1281      rw [h2, map_mul]; exact congrArg (· * _) (D.hEq_e j)1282  choose a1 a2 h1 h2 using hab1283  refine ⟨fun j => D.alpha j r * ∑ i : Fin (m.toMeasured.cellDegree c + 1), D.alpha j (co i) * a1 j1284      ^ (m.toMeasured.cellDegree c - i.val) * a2 j ^ i.val, fun j => ?_⟩1285  simp only1286  rw [hr, hf', map_mul, map_sum, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]1287  refine Finset.sum_congr rfl fun i _ => ?_1288  rw [map_mul, map_mul, map_pow, map_pow, h1, h2, mul_pow, mul_pow]1289  rw [← pow_mul_pow_sub ((D.mc j).S.t) (show i.val ≤ m.toMeasured.cellDegree c by omega)]1290  ring1291 1292private theorem member_t_ne_zero (m : ConcreteMember) : m.S.t ≠ 0 := by1293  intro h1294  have hv := m.S.vertical1295  rw [h, zero_pow m.S.a_pos.ne', mul_zero, zero_mul, ← map_zero (algebraMap m.O m.R)] at hv1296  exact m.S.pi_irreducible.ne_zero (m.S.base_injective hv)1297 1298private theorem cellChild_index_map (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)1299    : ∀ f :1300    m.R, Ideal.span {f} ∈ m.toMeasured.cell c → ∀ g : (∀ j, (D.mc j).R),1301    (∀ j, D.alpha j f = (D.mc j).S.t ^ m.toMeasured.cellDegree c * g j) → ∀ iota :1302    (m.R ⧸ Ideal.span {f}) →ₗ[m.O] ((∀ j, (D.mc j).R) ⧸ Ideal.span {g}),1303    (∀ h : m.R, iota (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk (Ideal.span {g})1304    (fun j => D.alpha j h)) → Function.Injective iota ∧ Module.length m.O1305    (((∀ j, (D.mc j).R) ⧸ Ideal.span {g}) ⧸ LinearMap.range iota) =1306    (chooseTwo (m.toMeasured.cellDegree c) : ℕ∞) := by1307  intro f hf g hg iota hiota1308  have hΦ : ∀ j, D.Φ (Ideal.span {f}) j = Ideal.span {g j} := fun j =>1309    strict_transform_ideal_of_generator m.O m.R (D.mc j).R (D.alpha j) ((D.mc j).S.t) (g j) _ f1310        (hg j)1311      (fun a b hab => mul_left_cancel₀ (member_t_ne_zero (D.mc j)) hab)1312  obtain ⟨ψ, hψinj, hlen, hψ⟩ := cell_member_index_map m c D (Ideal.span {f}) hf1313      (fun j => (D.mc j).R ⧸ Ideal.span {g j})1314    (fun j => Ideal.quotEquivOfEq (hΦ j).symm) (fun j r => rfl)1315  obtain ⟨⟨Ψ, hΨ⟩, -⟩ := pi_quotient_span_linearEquiv m.O (m.toMeasured.childIdx c)1316      (fun j => (D.mc j).R) g g1317  have hψ' : ∀ h : m.R, ψ (Ideal.Quotient.mk _ h) = fun j => Ideal.Quotient.mk (Ideal.span {g j})1318      (D.alpha j h) := by1319    intro h; funext j1320    apply (Ideal.quotEquivOfEq (hΦ j).symm).injective1321    rw [hψ h j]; rfl1322  have hcomp : ∀ x, iota x = Ψ.symm (ψ x) := by1323    intro x1324    obtain ⟨h, rfl⟩ := Ideal.Quotient.mk_surjective x1325    rw [hiota, hψ', ← hΨ, LinearEquiv.symm_apply_apply]1326  have hrange : (LinearMap.range ψ.toLinearMap).map (Ψ.symm : _ →ₗ[m.O] _) = LinearMap.range1327      iota := by1328    have hEq : (Ψ.symm : _ →ₗ[m.O] _) ∘ₗ ψ.toLinearMap = iota := LinearMap.ext fun x =>1329        (hcomp x).symm1330    rw [← LinearMap.range_comp, hEq]1331  refine ⟨?_, ?_⟩1332  · intro a b hab1333    rw [hcomp, hcomp] at hab1334    exact hψinj (Ψ.symm.injective hab)1335  · rw [← hlen]1336    exact (LinearEquiv.length_eq (Submodule.Quotient.equiv _ _ Ψ.symm hrange)).symm1337 1338 1339/-- **A concrete universe exists**: choosing child data for every cell of every concrete member1340yields a surface universe indexed by concrete members that satisfies the termination1341hypotheses. -/1342theorem concrete_universe_exists : ConcreteUniverse :=Theorem 6.21343  concrete_universe_of_cell_measure1344    (fun m c D _ ↦ @member_cell_box_measurable m c D.mc (fun j ↦ (D.child j).algO)1345      (fun j ↦ inferInstanceAs (Algebra m.O (D.mc j).R))1346      (fun j ↦ inferInstanceAs (IsScalarTower m.O (D.mc j).O (D.mc j).R)) (fun j ↦ (D.child j).pc)1347      (fun j ↦ (D.child j).pc_cont.2.2.1) (fun j ↦ (D.child j).pc_cont.2.2.2)1348      (fun j ↦ (D.child j).hcard) (cellChild_algebraMap_pi m c D) (cellChild_degree_sum m c D)1349      D.alpha (fun j ↦ (D.mc j).S.t) (fun _ ↦ rfl) (cellChild_pi_pow_eq m c D)1350      (cell_child_bijOn m c D) (cellChild_strict_generator m c D) (cellChild_index_map m c D)1351      (cellChild_firstContact_sum m c D))1352    (fun m c D _ ↦ @member_cell_box_measure m c D.mc (fun j ↦ (D.child j).algO)1353      (fun j ↦ inferInstanceAs (Algebra m.O (D.mc j).R))1354      (fun j ↦ inferInstanceAs (IsScalarTower m.O (D.mc j).O (D.mc j).R)) (fun j ↦ (D.child j).pc)1355      (fun j ↦ (D.child j).pc_cont.2.2.1) (fun j ↦ (D.child j).pc_cont.2.2.2)1356      (fun j ↦ (D.child j).hcard) (cellChild_algebraMap_pi m c D) (cellChild_degree_sum m c D)1357      D.alpha (fun j ↦ (D.mc j).S.t) (fun _ ↦ rfl) (cellChild_pi_pow_eq m c D)1358      (cell_child_bijOn m c D) (cellChild_strict_generator m c D) (cellChild_index_map m c D)1359      (cellChild_firstContact_sum m c D))1360 1361/-- **The root cell law** holds unconditionally. -/1362theorem root_cell_law : RootCellLaw :=(1.3)Theorem 1.1Cluster model and cluster law B_n(7.1)1363  root_cell_law_of_universe concrete_universe_exists1364 1365end SurfaceBlowup