File size: 3,454 Bytes
9425aed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 | {-# LANGUAGE StrictData #-}
-- =====================================================================
-- SINGULARITY ANALYSIS: Milnor Number & δ-Invariant
-- Author: Ahmad Ali Parr <ahmedparr93@gmail.com>
-- =====================================================================
module LiquidLean.Jacobian.SingularityAnalysis
( SingularityData(..)
, analyseSingularity
, genusFormula
) where
import LiquidLean.Jacobian.Theorem3Kernel
import LiquidLean.Jacobian.MoraLocal
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
-- =====================================================================
-- Singularity Data Type
-- =====================================================================
data SingularityData = SingularityData
{ sdMilnorMu :: !Int
, sdDeltaInv :: !Int
, sdBranches :: !Int
} deriving (Show, Eq)
-- =====================================================================
-- Singularity Analysis
-- =====================================================================
-- | Translate polynomial to origin
translate :: Polynomial -> (Rational, Rational) -> Polynomial
translate (Poly f) (u0, x0) = Poly $ Map.fromListWith (+)
[ ((u'-a, x'-b), coeff a b u0 x0 u' x')
| ((a,b), c) <- Map.toList f
, u' <- [0..a], x' <- [0..b]
, let coeff a b u0 x0 u' x' =
fromIntegral (choose a (a-u') * choose b (b-x'))
* (u0 ^ (a - u')) * (x0 ^ (b - x')) * c
]
where
choose n k = if k < 0 || k > n then 0 else product [n-k+1..n] `div` product [1..k]
-- | Lowestdegree part (initial form)
lowestDegreePart :: Polynomial -> (Polynomial, Int)
lowestDegreePart (Poly f) =
if Map.null f
then (zeroPoly, -1)
else let minDeg = minimum [u+x | (u,x) <- Map.keys f]
initTerms = [ (u,x,c) | ((u,x),c) <- Map.toList f, u+x == minDeg ]
in (fromTerms initTerms, minDeg)
-- | Count branches (factor count of lowest-degree part)
-- Conservative lower bound: actual factorization deferred to future work
countBranches :: Polynomial -> Int
countBranches h0 =
let (initForm, _) = lowestDegreePart h0
-- TODO: Implement full factorization-based branch count
-- For now, use degree as conservative lower bound on branch count
degree = totalDegree initForm
in max 1 degree
-- =====================================================================
-- Analytic Singularity Function
-- =====================================================================
analyseSingularity :: Polynomial -> (Rational, Rational) -> Thermal SingularityData
analyseSingularity h (u0, x0) = do
emitEnergy phiDecay
-- Translate singularity to origin
let h0 = translate h (u0, x0)
-- Compute partial derivatives
let fu = partialDerivative h0 0
let fv = partialDerivative h0 1
-- Run Mora's algorithm on jacobian ideal
gb <- groebnerBasisLocal [fu, fv]
let mu = countStandardMonomials gb
let r = countBranches h0
-- Milnor-Jung: δ = (μ + r - 1) / 2
let delta = (mu + r - 1) `div` 2
pure SingularityData { sdMilnorMu = mu, sdDeltaInv = delta, sdBranches = r }
-- =====================================================================
-- THEOREM (Plücker Genus Formula)
-- =====================================================================
-- | g = (d-1)(d-2)/2 - Σ δ_P
genusFormula :: Int -> [Int] -> Int
genusFormula d deltas =
let geometric = (d - 1) * (d - 2) `div` 2
singContrib = sum deltas
in geometric - singContrib
|