Statement-level definitions (the trust boundary)

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 Mathlib.FieldTheory.RatFunc.Basic7import Mathlib.MeasureTheory.Measure.Haar.Unique8import Mathlib.NumberTheory.ArithmeticFunction.Moebius9import Mathlib.NumberTheory.Padics.PadicIntegers10import Mathlib.RingTheory.IntegralClosure.IntegralRestrict11import Mathlib.RingTheory.MvPowerSeries.Basic12import Mathlib.RingTheory.RamificationInertia.Basic13import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology14 15/-!16# Statement-level definitions (the trust boundary)17 18Every definition occurring in the statements of the main theorems `SurfaceBlowup.main_dvr`,19`SurfaceBlowup.main_field_form` and `SurfaceBlowup.recip_main` lives in this file, and nothing else20does except the internal route-F densities at the end. These definitions are, constant for constant,21the owner-signed published definitions (Prove2Me nodes N001–N010, namespace `SurfaceBlowupV2`),22renamed into `SurfaceBlowup`; `Checks/run_checks.sh` verifies this at the kernel level against the23certified trees. They must not be edited beyond comments and docstrings.24 25* Factorization types `FactorType` (multisets of pairs `(e, f)`), `typeDegree`, `ValidType`.26* Rational expressions `Expr` in one variable `q`, with evaluation `Expr.eval` and the rational27  function `Expr.rational`.28* Laws (`Law`: finite lists of type-weighted expressions), their algebra and coefficients29  `lawCoeff`.30* The recursion states `State` (`S(a;c)` single-boundary, `T(a,b;c,h)` crossing), tangent patterns,31  children, the weights of §7 and the recursion `stateLaw`, giving `monicExpr n σ` and32  `projectiveExpr n σ`.33* The densities: `monicDensity O n σ` is the normalized Haar measure of the set of monic degree-`n`34  polynomials over `O` whose factorization over `Frac O` has type `σ`; `projectiveDensity O n σ` is35  the conditional measure of type `σ` among primitive binary forms.36* `densityValue x q = x(q)` as an element of `ℝ≥0∞`; `padicIntegers p K`, `PadicUnramified p K`.37 38Provenance: Def nodes Types, Expressions, Law, State, Patterns, Weights, Recursion, Density39(original N008 predicates and the route-F variants), Core, PadicField.40-/41 42noncomputable section43 44namespace SurfaceBlowup45 46open scoped BigOperators ENNReal47open IsLocalRing MeasureTheory48 49/-! ### Factorization types -/50 51/-- A factorization type: a multiset of pairs `(e, f)` (ramification index, residue degree), one per52irreducible factor. -/53abbrev FactorType := Multiset (ℕ × ℕ)Type of degree n54 55/-- The degree `∑ e·f` of a factorization type. -/56def typeDegree (σ : FactorType) : ℕ := (σ.map fun z => z.1 * z.2).sumType of degree n57 58/-- A type is valid if all its pairs have `e, f ≥ 1`. -/59def ValidType (σ : FactorType) : Prop := ∀ z ∈ σ, 0 < z.1 ∧ 0 < z.2Type of degree n60 61/-- Scaling the residue degrees by `δ` (the effect of descending along a degree-`δ` unramified62extension). -/63def scaleType (δ : ℕ) (σ : FactorType) : FactorType := σ.map fun z => (z.1, δ * z.2)(6.4)64 65/-! ### Rational expressions -/66 67/-- Syntactic rational expressions in one variable (the residue cardinality `q`). -/68inductive Expr whereType variables Z_{e,f}69  | const (r : ℚ)70  | var71  | add (x y : Expr)72  | mul (x y : Expr)73  | inv (x : Expr)74  deriving Repr, DecidableEq75 76namespace Expr77 78/-- Negation `-x`. -/79def neg (x : Expr) : Expr := .mul (.const (-1)) x80 81/-- Subtraction `x - y`. -/82def sub (x y : Expr) : Expr := .add x y.neg83 84/-- The power `x ^ n`. -/85def pow (x : Expr) : ℕ → Expr86  | 0 => .const 187  | n+1 => .mul (pow x n) x88 89/-- Evaluation at `q` (with `0⁻¹ = 0`). -/90def eval (q : ℚ) : Expr → ℚ91  | .const r => r92  | .var => q93  | .add x y => eval q x + eval q y94  | .mul x y => eval q x * eval q y95  | .inv x => (eval q x)⁻¹96 97/-- No denominator vanishes when evaluating at `q`. -/98def safe (q : ℚ) : Expr → Prop99  | .const _ => True100  | .var => True101  | .add x y => safe q x ∧ safe q y102  | .mul x y => safe q x ∧ safe q y103  | .inv x => safe q x ∧ eval q x ≠ 0104 105/-- Substitution of `y` for the variable. -/106def subst (x : Expr) (y : Expr) : Expr :=107  match x with108  | .const r => .const r109  | .var => y110  | .add a b => .add (subst a y) (subst b y)111  | .mul a b => .mul (subst a y) (subst b y)112  | .inv a => .inv (subst a y)113 114/-- A (numerator, denominator) pair of polynomials representing the expression. -/115def fraction : Expr → Polynomial ℚ × Polynomial ℚ116  | .const r => (Polynomial.C r, 1)117  | .var => (Polynomial.X, 1)118  | .add x y => let a := fraction x; let b := fraction y119               (a.1*b.2+b.1*a.2, a.2*b.2)120  | .mul x y => let a := fraction x; let b := fraction y121               (a.1*b.1, a.2*b.2)122  | .inv x => let a := fraction x; (a.2,a.1)123 124/-- The rational function `numerator / denominator` of the expression. -/125def rational (x : Expr) : RatFunc ℚ :=126  algebraMap (Polynomial ℚ) (RatFunc ℚ) x.fraction.1 /127    algebraMap (Polynomial ℚ) (RatFunc ℚ) x.fraction.2128 129/-- The sum of a list of expressions. -/130def sum (xs : List Expr) : Expr := xs.foldr .add (.const 0)131 132/-- The product of a list of expressions. -/133def prod (xs : List Expr) : Expr := xs.foldr .mul (.const 1)134 135/-- The expression is safe at every integer `q ≥ 2`. -/136def allSafe (x : Expr) : Prop := ∀ q : ℕ, 2 ≤ q → x.safe q137 138end Expr139 140/-- The rational function `f` has a representation `P / Q` with `Q(q) ≠ 0`. -/141def RegularAt (f : RatFunc ℚ) (q : ℚ) : Prop :=142  ∃ P Q : Polynomial ℚ, Q.eval q ≠ 0 ∧143    f = algebraMap (Polynomial ℚ) (RatFunc ℚ) P /144      algebraMap (Polynomial ℚ) (RatFunc ℚ) Q145 146/-! ### Laws -/147 148/-- A law: a finite formal sum of factorization types with expression coefficients. -/149abbrev Law := List (FactorType × Expr)Type variables Z_{e,f}150 151/-- The unit law (the empty type with coefficient `1`). -/152def lawOne : Law := [(0, .const 1)]153 154/-- The law of a single factor of type `(e, f)`. -/155def lawAtom (e f : ℕ) : Law := [({(e,f)}, .const 1)]156 157/-- Multiplying every coefficient by `x`. -/158def lawScale (x : Expr) (L : Law) : Law := L.map fun z => (z.1,.mul x z.2)159 160/-- The product of laws (types add, coefficients multiply). -/161def lawMul (L M : Law) : Law := L.flatMap fun z => M.map fun w => (z.1+w.1,.mul z.2 w.2)Type variables Z_{e,f}162 163/-- The product of a list of laws. -/164def lawProd (Ls : List Law) : Law := Ls.foldr lawMul lawOne165 166/-- The total coefficient of the type `σ` in a law. -/167def lawCoeff (L : Law) (σ : FactorType) : Expr :=Type variables Z_{e,f}168  Expr.sum (L.map fun z => if z.1=σ then z.2 else .const 0)169 170/-- Descent along a degree-`δ` unramified extension: scale types by `δ` and substitute `q ↦ q^δ`. -/171def lawDescend (δ : ℕ) (L : Law) : Law :=(6.4)172  L.map fun z => (scaleType δ z.1, z.2.subst (.pow .var δ))173 174/-- All coefficients of the law are safe at every `q ≥ 2`. -/175def LawSafe (L : Law) : Prop := ∀ z ∈ L, z.2.allSafe176 177/-! ### Recursion states and tangent patterns -/178 179/-- Recursion states: `single a c` is `S(a;c)` (one boundary component of multiplicity `a`, contact180`c`), `crossing a b c h` is `T(a,b;c,h)` (two crossing boundary components). -/181inductive State where(2.1)182  | single (a c : ℕ)183  | crossing (a b c h : ℕ)184  deriving DecidableEq, Repr185 186namespace State187 188/-- All parameters are positive. -/189def Valid : State → Prop(2.1)190  | .single a c => 0 < a ∧ 0 < c191  | .crossing a b c h => 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < h192 193/-- The degree `a·c` (resp. `a·c + b·h`). -/194def degree : State → ℕ(2.1)195  | .single a c => a*c196  | .crossing a b c h => a*c+b*h197 198/-- The weight `a` (resp. `a + b`). -/199def weight : State → ℕ200  | .single a _ => a201  | .crossing a b _ _ => a+b202 203/-- `0` for single-boundary states, `1` for crossing states. -/204def tag : State → ℕ205  | .single _ _ => 0206  | .crossing _ _ _ _ => 1207 208/-- The well-founded rank `2d² + 2(d - w) + tag` driving the recursion. -/209def rank (s : State) : ℕ := 2*s.degree*s.degree + 2*(s.degree-s.weight) + s.tagContact-size order210 211/-- Terminal states `S(a;1)`. -/212def terminal : State → Bool213  | .single _ 1 => true214  | _ => false215 216end State217 218/-- A residue-divisor pattern: multiplicities `m (i, j)` of closed points of degree `i + 1` with219contact `j + 1`. -/220abbrev Pattern (n : ℕ) := (Fin n × Fin n) → Fin (n+1)221 222/-- The weight `∑ (i + 1)(j + 1) m(i, j)` of a pattern. -/223def patternWeight {n : ℕ} (m : Pattern n) : ℕ :=224  ∑ ij : Fin n × Fin n, (ij.1.val+1)*(ij.2.val+1)*(m ij).val225 226/-- A tangent pattern of a state of degree `n`: the tangent degree `d`, the boundary contacts227`rt`, `rx`, and the pattern of the other points. -/228structure TangentPattern (n : ℕ) whereAllowed residue ideals, cells, occupied points229  d : Fin (n+1)230  rt : Fin (n+1)231  rx : Fin (n+1)232  other : Pattern n233  deriving DecidableEq, Fintype234 235/-- The admissible tangent patterns of a state (Proposition 5.1). -/236def Allowed (s : State) (P : TangentPattern s.degree) : Prop :=Allowed residue ideals, cells, occupied points(4.7)–(4.8)237  0<P.d.val ∧ P.rt.val+P.rx.val+patternWeight P.other=P.d.val ∧238  match s with239  | .single _ c => P.d.val≤c ∧ P.rx.val=0 ∧ (0<P.rt.val ↔ P.d.val<c)240  | .crossing _ _ c h => P.d.val≤c ∧ P.d.val≤h ∧241      (0<P.rt.val ↔ P.d.val<c) ∧ (0<P.rx.val ↔ P.d.val<h)242 243/-- The children `(δ, S(a; j + 1))` contributed by the non-boundary points of a pattern. -/244def otherChildren {n : ℕ} (a : ℕ) (m : Pattern n) : List (ℕ × State) :=(4.7)–(4.8)245  (Finset.univ : Finset (Fin n × Fin n)).toList.flatMap fun ij =>246    List.replicate (m ij).val (ij.1.val+1, .single a (ij.2.val+1))247 248/-- All children (residue degree, child state) of a state under a tangent pattern. -/249def children (s : State) (P : TangentPattern s.degree) : List (ℕ × State) :=(4.7)–(4.8)250  match s with251  | .single a c =>252    (if P.rt.val=0 then [] else [(1,.crossing a a P.rt.val (c-P.d.val))]) ++253      otherChildren a P.other254  | .crossing a b c h =>255    (if P.rt.val=0 then [] else [(1,.crossing (a+b) a P.rt.val (c-P.d.val))]) ++256    (if P.rx.val=0 then [] else [(1,.crossing (a+b) b P.rx.val (h-P.d.val))]) ++257      otherChildren (a+b) P.other258 259/-- Self patterns return to the same single-boundary state. -/260def SelfPattern (s : State) (P : TangentPattern s.degree) : Prop :=261  ∃ a c, s = .single a c ∧ children s P = [(1,s)]262 263open scoped Classical in264/-- The finite set of allowed tangent patterns. -/265noncomputable def allowedPatterns (s : State) : Finset (TangentPattern s.degree) :=266  (Finset.univ).filter (Allowed s)267 268/-! ### Weights (§7) -/269 270/-- `d(d+1)/2`. -/271def tri (d : ℕ) : ℕ := d*(d+1)/2272 273/-- `d(d-1)/2`. -/274def chooseTwo (d : ℕ) : ℕ := d*(d-1)/2275 276/-- The expression `q - 1`. -/277def eminusOne : Expr := .sub .var (.const 1)278 279/-- The volume `q^{-c}` (resp. `(q - 1) q^{-(c+h)}`) of a state. -/280def stateVolume : State → ExprProposition 3.3281  | .single _ c => .inv (.pow .var c)282  | .crossing _ _ c h => .mul eminusOne (.inv (.pow .var (c+h)))283 284/-- The self-return weight `q · q^{-tri c}` of `S(a;c)`. -/285def returnWeight (c : ℕ) : Expr := .mul .var (.inv (.pow .var (tri c)))(6.6)286 287/-- The probability of the tangent divisor degree `d` (equation (7.2)). -/288def divisorProbability (s : State) (d : ℕ) : Expr :=Proposition 6.1289  match s with290  | .single _ c => .mul (.inv (.pow .var (tri d))) (.pow eminusOne (if d<c then 1 else 0))291  | .crossing _ _ c h =>292    let j := (if d<c then 1 else 0) + (if d<h then 1 else 0)293    .mul (.inv (.pow .var (chooseTwo d)))294      (if j=0 then .inv eminusOne else .pow eminusOne (j-1))295 296/-- The number `(1/δ) ∑_{j ∣ δ} μ(j) q^{δ/j}` of closed points of degree `δ` of `ℙ¹` minus `∞`297(necklace polynomial). -/298def pointCount (δ : ℕ) : Expr :=(6.2)299  .mul (.const (1/(δ:ℚ))) (Expr.sum ((Nat.divisors δ).toList.map fun j =>300    .mul (.const ((ArithmeticFunction.moebius j : ℤ) : ℚ)) (.pow .var (δ/j))))301 302/-- Available points of degree `δ` (degree one: `q + offset`). -/303def availablePoints (offset : ℤ) (δ : ℕ) : Expr :=(6.3)304  if δ=1 then .add .var (.const offset) else pointCount δ305 306/-- The falling factorial `x (x - 1) ⋯ (x - m + 1)`. -/307def falling (x : Expr) (m : ℕ) : Expr :=(6.3)308  Expr.prod ((List.range m).map fun j => .sub x (.const j))309 310/-- The number of residue divisors with pattern `m` (choices of distinct points per degree). -/311def divisorCount {n : ℕ} (offset : ℤ) (m : Pattern n) : Expr :=(6.3)312  Expr.prod ((Finset.univ : Finset (Fin n)).toList.map fun i =>313    .mul (falling (availablePoints offset (i.val+1)) (∑ j : Fin n, (m (i,j)).val))314      (.const (1 / (∏ j : Fin n, ((Nat.factorial (m (i,j)).val : ℕ) : ℚ)))))315 316/-- The number of tangent divisors with the pattern of `P`. -/317def tangentCount (s : State) (P : TangentPattern s.degree) : Expr :=(6.3)318  divisorCount (match s with | .single _ _ => 0 | .crossing _ _ _ _ => -1) P.other319 320/-- `1 + q + ⋯ + q^n`. -/321def projectiveNormalizer (n : ℕ) : Expr :=Lemma 7.1322  Expr.sum ((List.range (n+1)).map fun i => .pow .var i)323 324/-! ### The recursion and the universal expressions -/325 326open scoped Classical in327/-- The measured recursion of §8 with explicit fuel. -/328noncomputable def stateLawFuel : ℕ → State → Law(6.7)329  | 0, _ => []330  | k+1, s =>331    match s with332    | .single a 1 => lawAtom a 1333    | _ =>334      let terms := (allowedPatterns s).toList.flatMap fun P =>335        if SelfPattern s P then [] else336          lawScale (.mul (tangentCount s P) (divisorProbability s P.d.val))337            (lawProd ((children s P).map fun z => lawDescend z.1 (stateLawFuel k z.2)))338      match s with339      | .single _ c => lawScale (.inv (.sub (.const 1) (returnWeight c))) terms340      | .crossing _ _ _ _ => terms341 342/-- The law of a state (fuel `rank + 1` suffices). -/343noncomputable def stateLaw (s : State) : Law := stateLawFuel (s.rank+1) sTheorem 6.2344 345/-- The law of the root cell `S(1;r)` (`lawOne` for `r = 0`). -/346noncomputable def rootLaw (r : ℕ) : Law := if r=0 then lawOne else stateLaw (.single 1 r)(1.5)Cluster model and cluster law B_n347 348/-- Residue patterns of total weight `n`. -/349noncomputable def residuePatterns (n : ℕ) : Finset (Pattern n) :=(7.3)350  Finset.univ.filter fun m => patternWeight m=n351 352/-- The global law: average over residue divisors of the products of descended child laws. -/353noncomputable def globalLaw (projective : Bool) (n : ℕ) : Law :=(1.5)(7.3)354  lawScale (.inv (if projective then projectiveNormalizer n else .pow .var n))355    ((residuePatterns n).toList.flatMap fun m =>356      lawScale (divisorCount (if projective then 1 else 0) m)357        (lawProd ((otherChildren 1 m).map fun z =>358          lawDescend z.1 (stateLaw z.2))))359 360/-- The universal monic density expression `A_n,σ(q)`. -/361noncomputable def monicExpr (n : ℕ) (σ : FactorType) : Expr := lawCoeff (globalLaw false n) σTheorem 1.1(1.5)362 363/-- The universal projective density expression `B_n,σ(q)`. -/364noncomputable def projectiveExpr (n : ℕ) (σ : FactorType) : Expr := lawCoeff (globalLaw true n) σTheorem 1.1(1.5)365 366/-! ### Densities -/367 368section Classical369 370variable (O : Type) [CommRing O] [IsDomain O]371 372/-- The fraction field of `O`. -/373abbrev BaseField := FractionRing O374 375/-- The invariant `(e, f)` of an irreducible `g`: ramification index and inertia degree of the376maximal ideal of the integral closure of `O` in `Frac(O)[X]/(g)` when that closure is local (junk377value `(0, 0)` otherwise). -/378noncomputable def factorInvariant (g : Polynomial (BaseField O)) : ℕ × ℕ := byMonic model379  classical380  let B := integralClosure O (AdjoinRoot g)381  exact if h : IsLocalRing B then382    letI : IsLocalRing B := h383    ((maximalIdeal B).ramificationIdx O, (maximalIdeal B).inertiaDeg O)384  else (0,0)385 386/-- `F` is the product of distinct monic irreducibles whose invariants form the type `σ`. -/387def HasPolynomialType (F : Polynomial (BaseField O)) (σ : FactorType) : Prop :=Monic model388  ∃ gs : List (Polynomial (BaseField O)),389    (∀ g ∈ gs, g.Monic ∧ Irreducible g) ∧ gs.Pairwise (fun g h => g ≠ h) ∧390    F=gs.prod ∧ σ=(gs.map (factorInvariant O) : Multiset (ℕ × ℕ))391 392/-- The monic polynomial `X^n + ∑ aᵢ Xⁱ`. -/393def monicPolynomial {n : ℕ} (a : Fin n → O) : Polynomial (BaseField O) :=Monic model394  Polynomial.X^n + ∑ i : Fin n,395    Polynomial.C (algebraMap O (BaseField O) (a i)) * Polynomial.X^i.val396 397/-- The polynomial `∑ aᵢ Xⁱ` (the dehomogenized binary form). -/398def affinePolynomial {n : ℕ} (a : Fin (n + 1) → O) : Polynomial (BaseField O) :=Projective model399  ∑ i : Fin (n+1), Polynomial.C (algebraMap O (BaseField O) (a i)) * Polynomial.X^i.val400 401/-- Some coefficient is a unit. -/402def primitive {n : ℕ} (a : Fin (n + 1) → O) : Prop := ∃ i, IsUnit (a i)Projective model403 404/-- The binary form with coefficients `a` has type `σ` (a missing top degree contributes the point405at infinity, of type `(1, 1)`). -/406def HasBinaryType {n : ℕ} (a : Fin (n + 1) → O) (σ : FactorType) : Prop :=Projective model407  let F := affinePolynomial O a408  F≠0 ∧ F.natDegree≤n ∧ n-F.natDegree≤1 ∧409    ∃ τ, HasPolynomialType O (Polynomial.C F.leadingCoeff⁻¹ * F) τ ∧410      σ=τ+Multiset.replicate (n-F.natDegree) (1,1)411 412end Classical413 414section Measure415 416variable (O : Type) [CommRing O] [IsDomain O]417  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]418  [SecondCountableTopology O]419  [MeasurableSpace O] [BorelSpace O]420 421/-- The normalized Haar (probability) measure on `Oⁿ`. -/422noncomputable def coefficientMeasure (n : ℕ) : Measure (Fin n → O) :=Monic model423  (Measure.addHaar (G := Fin n → O) Set.univ)⁻¹ • Measure.addHaar (G := Fin n → O)424 425/-- The probability that a random monic polynomial of degree `n` over `O` has type `σ`. -/426noncomputable def monicDensity (n : ℕ) (σ : FactorType) : ℝ≥0∞ :=Monic model427  coefficientMeasure O n {a | HasPolynomialType O (monicPolynomial O a) σ}428 429/-- The probability that a random primitive binary form of degree `n` over `O` has type `σ`. -/430noncomputable def projectiveDensity (n : ℕ) (σ : FactorType) : ℝ≥0∞ :=Projective model431  coefficientMeasure O (n+1) {a | primitive O a ∧ HasBinaryType O a σ} /432    coefficientMeasure O (n+1) {a | primitive O a}433 434end Measure435 436/-- The value `x(q)` of an expression, as an extended nonnegative real. -/437abbrev densityValue (x : Expr) (q : ℕ) : ℝ≥0∞ := ENNReal.ofReal ((x.eval q : ℚ) : ℝ)438 439/-- `q` is a prime power `p^r`, `r ≥ 1`. -/440def PrimePower (q : ℕ) : Prop := ∃ p r : ℕ, p.Prime ∧ 0<r ∧ q=p^r441 442/-- Both universal expressions are regular at every prime power. -/443def FormulaRegular (n : ℕ) (σ : FactorType) : Prop :=444  ∀ q : ℕ, PrimePower q →445    RegularAt (monicExpr n σ).rational q ∧ RegularAt (projectiveExpr n σ).rational q446 447/-! ### Rings of integers of finite extensions of `ℚ_p` -/448 449section PadicIntegers450 451variable (p : ℕ) [Fact p.Prime] (K : Type) [Field K] [Algebra ℤ_[p] K]452 453/-- The ring of integers of `K`: the integral closure of `ℤ_[p]` in `K`, as a type. -/454abbrev padicIntegers : Type := ↥(integralClosure ℤ_[p] K)455 456/-- `K/ℚ_p` is unramified (for the ring of integers `padicIntegers p K`) iff `p` stays457irreducible. -/458def PadicUnramified : Prop := Irreducible (p : padicIntegers p K)459 460end PadicIntegers461 462/-! ### Internal: route-F type predicates463 464The proofs work with the variants below, whose type predicates additionally record that the integral465closure of `O` in every root field is a finite `O`-module (automatic for separable factors). They466agree with the original densities because the inseparable locus is Haar-null467(`orig_monicDensity_eq`, `orig_projectiveDensity_eq`). -/468 469section RouteF470 471variable (O : Type) [CommRing O] [IsDomain O]472 473/-- `HasPolynomialType` together with finiteness of the integral closure in each root field. -/474def HasPolynomialTypeF (F : Polynomial (BaseField O)) (σ : FactorType) : Prop :=Remark 1.3Reduced-algebra type conventionRemark 6.3475  ∃ gs : List (Polynomial (BaseField O)),476    (∀ g ∈ gs, g.Monic ∧ Irreducible g) ∧ gs.Pairwise (fun g h => g ≠ h) ∧477    F=gs.prod ∧ σ=(gs.map (factorInvariant O) : Multiset (ℕ × ℕ)) ∧478    ∀ g ∈ gs, Module.Finite O (integralClosure O (AdjoinRoot g))479 480/-- `HasBinaryType` with `HasPolynomialTypeF` in place of `HasPolynomialType`. -/481def HasBinaryTypeF {n : ℕ} (a : Fin (n + 1) → O) (σ : FactorType) : Prop :=482  let F := affinePolynomial O a483  F≠0 ∧ F.natDegree≤n ∧ n-F.natDegree≤1 ∧484    ∃ τ, HasPolynomialTypeF O (Polynomial.C F.leadingCoeff⁻¹ * F) τ ∧485      σ=τ+Multiset.replicate (n-F.natDegree) (1,1)486 487variable [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]488  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]489 490/-- The monic density for the route-F predicate. -/491noncomputable def monicDensityF (n : ℕ) (σ : FactorType) : ℝ≥0∞ :=492  coefficientMeasure O n {a | HasPolynomialTypeF O (monicPolynomial O a) σ}493 494/-- The projective density for the route-F predicate. -/495noncomputable def projectiveDensityF (n : ℕ) (σ : FactorType) : ℝ≥0∞ :=496  coefficientMeasure O (n+1) {a | primitive O a ∧ HasBinaryTypeF O a σ} /497    coefficientMeasure O (n+1) {a | primitive O a}498 499end RouteF500 501end SurfaceBlowup502 503end