A machine-checked solution to the Jacobians challenge

A machine-checked solution to the Jacobians challenge

Table of Contents

1.	How to validate this solution
2.	Conformance: Buzzard’s spec vs. this formalization
3.	holomorphic forms
4.	local multiplicity
5.	surfaces and charts
6.	mapping degree
7.	paths and integrals
8.	residue calculus
9.	jacobian construction
10.	projective line
11.	meromorphic and divisors
12.	meromorphic trace
13.	sphere topology
14.	cech cohomology
15.	form trace tower
16.	dbar solvability
17.	dolbeault comparison
18.	planar stokes atoms
19.	finiteness and chi
20.	canonical forms
21.	laurent tails
22.	monodromy
23.	residue theorem
24.	serre duality cech
25.	abel weak solutions
26.	proper map degree
27.	serre duality tails
28.	cech h1 genus
29.	riemann roch
30.	abel theorem
31.	genus zero headline
32.	period lattice rank

6. mapping degree

6.1.	Keystones
6.2.	Builds on
6.3.	MappingDegree
6.4.	MappingDegree.AnalyticContinuationGlobalization
6.5.	MappingDegree.AnalyticFiberDiscrete
6.6.	MappingDegree.AnalyticKthRoot
6.7.	MappingDegree.ChartBallOffCentreWitnessDischarge
6.8.	MappingDegree.ChartLocalDetour
6.9.	MappingDegree.ChartOverlapAvoidanceFull
6.10.	MappingDegree.ChartOverlapPropagationDischarge
6.11.	MappingDegree.ChartPullbackDataConstruction
6.12.	MappingDegree.ChartPullbackNotEventuallyConstDischarge
6.13.	MappingDegree.ChartRestrictionToBall
6.14.	MappingDegree.ChartedSpaceLocPathConnected
6.15.	MappingDegree.ClopennessOfLocallyConstDischarge
6.16.	MappingDegree.ConnectedManifoldPathConnected
6.17.	MappingDegree.ConnectivityGlobalizationReduction
6.18.	MappingDegree.CriticalSetDerivBridge
6.19.	MappingDegree.CriticalSetDiscrete
6.20.	MappingDegree.CriticalValueSetFinite
6.21.	MappingDegree.CriticalValuesFiniteGeneral
6.22.	MappingDegree.Degree
6.23.	MappingDegree.DegreeWellDefined
6.24.	MappingDegree.FibreCardLocallyConstantFromNormalForm
6.25.	MappingDegree.FibreCardOnRegularSubset
6.26.	MappingDegree.FibreCardWellDefinedAtRegular
6.27.	MappingDegree.FibresFiniteAssembly
6.28.	MappingDegree.FibresFiniteUnconditional
6.29.	MappingDegree.HLcUnconditional
6.30.	MappingDegree.HPkgUnconditional
6.31.	MappingDegree.HurwitzPatchingDataConstruction
6.32.	MappingDegree.HurwitzWellDefinedFromHPath
6.33.	MappingDegree.HurwitzWellDefinedUnconditionalTopo
6.34.	MappingDegree.IsPathConnectedBallMinusCountable
6.35.	MappingDegree.LocalKFoldMultiplicity
6.36.	MappingDegree.LocalKFoldMultiplicityFullyUnconditional
6.37.	MappingDegree.LocalKFoldMultiplicityUnconditional
6.38.	MappingDegree.LocalMultiplicityInvariance
6.39.	MappingDegree.LocalNormalForm
6.40.	MappingDegree.LocalSheetDataAtRegularValue
6.41.	MappingDegree.LocalSheetDataFromContMDiff
6.42.	MappingDegree.MeromorphicDivisor
6.43.	MappingDegree.PathConnectedComplFinite
6.44.	MappingDegree.PathSubdivisionByBallCharts
6.45.	MappingDegree.PerChartNonConstancyReduction
6.46.	MappingDegree.PreconnectedFromFiniteComplement
6.47.	MappingDegree.RegularSubsetPreconnected
6.48.	MappingDegree.RegularValueExistsRegUnconditional
6.49.	MappingDegree.RegularValueExistsUnconditional
6.50.	MappingDegree.RoucheBridge
6.51.	MappingDegree.WithinChartWitnessReduction

6.36. MappingDegree.LocalKFoldMultiplicityFullyUnconditional

Source Code
Report Issues

←6.35. MappingDegree.LocalKFoldMultiplicity 6.37. MappingDegree.LocalKFoldMultiplicityUnconditional→

6.36. MappingDegree.LocalKFoldMultiplicityFullyUnconditional🔗

Jacobians.MappingDegree.LocalKFoldMultiplicityFullyUnconditional — source

←6.35. MappingDegree.LocalKFoldMultiplicity 6.37. MappingDegree.LocalKFoldMultiplicityUnconditional→