The cluster density

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.Basic7 8/-!9# The cluster density10 11Definitions for the cluster clause of Theorem 1.1: the cluster cell `(πO)^n` (coefficient vectors12whose monic polynomial reduces to `X^n`), the universal cluster expression `B_{n,σ}` (the13coefficient of `σ` in the root law, the law of the state `S(1;n)`), and the cluster probability14`clusterDensity O n σ` (the normalized restriction of the coefficient measure to the cluster cell,15with the reduced-algebra type predicate `HasPolynomialType`).16-/17 18noncomputable section19 20namespace SurfaceBlowup21 22open scoped ENNReal23 24section Classical25 26variable (O : Type) [CommRing O] [IsDomain O] [IsLocalRing O]27 28/-- The cluster cell `(πO)^n`: coefficient vectors whose monic polynomial reduces to `X^n`29(paper display (1.1), measure `μ_cluster`). -/30def clusterCell (n : ℕ) : Set (Fin n → O) := {a | ∀ i, a i ∈ IsLocalRing.maximalIdeal O}31 32end Classical33 34/-- `B_{n,σ}`: the coefficient of `σ` in the root law, the law of the state `S(1;n)`35(paper display (7.1)). -/36noncomputable def clusterExpr (n : ℕ) (σ : FactorType) : Expr := lawCoeff (rootLaw n) σTheorem 1.137 38section Measure39 40variable (O : Type) [CommRing O] [IsDomain O] [IsLocalRing O]41  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]42  [SecondCountableTopology O]43  [MeasurableSpace O] [BorelSpace O]44 45/-- The cluster probability of type `σ` (paper display (1.1)): the normalized restriction of46the coefficient measure to the cluster cell. The event uses `HasPolynomialType` (the47reduced-algebra convention: a factorization into distinct monic irreducible factors, inseparable48factors allowed); the inseparable locus is Haar-null, so the étale convention gives the same49value (`clusterDensity_eq_etale`). -/50noncomputable def clusterDensity (n : ℕ) (σ : FactorType) : ℝ≥0∞ :=Theorem 1.151  coefficientMeasure O n (clusterCell O n ∩ {a | HasPolynomialType O (monicPolynomial O a) σ}) /52    coefficientMeasure O n (clusterCell O n)53 54end Measure55 56end SurfaceBlowup