pith. machine review for the scientific record. sign in

NumberTheory

NumberTheory modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.

108 modules · 1620 thm/lemma · 21270 lines
module thm lemma def lines papers
NumberTheory.AnalyticTrace 19 0 5 446
NumberTheory.AnnularCost 28 0 10 656
NumberTheory.ArgumentPrincipleProved 5 0 0 177
NumberTheory.ArgumentPrincipleSensor 1 0 1 48
NumberTheory.BoundaryTransport 4 0 0 60
NumberTheory.BoundedPhaseVisibility 2 0 1 78
NumberTheory.CarrierBudgetComparison 8 0 1 293
NumberTheory.CirclePhaseLift 10 0 1 378
NumberTheory.ClassicalZeroFreeRegion 3 0 2 104
NumberTheory.CompletedXiSymmetry 8 0 3 121
NumberTheory.CompletedZetaLedger 2 0 1 48
NumberTheory.CompositionDivergence 5 0 0 168
NumberTheory.ConcreteEulerLedger 22 0 3 264
NumberTheory.ContourWinding 5 0 3 142
NumberTheory.CostCoveringBridge 7 0 4 269
NumberTheory.CostOperatorRegularity 5 0 4 226
NumberTheory.CostTwistedLSeries 10 0 3 177
NumberTheory.DefectSampledTrace 12 0 10 474
NumberTheory.DirectedEulerLedger 5 0 2 203
NumberTheory.EffectivePrimePhaseInput 2 0 3 82
NumberTheory.ErdosStrausBoxPhase 3 0 3 75
NumberTheory.ErdosStrausRCL 9 0 1 249
NumberTheory.ErdosStrausResidualClosed 1 0 0 32
NumberTheory.ErdosStrausRotationHierarchy 10 0 7 264
NumberTheory.Erdos_C7_Closure 4 0 0 114
NumberTheory.EulerCarrierComplex 2 0 4 152
NumberTheory.EulerCarrierRealizability 1 0 2 38
NumberTheory.EulerInstantiation 49 0 29 994
NumberTheory.EulerLedgerPartition 3 0 5 99
NumberTheory.EulerProductEqualsZeta 6 0 0 82
NumberTheory.FinitePhaseCompleteness 2 0 0 49
NumberTheory.HadamardFactorization 5 0 3 116
NumberTheory.HadamardGenusOne 11 0 4 239
NumberTheory.HadamardRegularTail 2 0 3 118
NumberTheory.HilbertPolyaCandidate 19 0 8 307
NumberTheory.HilbertPolyaFunctionField 5 0 3 175
NumberTheory.HonestPhaseAdmissibility 7 0 4 139
NumberTheory.HonestPhaseBudgetBridge 7 0 2 249
NumberTheory.LogicErdosStrausBoxPhase 3 0 4 70
NumberTheory.LogicErdosStrausRCL 4 0 1 50
NumberTheory.LogicLedgerInterop 2 0 1 68
NumberTheory.LogicPhaseBudgetBridge 1 0 1 52
NumberTheory.LogicPrimeLedgerAtom 5 0 3 69
NumberTheory.LogicRH_From_RCL 3 0 2 84
NumberTheory.MellinPullback 6 0 2 157
NumberTheory.MellinTransform 7 0 5 166
NumberTheory.MeromorphicCircleOrder 23 0 15 986
NumberTheory.MinimalVisibilityEngine 3 0 1 82
NumberTheory.PhaseBudgetEngineFromRS 0 0 3 52
NumberTheory.PhaseBudgetToErdosStraus 1 0 2 61
NumberTheory.PhaseFailureCost 3 0 2 68
NumberTheory.PhiLadderLattice 19 0 4 253
NumberTheory.Port 0 0 0 48
NumberTheory.Port.BrunTitchmarsh 6 0 1 118
NumberTheory.Port.PNT 7 0 1 135
NumberTheory.Port.RiemannHypothesis 4 0 1 140
NumberTheory.PrimeCostSpectrum 14 2 6 353
NumberTheory.PrimeCostSpectrumPoly 13 1 3 273
NumberTheory.PrimeLedgerAtom 5 0 2 74
NumberTheory.PrimeLedgerStructure 14 0 1 251
NumberTheory.PrimePhaseDistribution 2 0 2 92
NumberTheory.Primes 0 0 0 23
NumberTheory.Primes.ArithmeticFunctions 813 0 10 2882
NumberTheory.Primes.Basic 5 0 0 43
NumberTheory.Primes.Factorization 18 0 1 147
NumberTheory.Primes.GCDLCM 4 0 0 62
NumberTheory.Primes.Modular 15 0 2 191
NumberTheory.Primes.RSConstants 47 0 0 182
NumberTheory.Primes.Resonance 2 0 1 56
NumberTheory.Primes.Squarefree 8 0 0 102
NumberTheory.Primes.Wrappers 9 0 0 80
NumberTheory.ProxyPhysicalizationBridge 11 0 2 189
NumberTheory.RH_Certificate 5 0 0 117
NumberTheory.RH_From_RCL 3 0 0 47
NumberTheory.RSPhysicalThesisDecomposition 3 0 1 69
NumberTheory.RSPhysicalThesisFromRCL 1 0 0 20
NumberTheory.RecognitionTheta 21 0 6 323
NumberTheory.RecognitionTheta.Convergence 2 0 2 93
NumberTheory.RecognitionTheta.MellinFactor 2 0 3 97
NumberTheory.RecognitionTheta.ModularIdentity 1 0 2 72
NumberTheory.ResidualGapHonest 2 0 1 76
NumberTheory.RiemannHypothesis.AttachmentWithMargin 5 0 1 158
NumberTheory.RiemannHypothesis.BRFPlumbing 5 0 2 142
NumberTheory.RiemannHypothesis.CertificateWindow 3 4 7 243
NumberTheory.RiemannHypothesis.ErrorBudget 7 0 6 267
NumberTheory.RiemannHypothesis.LocalToGlobalWedge 3 2 1 276
NumberTheory.RiemannHypothesis.PickGapPersistence 12 0 2 407
NumberTheory.RiemannHypothesis.PrimeTailBounds 13 0 1 321
NumberTheory.RiemannHypothesis.Wedge 3 0 1 68
NumberTheory.RiemannHypothesis.WindowToOscillation 4 2 1 325
NumberTheory.RiemannHypothesis.XiSensorPickPositivity 4 0 6 169
NumberTheory.SampledTrace 4 0 4 195
NumberTheory.StripZeroFreeRegion 6 0 5 175
NumberTheory.SubsetProductPhase 4 0 3 87
NumberTheory.T1BoundaryExclusion 1 0 1 35
NumberTheory.T1PhaseBudgetBound 2 0 1 59
NumberTheory.UniformFailureFloor 3 0 1 38
NumberTheory.UniversalCostSpectrum 10 0 3 225
NumberTheory.VectorCSymmetryOnlyNoGo 9 0 2 160
NumberTheory.VisibilityFromFloorBudget 3 0 1 106
NumberTheory.WeakZeroFreeRegion 4 0 1 117
NumberTheory.XiJBridge 17 0 1 185
NumberTheory.ZeroCompositionInterface 6 0 0 107
NumberTheory.ZeroCompositionLaw 14 0 1 201
NumberTheory.ZeroDoublingLaw 5 0 1 80
NumberTheory.ZeroLocationCost 14 0 5 172
NumberTheory.ZetaFromTheta 6 0 4 174
NumberTheory.ZetaLedgerBridge 16 0 1 300

full source mirrored from github.com/jonwashburn/shape-of-logic