Regression guard for 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.Cluster.Main7import Tests.Regression8 9/-!10# Regression guard for the cluster density11 12The quadratic cluster law: over every complete DVR with finite residue field of cardinality `q`,13a random monic quadratic reducing to `X²` is ramified (type `(2,1)`) with probability14`q / (q + 1)`, split or inert each with probability `1 / (2(q + 1))`. Derived from15`SurfaceBlowup.main_dvr_cluster` and the law of `S(1;2)` (`SurfaceBlowup.Tests.single_two_law`).16-/17 18namespace SurfaceBlowup.Tests19 20open IsLocalRing21 22variable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]23  [IsAdicComplete (maximalIdeal O) O] [Finite (ResidueField O)] [TopologicalSpace O]24  [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]25  [MeasurableSpace O] [BorelSpace O]26 27/-- The value at `q = |k|` of the quadratic cluster law. -/28private theorem clusterDensity_two (htop : IsAdic (maximalIdeal O)) (σ : FactorType) :29    clusterDensity O 2 σ = ENNReal.ofReal (30      (if σ = {(2,1)} then (Nat.card (ResidueField O) : ℚ) / (Nat.card (ResidueField O) + 1)31        else 0) +32      (if σ = {(1,1),(1,1)} then 1 / (2 * ((Nat.card (ResidueField O) : ℚ) + 1)) else 0) +33      (if σ = {(1,2)} then 1 / (2 * ((Nat.card (ResidueField O) : ℚ) + 1)) else 0) : ℚ) := by34  have hq : 1 < (Nat.card (ResidueField O) : ℚ) := by exact_mod_cast Finite.one_lt_card35  rw [main_dvr_cluster O htop, clusterExpr, rootLaw, if_neg two_ne_zero, densityValue,36    single_two_law 1 one_pos _ hq]37 38/-- Quadratic cluster, ramified: probability `q / (q + 1)`. -/39theorem clusterDensity_two_ramified (htop : IsAdic (maximalIdeal O)) :(1.3)40    clusterDensity O 2 {(2,1)} =41      ENNReal.ofReal (Nat.card (ResidueField O) / (Nat.card (ResidueField O) + 1)) := by42  rw [clusterDensity_two O htop]43  simp +decide44 45/-- Quadratic cluster, split: probability `1 / (2(q + 1))`. -/46theorem clusterDensity_two_split (htop : IsAdic (maximalIdeal O)) :(1.3)47    clusterDensity O 2 {(1,1),(1,1)} =48      ENNReal.ofReal (1 / (2 * (Nat.card (ResidueField O) + 1))) := by49  rw [clusterDensity_two O htop]50  simp +decide51 52/-- Quadratic cluster, inert: probability `1 / (2(q + 1))`. -/53theorem clusterDensity_two_inert (htop : IsAdic (maximalIdeal O)) :(1.3)54    clusterDensity O 2 {(1,2)} =55      ENNReal.ofReal (1 / (2 * (Nat.card (ResidueField O) + 1))) := by56  rw [clusterDensity_two O htop]57  simp +decide58 59end SurfaceBlowup.Tests