anthropics/formal-math
File Churn
File change frequency (churn) shows the distribution of file updates (days with at least one commit).
Overview
File Change Frequency Overall
  • There are 769 files with 183,419 lines of code.
    • 0 files changed more than 100 times (0 lines of code)
    • 0 files changed 51-100 times (0 lines of code)
    • 0 files changed 21-50 times (0 lines of code)
    • 0 files changed 6-20 times (0 lines of code)
    • 769 files changed 1-5 times (183,419 lines of code)
0% | 0% | 0% | 0% | 100%
Legend:
101+
51-100
21-50
6-20
1-5

explore: grouped by folders | grouped by update frequency | data
Contributors Count Frequency Overall
  • There are 769 files with 183,419 lines of code.
    • 0 files changed by more than 25 contributors (0 lines of code)
    • 0 files changed by 11-25 contributors (0 lines of code)
    • 0 files changed by 6-10 contributors (0 lines of code)
    • 21 files changed by 2-5 contributors (2,265 lines of code)
    • 748 files changed by 1 contributor (181,154 lines of code)
0% | 0% | 0% | 1% | 98%
Legend:
26+
11-25
6-10
2-5
1

explore: grouped by folders | grouped by contributors count | data
File Change Frequency per File Extension
lean, md, json, sh, gitignore, py, toml, txt, yml, rb, yaml
File Change Frequency per Extension
The number of recorded file updates
101+
51-100
21-50
6-20
1-5
lean0% | 0% | 0% | 0% | 100%
py0% | 0% | 0% | 0% | 100%
yaml0% | 0% | 0% | 0% | 100%
rb0% | 0% | 0% | 0% | 100%
toml0% | 0% | 0% | 0% | 100%
File Change Frequency per Logical Decomposition
primary
primary (file change frequency)
The number of recorded file updates
101+
51-100
21-50
6-20
1-5
zeta230% | 0% | 0% | 0% | 100%
3sum-apsp0% | 0% | 0% | 0% | 100%
.github0% | 0% | 0% | 0% | 100%
Most Frequently Changed Files (Top 50)

See data for all files...

File# lines# unitscreatedlast modified# changes
(days)		# contributorsline
churn		first
contributor		latest
contributor
lean
ZeroSummabilityGen.lean
in zeta23/Zeta23/WeilEF
 6 - 2026-08-28 2026-08-28 1 1 +12 / -0 jleder@anthropic.com jleder@anthropic.com
dependabot.yml
in .github
 6 - 2026-08-28 2026-08-28 1 2 +12 / -0 jleder@anthropic.com ralph@anthropic.com
lean
EndStatement.lean
in 3sum-apsp/Solution
 8 - 2026-10-06 2026-10-06 1 1 +9 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
PaperStatements.lean
in 3sum-apsp/Solution
 9 - 2026-10-06 2026-10-06 1 1 +11 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Sec1.lean
in 3sum-apsp/ThreeSumApsp
 11 - 2026-10-06 2026-10-06 1 1 +14 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
LinAlg.lean
in zeta23/Zeta23
 12 - 2026-08-28 2026-08-28 1 1 +24 / -0 jleder@anthropic.com jleder@anthropic.com
lean
XiPrime.lean
in zeta23/scripts/PrintAxioms
 12 - 2026-08-28 2026-08-28 1 2 +26 / -0 jleder@anthropic.com ralph@anthropic.com
lakefile.toml
in zeta23/docbuild
 12 - 2026-08-28 2026-08-28 1 2 +28 / -0 jleder@anthropic.com ralph@anthropic.com
lean
ModelChecks.lean
in 3sum-apsp/ThreeSumApsp
 13 - 2026-10-06 2026-10-06 1 1 +16 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Statements.lean
in 3sum-apsp/ThreeSumApsp
 15 - 2026-10-06 2026-10-06 1 1 +18 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
ConditionalTimes.lean
in 3sum-apsp/ThreeSumApsp
 16 - 2026-10-06 2026-10-06 1 1 +19 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Zeta23.lean
in zeta23
 18 - 2026-08-28 2026-08-28 1 1 +36 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Support.lean
in zeta23/Zeta23/FromPNTPlus/Mathlib/Algebra/Notation
 19 - 2026-08-28 2026-08-28 1 1 +48 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Statement.lean
in zeta23/Zeta23/RvM
 19 - 2026-08-28 2026-08-28 1 1 +46 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ThreeSumApsp.lean
in 3sum-apsp
 20 - 2026-10-06 2026-10-06 1 1 +23 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
RvMChiDefs.lean
in zeta23/Zeta23/ThmE
 20 - 2026-08-28 2026-08-28 1 1 +50 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PairCeiling.lean
in zeta23/scripts/PrintAxioms
 20 - 2026-08-28 2026-08-28 1 2 +42 / -0 jleder@anthropic.com ralph@anthropic.com
lean
Basic.lean
in 3sum-apsp/ThreeSumApsp/Util
 21 - 2026-10-06 2026-10-06 1 1 +24 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Sec5.lean
in 3sum-apsp/ThreeSumApsp
 22 - 2026-10-06 2026-10-06 1 1 +25 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
QuarticWindow.lean
in zeta23/Zeta23/XiPrime
 22 - 2026-08-28 2026-08-28 1 1 +44 / -0 jleder@anthropic.com jleder@anthropic.com
lean
GevreyPhi.lean
in zeta23/Zeta23/Taper
 23 - 2026-08-28 2026-08-28 1 1 +54 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Sec2.lean
in 3sum-apsp/ThreeSumApsp
 24 - 2026-10-06 2026-10-06 1 1 +27 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Program.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/AllInstances
 25 - 2026-10-06 2026-10-06 1 1 +34 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
RoutineFacts.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30
 25 - 2026-10-06 2026-10-06 1 1 +35 / -0 ecprice@anthropic.com ecprice@anthropic.com
lakefile.toml
in zeta23
 25 - 2026-08-28 2026-08-28 1 2 +76 / -14 jleder@anthropic.com jleder@anthropic.com
lean
Sec4.lean
in 3sum-apsp/ThreeSumApsp
 26 - 2026-10-06 2026-10-06 1 1 +29 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Basic.lean
in zeta23/Zeta23/FromPNTPlus/Mathlib/Analysis/SpecialFunctions/Log
 26 - 2026-08-28 2026-08-28 1 1 +56 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Final.lean
in zeta23/Zeta23/MV
 26 - 2026-08-28 2026-08-28 1 1 +72 / -0 jleder@anthropic.com jleder@anthropic.com
lean
BacklundDefs.lean
in zeta23/Zeta23/RvM
 26 - 2026-08-28 2026-08-28 1 1 +66 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Theorem5.lean
in 3sum-apsp/ThreeSumApsp/RunningTimes/Sec2
 27 - 2026-10-06 2026-10-06 1 1 +35 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Profile.lean
in zeta23/Zeta23/Defs
 27 - 2026-08-28 2026-08-28 1 1 +68 / -0 jleder@anthropic.com jleder@anthropic.com
lean
InstancePriorities.lean
in zeta23/Zeta23/Prelude
 27 - 2026-08-28 2026-08-28 1 1 +60 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Complete.lean
in zeta23/Zeta23/GammaFacts
 27 - 2026-08-28 2026-08-28 1 1 +64 / -0 jleder@anthropic.com jleder@anthropic.com
lean
MonoConvolution.lean
in 3sum-apsp/ThreeSumApsp/Sec1
 28 - 2026-10-06 2026-10-06 1 1 +36 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Final.lean
in zeta23/Zeta23/PrimeSideB
 28 - 2026-08-28 2026-08-28 1 1 +70 / -0 jleder@anthropic.com jleder@anthropic.com
lakefile.toml
in 3sum-apsp
 29 - 2026-10-06 2026-10-06 1 1 +36 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Family.lean
in zeta23/Zeta23/XiPrime/QuarticWindow
 29 - 2026-08-28 2026-08-28 1 1 +74 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Corollary39.lean
in 3sum-apsp/ThreeSumApsp/RunningTimes/Sec5
 30 - 2026-10-06 2026-10-06 1 1 +40 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
PrintAxioms.lean
in zeta23/scripts
 30 - 2026-08-28 2026-08-28 1 2 +62 / -0 jleder@anthropic.com ralph@anthropic.com
lean
Sec3.lean
in 3sum-apsp/ThreeSumApsp
 31 - 2026-10-06 2026-10-06 1 1 +33 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
XiPrime.lean
in zeta23/ChallengeDeps
 32 - 2026-08-28 2026-08-28 1 2 +88 / -0 jleder@anthropic.com ralph@anthropic.com
lean
Realized.lean
in 3sum-apsp/ThreeSumApsp/Machine
 33 - 2026-10-06 2026-10-06 1 1 +43 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
BruteForceClaim.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem19
 33 - 2026-10-06 2026-10-06 1 1 +41 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
LT.lean
in zeta23/Zeta23/XiPrime/Coeff
 33 - 2026-08-28 2026-08-28 1 1 +84 / -0 jleder@anthropic.com jleder@anthropic.com
lean
TracesHyp.lean
in zeta23/Zeta23/ThmDE
 33 - 2026-08-28 2026-08-28 1 1 +80 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Theorem30.lean
in 3sum-apsp/ThreeSumApsp/RunningTimes/Sec4
 34 - 2026-10-06 2026-10-06 1 1 +43 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
LightModel.lean
in 3sum-apsp/ThreeSumApsp/Programs
 34 - 2026-10-06 2026-10-06 1 1 +43 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Flag.lean
in 3sum-apsp/ThreeSumApsp/Util
 35 - 2026-10-06 2026-10-06 1 1 +47 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
ZetaConj.lean
in zeta23/Zeta23/FromPNTPlus
 35 - 2026-08-28 2026-08-28 1 1 +82 / -0 jleder@anthropic.com jleder@anthropic.com
lean
RvMChi.lean
in zeta23/Zeta23/ThmE
 35 - 2026-08-28 2026-08-28 1 1 +82 / -0 jleder@anthropic.com jleder@anthropic.com
Files With Most Churn (Top 50)
Based on the number of lines added and deleted across all commits.

See data for all files...

File# lines# unitscreatedlast modified# changes
(days)		# contributorsline
churn		first
contributor		latest
contributor
lean
MediumPNT.lean
in zeta23/Zeta23/FromPNTPlus
 3387 - 2026-08-28 2026-08-28 1 1 +7462 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZetaBounds.lean
in zeta23/Zeta23/FromPNTPlus
 2788 - 2026-08-28 2026-08-28 1 1 +6120 / -0 jleder@anthropic.com jleder@anthropic.com
lean
 3474 - 2026-10-06 2026-10-06 1 1 +4194 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Window.lean
in zeta23/Zeta23/ThmD
 1737 - 2026-08-28 2026-08-28 1 1 +3584 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Assembly.lean
in zeta23/Zeta23
 1451 - 2026-08-28 2026-08-28 1 1 +3266 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PrimeSideChi.lean
in zeta23/Zeta23/ThmE
 1381 - 2026-08-28 2026-08-28 1 1 +2878 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZeroFree.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1351 - 2026-08-28 2026-08-28 1 1 +2818 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Basic.lean
in zeta23/Zeta23/PrimeSideA
 1276 - 2026-08-28 2026-08-28 1 1 +2770 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Chebyshev.lean
in zeta23/Zeta23
 1144 - 2026-08-28 2026-08-28 1 1 +2422 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Expansion.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1035 - 2026-08-28 2026-08-28 1 1 +2322 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ResidueCalcOnRectangles.lean
in zeta23/Zeta23/FromPNTPlus
 1062 - 2026-08-28 2026-08-28 1 1 +2306 / -0 jleder@anthropic.com jleder@anthropic.com
lean
TestWeight.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1012 - 2026-08-28 2026-08-28 1 1 +2272 / -0 jleder@anthropic.com jleder@anthropic.com
lean
MellinCalculus.lean
in zeta23/Zeta23/FromPNTPlus
 974 - 2026-08-28 2026-08-28 1 1 +2096 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Transfer.lean
in zeta23/Zeta23/XiPrime
 982 - 2026-08-28 2026-08-28 1 1 +2074 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PPChi.lean
in zeta23/Zeta23/ThmE
 946 - 2026-08-28 2026-08-28 1 1 +2014 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Decay.lean
in zeta23/Zeta23/Taper
 908 - 2026-08-28 2026-08-28 1 1 +2008 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZeroSide.lean
in zeta23/Zeta23
 830 - 2026-08-28 2026-08-28 1 1 +1994 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Effective.lean
in zeta23/Zeta23/WeilEF
 909 - 2026-08-28 2026-08-28 1 1 +1876 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EndsE1.lean
in zeta23/Zeta23/PrimeSideA
 851 - 2026-08-28 2026-08-28 1 1 +1802 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PrimeSideB.lean
in zeta23/Zeta23
 746 - 2026-08-28 2026-08-28 1 1 +1652 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EndsNu.lean
in zeta23/Zeta23/PrimeSideA
 768 - 2026-08-28 2026-08-28 1 1 +1642 / -0 jleder@anthropic.com jleder@anthropic.com
lean
VerticalLine.lean
in zeta23/Zeta23/WeilEF
 763 - 2026-08-28 2026-08-28 1 1 +1576 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ExplicitFormula.lean
in zeta23/Zeta23
 662 - 2026-08-28 2026-08-28 1 1 +1468 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EFExpansion.lean
in zeta23/Zeta23/XiPrime/Hardy
 650 - 2026-08-28 2026-08-28 1 1 +1454 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PPKernel.lean
in zeta23/Zeta23/PrimeSideB
 642 - 2026-08-28 2026-08-28 1 1 +1428 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EndsCore.lean
in zeta23/Zeta23/PrimeSideA
 604 - 2026-08-28 2026-08-28 1 1 +1396 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Tail.lean
in zeta23/Zeta23
 615 - 2026-08-28 2026-08-28 1 1 +1382 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Traces.lean
in zeta23/Zeta23/ThmD
 640 - 2026-08-28 2026-08-28 1 1 +1334 / -0 jleder@anthropic.com jleder@anthropic.com
lean
IntMuChi.lean
in zeta23/Zeta23/ThmE
 641 - 2026-08-28 2026-08-28 1 1 +1332 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Landau.lean
in zeta23/Zeta23/WeilEF
 641 - 2026-08-28 2026-08-28 1 1 +1322 / -0 jleder@anthropic.com jleder@anthropic.com
lean
FullLineChiProof.lean
in zeta23/Zeta23/ThmE
 613 - 2026-08-28 2026-08-28 1 1 +1302 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PP.lean
in zeta23/Zeta23/XiPrime/PrimeSide
 605 - 2026-08-28 2026-08-28 1 1 +1288 / -0 jleder@anthropic.com jleder@anthropic.com
lean
StirlingVert.lean
in zeta23/Zeta23/GammaFacts
 581 - 2026-08-28 2026-08-28 1 1 +1284 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Norms.lean
in zeta23/Zeta23/Taper
 577 - 2026-08-28 2026-08-28 1 1 +1250 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Dependence.lean
in zeta23/Zeta23/XiPrime/Transfer
 565 - 2026-08-28 2026-08-28 1 1 +1202 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Final.lean
in zeta23/Zeta23/XiPrime
 516 - 2026-08-28 2026-08-28 1 1 +1200 / -0 jleder@anthropic.com jleder@anthropic.com
lean
FullLine.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 542 - 2026-08-28 2026-08-28 1 1 +1186 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Assembly.lean
in zeta23/Zeta23/XiPrime
 545 - 2026-08-28 2026-08-28 1 1 +1178 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Traces.lean
in zeta23/Zeta23/XiPrime/PrimeSide
 528 - 2026-08-28 2026-08-28 1 1 +1160 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PsiC.lean
in zeta23/Zeta23/ThmD
 535 - 2026-08-28 2026-08-28 1 1 +1146 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Generic.lean
in zeta23/Zeta23/XiPrime/ZeroCount
 556 - 2026-08-28 2026-08-28 1 1 +1144 / -0 jleder@anthropic.com jleder@anthropic.com
lean
NonSquarefree.lean
in zeta23/Zeta23/XiPrime/Coeff
 522 - 2026-08-28 2026-08-28 1 1 +1130 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZeroFree.lean
in zeta23/Zeta23/XiPrime/Hardy
 527 - 2026-08-28 2026-08-28 1 1 +1120 / -0 jleder@anthropic.com jleder@anthropic.com
lean
AssemblyQ.lean
in zeta23/Zeta23/ThmE
 515 - 2026-08-28 2026-08-28 1 1 +1118 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Spacing.lean
in zeta23/Zeta23/MV
 515 - 2026-08-28 2026-08-28 1 1 +1088 / -0 jleder@anthropic.com jleder@anthropic.com
lean
MainTermChi.lean
in zeta23/Zeta23/ThmE
 520 - 2026-08-28 2026-08-28 1 1 +1082 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Moments.lean
in zeta23/Zeta23/XiPrime/QuarticWindow
 505 - 2026-08-28 2026-08-28 1 1 +1074 / -0 jleder@anthropic.com jleder@anthropic.com
lean
IntMu.lean
in zeta23/Zeta23/GammaFacts
 515 - 2026-08-28 2026-08-28 1 1 +1048 / -0 jleder@anthropic.com jleder@anthropic.com
lean
WindowCore.lean
in zeta23/Zeta23/ThmD
 410 - 2026-08-28 2026-08-28 1 1 +1028 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Functional.lean
in zeta23/Zeta23/ThmD
 464 - 2026-08-28 2026-08-28 1 1 +1010 / -0 jleder@anthropic.com jleder@anthropic.com
Files With Most Contributors (Top 50)
Based on the number of unique email addresses found in commits.

See data for all files...

File# lines# unitscreatedlast modified# changes
(days)		# contributorsline
churn		first
contributor		latest
contributor
dependabot.yml
in .github
 6 - 2026-08-28 2026-08-28 1 2 +12 / -0 jleder@anthropic.com ralph@anthropic.com
lean
XiPrime.lean
in zeta23/ChallengeDeps
 32 - 2026-08-28 2026-08-28 1 2 +88 / -0 jleder@anthropic.com ralph@anthropic.com
228 - 2026-08-28 2026-08-28 1 2 +722 / -222 ralph@anthropic.com jleder@anthropic.com
lean
XiPrime.lean
in zeta23/Solution
 45 - 2026-08-28 2026-08-28 1 2 +104 / -0 jleder@anthropic.com ralph@anthropic.com
lean
Solution.lean
in zeta23
 119 - 2026-08-28 2026-08-28 1 2 +284 / -0 jleder@anthropic.com ralph@anthropic.com
lakefile.toml
in zeta23/docbuild
 12 - 2026-08-28 2026-08-28 1 2 +28 / -0 jleder@anthropic.com ralph@anthropic.com
validate-formalization.rb
in zeta23/scripts
 157 4 2026-08-28 2026-08-28 1 2 +352 / -0 jleder@anthropic.com ralph@anthropic.com
lean
PrintAxioms.lean
in zeta23/scripts
 30 - 2026-08-28 2026-08-28 1 2 +62 / -0 jleder@anthropic.com ralph@anthropic.com
lean
PairCeiling.lean
in zeta23/scripts/PrintAxioms
 20 - 2026-08-28 2026-08-28 1 2 +42 / -0 jleder@anthropic.com ralph@anthropic.com
lean
XiPrime.lean
in zeta23/scripts/PrintAxioms
 12 - 2026-08-28 2026-08-28 1 2 +26 / -0 jleder@anthropic.com ralph@anthropic.com
lakefile.toml
in zeta23
 25 - 2026-08-28 2026-08-28 1 2 +76 / -14 jleder@anthropic.com jleder@anthropic.com
lean
XiPrime.lean
in zeta23/Challenge
 86 - 2026-08-28 2026-08-28 1 2 +212 / -0 jleder@anthropic.com ralph@anthropic.com
lean
Sylvester.lean
in zeta23/Zeta23/LinAlg
 282 - 2026-08-28 2026-08-28 1 2 +621 / -3 ralph@anthropic.com jleder@anthropic.com
lean
Weyl.lean
in zeta23/Zeta23/LinAlg
 123 - 2026-08-28 2026-08-28 1 2 +275 / -3 ralph@anthropic.com jleder@anthropic.com
lean
HermitianPosPart.lean
in zeta23/Zeta23/LinAlg
 167 - 2026-08-28 2026-08-28 1 2 +411 / -3 ralph@anthropic.com jleder@anthropic.com
lean
VonNeumann.lean
in zeta23/Zeta23/LinAlg
 181 - 2026-08-28 2026-08-28 1 2 +411 / -3 ralph@anthropic.com jleder@anthropic.com
lean
Inertia.lean
in zeta23/Zeta23/LinAlg
 125 - 2026-08-28 2026-08-28 1 2 +279 / -3 ralph@anthropic.com jleder@anthropic.com
lean
RankTrace.lean
in zeta23/Zeta23/LinAlg
 239 - 2026-08-28 2026-08-28 1 2 +537 / -3 ralph@anthropic.com jleder@anthropic.com
lean
PosIndex.lean
in zeta23/Zeta23/LinAlg
 103 - 2026-08-28 2026-08-28 1 2 +257 / -3 ralph@anthropic.com jleder@anthropic.com
lean
 85 - 2026-08-28 2026-08-28 1 2 +218 / -0 jleder@anthropic.com ralph@anthropic.com
lean
 188 - 2026-08-28 2026-08-28 1 2 +462 / -0 jleder@anthropic.com ralph@anthropic.com
lean
Zeta23.lean
in zeta23
 18 - 2026-08-28 2026-08-28 1 1 +36 / -0 jleder@anthropic.com jleder@anthropic.com
lean
MV.lean
in zeta23/Zeta23
 212 - 2026-08-28 2026-08-28 1 1 +480 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Limit.lean
in zeta23/Zeta23/ThmDE
 43 - 2026-08-28 2026-08-28 1 1 +98 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Endgame.lean
in zeta23/Zeta23/ThmDE
 420 - 2026-08-28 2026-08-28 1 1 +870 / -0 jleder@anthropic.com jleder@anthropic.com
lean
TracesHyp.lean
in zeta23/Zeta23/ThmDE
 33 - 2026-08-28 2026-08-28 1 1 +80 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Traces.lean
in zeta23/Zeta23/ThmDE
 251 - 2026-08-28 2026-08-28 1 1 +552 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Mult.lean
in zeta23/Zeta23/ThmDE
 441 - 2026-08-28 2026-08-28 1 1 +920 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Final.lean
in zeta23/Zeta23/ThmDE
 136 - 2026-08-28 2026-08-28 1 1 +312 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PP.lean
in zeta23/Zeta23/ThmDE
 47 - 2026-08-28 2026-08-28 1 1 +106 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZeroSide.lean
in zeta23/Zeta23/ThmDE
 61 - 2026-08-28 2026-08-28 1 1 +148 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Concrete.lean
in zeta23/Zeta23/ThmDE
 225 - 2026-08-28 2026-08-28 1 1 +484 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PPKernel.lean
in zeta23/Zeta23/PrimeSideB
 642 - 2026-08-28 2026-08-28 1 1 +1428 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Traces.lean
in zeta23/Zeta23/PrimeSideB
 193 - 2026-08-28 2026-08-28 1 1 +418 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Final.lean
in zeta23/Zeta23/PrimeSideB
 28 - 2026-08-28 2026-08-28 1 1 +70 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PP.lean
in zeta23/Zeta23/PrimeSideB
 440 - 2026-08-28 2026-08-28 1 1 +962 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PPOffDiag.lean
in zeta23/Zeta23/PrimeSideB
 166 - 2026-08-28 2026-08-28 1 1 +346 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Concrete.lean
in zeta23/Zeta23/PrimeSideB
 83 - 2026-08-28 2026-08-28 1 1 +212 / -0 jleder@anthropic.com jleder@anthropic.com
lean
GzGp.lean
in zeta23/Zeta23/Hypotheses
 130 - 2026-08-28 2026-08-28 1 1 +296 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Unconditional.lean
in zeta23/Zeta23
 42 - 2026-08-28 2026-08-28 1 1 +100 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Taper.lean
in zeta23/Zeta23
 153 - 2026-08-28 2026-08-28 1 1 +344 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EFContour.lean
in zeta23/Zeta23/XiPrime/Hardy
 426 - 2026-08-28 2026-08-28 1 1 +910 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Count.lean
in zeta23/Zeta23/XiPrime/Hardy
 263 - 2026-08-28 2026-08-28 1 1 +582 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EFBasic.lean
in zeta23/Zeta23/XiPrime/Hardy
 297 - 2026-08-28 2026-08-28 1 1 +680 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EFFinal.lean
in zeta23/Zeta23/XiPrime/Hardy
 59 - 2026-08-28 2026-08-28 1 1 +136 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EFExpansion.lean
in zeta23/Zeta23/XiPrime/Hardy
 650 - 2026-08-28 2026-08-28 1 1 +1454 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZeroFree.lean
in zeta23/Zeta23/XiPrime/Hardy
 527 - 2026-08-28 2026-08-28 1 1 +1120 / -0 jleder@anthropic.com jleder@anthropic.com
lean
TwoLine.lean
in zeta23/Zeta23/XiPrime/Hardy
 259 - 2026-08-28 2026-08-28 1 1 +564 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EFMain.lean
in zeta23/Zeta23/XiPrime/Hardy
 402 - 2026-08-28 2026-08-28 1 1 +846 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Basic.lean
in zeta23/Zeta23/XiPrime/Hardy
 240 - 2026-08-28 2026-08-28 1 1 +578 / -0 jleder@anthropic.com jleder@anthropic.com
Files With Least Contributors (Top 50)
Based on the number of unique email addresses found in commits.

See data for all files...

File# lines# unitscreatedlast modified# changes
(days)		# contributorsline
churn		first
contributor		latest
contributor
lean
 3474 - 2026-10-06 2026-10-06 1 1 +4194 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
MediumPNT.lean
in zeta23/Zeta23/FromPNTPlus
 3387 - 2026-08-28 2026-08-28 1 1 +7462 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZetaBounds.lean
in zeta23/Zeta23/FromPNTPlus
 2788 - 2026-08-28 2026-08-28 1 1 +6120 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Window.lean
in zeta23/Zeta23/ThmD
 1737 - 2026-08-28 2026-08-28 1 1 +3584 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Assembly.lean
in zeta23/Zeta23
 1451 - 2026-08-28 2026-08-28 1 1 +3266 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PrimeSideChi.lean
in zeta23/Zeta23/ThmE
 1381 - 2026-08-28 2026-08-28 1 1 +2878 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZeroFree.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1351 - 2026-08-28 2026-08-28 1 1 +2818 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Basic.lean
in zeta23/Zeta23/PrimeSideA
 1276 - 2026-08-28 2026-08-28 1 1 +2770 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Chebyshev.lean
in zeta23/Zeta23
 1144 - 2026-08-28 2026-08-28 1 1 +2422 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ResidueCalcOnRectangles.lean
in zeta23/Zeta23/FromPNTPlus
 1062 - 2026-08-28 2026-08-28 1 1 +2306 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Expansion.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1035 - 2026-08-28 2026-08-28 1 1 +2322 / -0 jleder@anthropic.com jleder@anthropic.com
lean
TestWeight.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1012 - 2026-08-28 2026-08-28 1 1 +2272 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Transfer.lean
in zeta23/Zeta23/XiPrime
 982 - 2026-08-28 2026-08-28 1 1 +2074 / -0 jleder@anthropic.com jleder@anthropic.com
lean
MellinCalculus.lean
in zeta23/Zeta23/FromPNTPlus
 974 - 2026-08-28 2026-08-28 1 1 +2096 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PPChi.lean
in zeta23/Zeta23/ThmE
 946 - 2026-08-28 2026-08-28 1 1 +2014 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Effective.lean
in zeta23/Zeta23/WeilEF
 909 - 2026-08-28 2026-08-28 1 1 +1876 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Decay.lean
in zeta23/Zeta23/Taper
 908 - 2026-08-28 2026-08-28 1 1 +2008 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EndsE1.lean
in zeta23/Zeta23/PrimeSideA
 851 - 2026-08-28 2026-08-28 1 1 +1802 / -0 jleder@anthropic.com jleder@anthropic.com
lean
ZeroSide.lean
in zeta23/Zeta23
 830 - 2026-08-28 2026-08-28 1 1 +1994 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EndsNu.lean
in zeta23/Zeta23/PrimeSideA
 768 - 2026-08-28 2026-08-28 1 1 +1642 / -0 jleder@anthropic.com jleder@anthropic.com
lean
VerticalLine.lean
in zeta23/Zeta23/WeilEF
 763 - 2026-08-28 2026-08-28 1 1 +1576 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PrimeSideB.lean
in zeta23/Zeta23
 746 - 2026-08-28 2026-08-28 1 1 +1652 / -0 jleder@anthropic.com jleder@anthropic.com
lean
NodeArray.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 740 - 2026-10-06 2026-10-06 1 1 +819 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Host.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight
 714 - 2026-10-06 2026-10-06 1 1 +807 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
AllPairs.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus
 704 - 2026-10-06 2026-10-06 1 1 +783 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
BandArray.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode
 669 - 2026-10-06 2026-10-06 1 1 +755 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
ExplicitFormula.lean
in zeta23/Zeta23
 662 - 2026-08-28 2026-08-28 1 1 +1468 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EFExpansion.lean
in zeta23/Zeta23/XiPrime/Hardy
 650 - 2026-08-28 2026-08-28 1 1 +1454 / -0 jleder@anthropic.com jleder@anthropic.com
lean
PPKernel.lean
in zeta23/Zeta23/PrimeSideB
 642 - 2026-08-28 2026-08-28 1 1 +1428 / -0 jleder@anthropic.com jleder@anthropic.com
lean
IntMuChi.lean
in zeta23/Zeta23/ThmE
 641 - 2026-08-28 2026-08-28 1 1 +1332 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Landau.lean
in zeta23/Zeta23/WeilEF
 641 - 2026-08-28 2026-08-28 1 1 +1322 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Traces.lean
in zeta23/Zeta23/ThmD
 640 - 2026-08-28 2026-08-28 1 1 +1334 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Codes.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted
 633 - 2026-10-06 2026-10-06 1 1 +705 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Nodes.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 620 - 2026-10-06 2026-10-06 1 1 +686 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Tail.lean
in zeta23/Zeta23
 615 - 2026-08-28 2026-08-28 1 1 +1382 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Strassen.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing
 615 - 2026-10-06 2026-10-06 1 1 +707 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
FullLineChiProof.lean
in zeta23/Zeta23/ThmE
 613 - 2026-08-28 2026-08-28 1 1 +1302 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Buckets.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 608 - 2026-10-06 2026-10-06 1 1 +681 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
PP.lean
in zeta23/Zeta23/XiPrime/PrimeSide
 605 - 2026-08-28 2026-08-28 1 1 +1288 / -0 jleder@anthropic.com jleder@anthropic.com
lean
EndsCore.lean
in zeta23/Zeta23/PrimeSideA
 604 - 2026-08-28 2026-08-28 1 1 +1396 / -0 jleder@anthropic.com jleder@anthropic.com
lean
SharedStage.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5
 601 - 2026-10-06 2026-10-06 1 1 +648 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
MaxTriangle.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight
 597 - 2026-10-06 2026-10-06 1 1 +657 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
StirlingVert.lean
in zeta23/Zeta23/GammaFacts
 581 - 2026-08-28 2026-08-28 1 1 +1284 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Loop.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host
 580 - 2026-10-06 2026-10-06 1 1 +645 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Host.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/NegativeTriangle
 580 - 2026-10-06 2026-10-06 1 1 +646 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Norms.lean
in zeta23/Zeta23/Taper
 577 - 2026-08-28 2026-08-28 1 1 +1250 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Reduction.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 574 - 2026-10-06 2026-10-06 1 1 +654 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Dependence.lean
in zeta23/Zeta23/XiPrime/Transfer
 565 - 2026-08-28 2026-08-28 1 1 +1202 / -0 jleder@anthropic.com jleder@anthropic.com
lean
Modulus.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 565 - 2026-10-06 2026-10-06 1 1 +632 / -0 ecprice@anthropic.com ecprice@anthropic.com
lean
Generic.lean
in zeta23/Zeta23/XiPrime/ZeroCount
 556 - 2026-08-28 2026-08-28 1 1 +1144 / -0 jleder@anthropic.com jleder@anthropic.com
Correlations

File Size vs. Number of Changes: 769 points

3sum-apsp/Challenge/EndStatement.lean x: 71 lines of code y: 1 # changes 3sum-apsp/Challenge/PaperStatements.lean x: 218 lines of code y: 1 # changes 3sum-apsp/EndStatement.lean x: 115 lines of code y: 1 # changes 3sum-apsp/PaperStatements.lean x: 3474 lines of code y: 1 # changes 3sum-apsp/Solution/EndStatement.lean x: 8 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp.lean x: 20 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/ConditionalTimes.lean x: 16 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 57 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 307 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 150 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 177 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 104 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 134 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 273 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/Conditions.lean x: 127 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/Dispatcher.lean x: 79 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 202 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 427 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 294 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 229 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 338 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/ArrayAt.lean x: 110 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/Copy.lean x: 66 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/CountSort.lean x: 433 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 240 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/Logs.lean x: 235 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/Merge.lean x: 166 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/MergeSort.lean x: 195 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 95 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 159 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 186 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 371 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/RowMajor.lean x: 84 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 316 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/Syntax.lean x: 138 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 346 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Lang/TopProcedure.lean x: 329 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 50 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 33 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/AllInstances/RegimeTest.lean x: 322 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/AllInstances/Solver.lean x: 340 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 502 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/AllBands.lean x: 264 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 669 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArrayFacts.lean x: 175 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/LibraryContracts.lean x: 56 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Pruned/Recursion.lean x: 352 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Pruned/Union.lean x: 246 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 601 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 286 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 633 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Sort.lean x: 309 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 461 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/CountPrime.lean x: 426 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/RingOps.lean x: 281 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/SizeTable.lean x: 94 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 615 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 481 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceCount.lean x: 40 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 402 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 580 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/Classes.lean x: 452 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 536 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Parameters/Primes.lean x: 225 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/TimeBound/Total.lean x: 212 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 412 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Buckets.lean x: 608 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 440 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Distinct.lean x: 362 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 565 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 740 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Reduction.lean x: 574 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/TimeBound.lean x: 156 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 255 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Passes.lean x: 381 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 704 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/BitSearch.lean x: 420 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec4/ChoosingParameters/InnerProduct.lean x: 123 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/Contracts.lean x: 499 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/Insert.lean x: 366 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 390 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/Tile.lean x: 189 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 714 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/RunningTimes/Sec2/Theorem5.lean x: 27 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 515 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 525 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Sec4/Lemma27_28.lean x: 491 lines of code y: 1 # changes 3sum-apsp/ThreeSumApsp/Util/Asymptotics/Scale.lean x: 260 lines of code y: 1 # changes 3sum-apsp/scripts/index.py x: 383 lines of code y: 1 # changes .github/dependabot.yml x: 6 lines of code y: 1 # changes zeta23/Zeta23/Assembly.lean x: 1451 lines of code y: 1 # changes zeta23/Zeta23/Chebyshev.lean x: 1144 lines of code y: 1 # changes zeta23/Zeta23/ExplicitFormula.lean x: 662 lines of code y: 1 # changes zeta23/Zeta23/Final.lean x: 299 lines of code y: 1 # changes zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 3387 lines of code y: 1 # changes zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 974 lines of code y: 1 # changes zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 1062 lines of code y: 1 # changes zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 2788 lines of code y: 1 # changes zeta23/Zeta23/PrimeSideA/Basic.lean x: 1276 lines of code y: 1 # changes zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 851 lines of code y: 1 # changes zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 768 lines of code y: 1 # changes zeta23/Zeta23/PrimeSideB/PPKernel.lean x: 642 lines of code y: 1 # changes zeta23/Zeta23/RvM/MainTerm.lean x: 468 lines of code y: 1 # changes zeta23/Zeta23/Tail/Count.lean x: 472 lines of code y: 1 # changes zeta23/Zeta23/Taper/Decay.lean x: 908 lines of code y: 1 # changes zeta23/Zeta23/ThmD/Window.lean x: 1737 lines of code y: 1 # changes zeta23/Zeta23/ThmE/FullLineChiProof.lean x: 613 lines of code y: 1 # changes zeta23/Zeta23/ThmE/PPChi.lean x: 946 lines of code y: 1 # changes zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 1381 lines of code y: 1 # changes zeta23/Zeta23/WeilEF/VerticalLine.lean x: 763 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/Assembly.lean x: 545 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 1035 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 1012 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 1351 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/Hardy/EFContour/Rectangle.lean x: 400 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/Hardy/EFExpansion.lean x: 650 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/Hardy/ZeroFree.lean x: 527 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/Transfer.lean x: 982 lines of code y: 1 # changes zeta23/Zeta23/XiPrime/ZeroCount/Generic.lean x: 556 lines of code y: 1 # changes zeta23/Zeta23/ZeroSide.lean x: 830 lines of code y: 1 # changes
1.0
# changes
  min: 1.0
  average: 1.0
  25th percentile: 1.0
  median: 1.0
  75th percentile: 1.0
  max: 1.0
0 3474.0
lines of code
min: 6.0 | average: 238.52 | 25th percentile: 94.0 | median: 170.0 | 75th percentile: 306.5 | max: 3474.0

Number of Contributors vs. Number of Changes: 769 points

3sum-apsp/Challenge/EndStatement.lean x: 1 # contributors y: 1 # changes zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 2 # contributors y: 1 # changes
1.0
# changes
  min: 1.0
  average: 1.0
  25th percentile: 1.0
  median: 1.0
  75th percentile: 1.0
  max: 1.0
0 2.0
# contributors
min: 1.0 | average: 1.03 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 2.0

Number of Contributors vs. File Size: 769 points

3sum-apsp/Challenge/EndStatement.lean x: 1 # contributors y: 71 lines of code 3sum-apsp/Challenge/PaperStatements.lean x: 1 # contributors y: 218 lines of code 3sum-apsp/EndStatement.lean x: 1 # contributors y: 115 lines of code 3sum-apsp/PaperStatements.lean x: 1 # contributors y: 3474 lines of code 3sum-apsp/Solution/EndStatement.lean x: 1 # contributors y: 8 lines of code 3sum-apsp/ThreeSumApsp.lean x: 1 # contributors y: 20 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 1 # contributors y: 57 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 # contributors y: 307 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 # contributors y: 150 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 # contributors y: 177 lines of code 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 1 # contributors y: 104 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 1 # contributors y: 134 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 # contributors y: 273 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 # contributors y: 202 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 # contributors y: 427 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 1 # contributors y: 294 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 1 # contributors y: 229 lines of code 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 # contributors y: 338 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 1 # contributors y: 240 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 1 # contributors y: 95 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 1 # contributors y: 159 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 1 # contributors y: 186 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 # contributors y: 371 lines of code 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 1 # contributors y: 316 lines of code 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 1 # contributors y: 346 lines of code 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 # contributors y: 50 lines of code 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 1 # contributors y: 33 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 # contributors y: 502 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 # contributors y: 669 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 # contributors y: 601 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 # contributors y: 286 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 # contributors y: 633 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 1 # contributors y: 461 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 # contributors y: 615 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 # contributors y: 481 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 1 # contributors y: 402 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 # contributors y: 580 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Text.lean x: 1 # contributors y: 356 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 1 # contributors y: 536 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 # contributors y: 412 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 1 # contributors y: 440 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 1 # contributors y: 565 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 # contributors y: 740 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 1 # contributors y: 620 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 1 # contributors y: 255 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 # contributors y: 704 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 1 # contributors y: 390 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 1 # contributors y: 714 lines of code 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 1 # contributors y: 515 lines of code 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 1 # contributors y: 525 lines of code zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 2 # contributors y: 167 lines of code zeta23/Zeta23/LinAlg/Inertia.lean x: 2 # contributors y: 125 lines of code zeta23/Zeta23/LinAlg/PosIndex.lean x: 2 # contributors y: 103 lines of code zeta23/Zeta23/LinAlg/RankTrace.lean x: 2 # contributors y: 239 lines of code zeta23/Zeta23/LinAlg/Sylvester.lean x: 2 # contributors y: 282 lines of code zeta23/Zeta23/LinAlg/VonNeumann.lean x: 2 # contributors y: 181 lines of code zeta23/Zeta23/LinAlg/Weyl.lean x: 2 # contributors y: 123 lines of code zeta23/formalization.yaml x: 2 # contributors y: 228 lines of code .github/dependabot.yml x: 2 # contributors y: 6 lines of code zeta23/Challenge/XiPrime.lean x: 2 # contributors y: 86 lines of code zeta23/ChallengeDeps/XiPrime.lean x: 2 # contributors y: 32 lines of code zeta23/Solution/XiPrime.lean x: 2 # contributors y: 45 lines of code zeta23/lakefile.toml x: 2 # contributors y: 25 lines of code zeta23/scripts/validate-formalization.rb x: 2 # contributors y: 157 lines of code zeta23/Zeta23/Assembly.lean x: 1 # contributors y: 1451 lines of code zeta23/Zeta23/Chebyshev.lean x: 1 # contributors y: 1144 lines of code zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 1 # contributors y: 3387 lines of code zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 1 # contributors y: 974 lines of code zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 1 # contributors y: 1062 lines of code zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 1 # contributors y: 2788 lines of code zeta23/Zeta23/GammaFacts/Series.lean x: 1 # contributors y: 478 lines of code zeta23/Zeta23/PrimeSideA/Basic.lean x: 1 # contributors y: 1276 lines of code zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 1 # contributors y: 851 lines of code zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 1 # contributors y: 768 lines of code zeta23/Zeta23/Taper/Decay.lean x: 1 # contributors y: 908 lines of code zeta23/Zeta23/ThmD/Window.lean x: 1 # contributors y: 1737 lines of code zeta23/Zeta23/ThmE/PPChi.lean x: 1 # contributors y: 946 lines of code zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 1 # contributors y: 1381 lines of code zeta23/Zeta23/WeilEF/VerticalLine.lean x: 1 # contributors y: 763 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 1 # contributors y: 1035 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 1 # contributors y: 1012 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 1 # contributors y: 1351 lines of code zeta23/Zeta23/XiPrime/Hardy/EFExpansion.lean x: 1 # contributors y: 650 lines of code zeta23/Zeta23/XiPrime/ZeroCount/Generic.lean x: 1 # contributors y: 556 lines of code zeta23/Zeta23/ZeroSide.lean x: 1 # contributors y: 830 lines of code
3474.0
lines of code
  min: 6.0
  average: 238.52
  25th percentile: 94.0
  median: 170.0
  75th percentile: 306.5
  max: 3474.0
0 2.0
# contributors
min: 1.0 | average: 1.03 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 2.0

Number of Changes vs. Line Churn: 1160 points

.github/scripts/comparator-check.sh x: 2 # changes y: 274 line churn .github/workflows/lean-projects.yml x: 2 # changes y: 571 line churn 3sum-apsp/.gitignore x: 1 # changes y: 4 line churn 3sum-apsp/Challenge/EndStatement.lean x: 1 # changes y: 82 line churn 3sum-apsp/Challenge/PaperStatements.lean x: 1 # changes y: 266 line churn 3sum-apsp/EndStatement.lean x: 1 # changes y: 139 line churn 3sum-apsp/LICENSE x: 1 # changes y: 201 line churn 3sum-apsp/PaperStatements.lean x: 1 # changes y: 4194 line churn 3sum-apsp/README.md x: 1 # changes y: 164 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 # changes y: 362 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 # changes y: 335 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Dispatcher.lean x: 1 # changes y: 96 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 # changes y: 259 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 # changes y: 479 line churn 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 # changes y: 390 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/CountSort.lean x: 1 # changes y: 500 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/MergeSort.lean x: 1 # changes y: 221 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 # changes y: 422 line churn 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 # changes y: 58 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 # changes y: 568 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 # changes y: 755 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 # changes y: 648 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 # changes y: 316 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 # changes y: 705 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 # changes y: 707 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 # changes y: 543 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 # changes y: 645 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 # changes y: 456 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 # changes y: 819 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 # changes y: 783 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/GraphH/Fill.lean x: 1 # changes y: 612 line churn 3sum-apsp/docs/FILES.md x: 1 # changes y: 844 line churn README.md x: 8 # changes y: 413 line churn .github/workflows/zeta23-ci.yml x: 2 # changes y: 439 line churn zeta23/formalization.yaml x: 1 # changes y: 944 line churn zeta23/comparator/Challenge.lean x: 1 # changes y: 924 line churn AUDIT.md x: 6 # changes y: 820 line churn Zeta23.lean x: 3 # changes y: 44 line churn Zeta23/Analytic/RectangleLogDeriv.lean x: 2 # changes y: 1120 line churn Zeta23/Assembly.lean x: 2 # changes y: 3526 line churn Zeta23/Chebyshev.lean x: 2 # changes y: 2968 line churn Zeta23/Defs.lean x: 2 # changes y: 688 line churn Zeta23/ExplicitFormula.lean x: 2 # changes y: 1522 line churn Zeta23/Final.lean x: 2 # changes y: 850 line churn Zeta23/FinalMult.lean x: 2 # changes y: 788 line churn Zeta23/FromPNTPlus/Fourier.lean x: 2 # changes y: 408 line churn Zeta23/FromPNTPlus/MediumPNT.lean x: 2 # changes y: 7466 line churn Zeta23/FromPNTPlus/MellinCalculus.lean x: 1 # changes y: 2096 line churn Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 1 # changes y: 2306 line churn Zeta23/FromPNTPlus/StrongPNTPrefix.lean x: 2 # changes y: 1012 line churn Zeta23/FromPNTPlus/ZetaBounds.lean x: 1 # changes y: 6120 line churn Zeta23/GammaFacts/IntMu.lean x: 1 # changes y: 1048 line churn Zeta23/GammaFacts/StirlingVert.lean x: 1 # changes y: 1284 line churn Zeta23/LinAlg/PosIndex.lean x: 2 # changes y: 264 line churn Zeta23/LinAlg/RankTrace.lean x: 2 # changes y: 544 line churn Zeta23/LinAlg/Sylvester.lean x: 2 # changes y: 628 line churn Zeta23/LinAlg/Weyl.lean x: 2 # changes y: 298 line churn Zeta23/MV/Spacing.lean x: 2 # changes y: 1104 line churn Zeta23/PairCeiling/Bridge.lean x: 2 # changes y: 892 line churn Zeta23/PairCeiling/LawN256.lean x: 2 # changes y: 1164 line churn Zeta23/PairCeiling/NumericCert.lean x: 2 # changes y: 1304 line churn Zeta23/PairCeiling/RowCert.lean x: 2 # changes y: 668 line churn Zeta23/PairCeiling/Signed.lean x: 2 # changes y: 468 line churn Zeta23/PairCeiling/Stability.lean x: 2 # changes y: 1332 line churn Zeta23/PiFacts.lean x: 1 # changes y: 854 line churn Zeta23/Poisson/PaperFT.lean x: 2 # changes y: 354 line churn Zeta23/PrimeSideA/Basic.lean x: 2 # changes y: 2866 line churn Zeta23/PrimeSideA/CrossMuP.lean x: 2 # changes y: 336 line churn Zeta23/PrimeSideA/CrossMuPCore.lean x: 2 # changes y: 974 line churn Zeta23/PrimeSideA/EndsCore.lean x: 2 # changes y: 1456 line churn Zeta23/PrimeSideA/EndsE1.lean x: 2 # changes y: 1842 line churn Zeta23/PrimeSideA/EndsE2.lean x: 2 # changes y: 2080 line churn Zeta23/PrimeSideA/EndsNu.lean x: 2 # changes y: 2224 line churn Zeta23/PrimeSideA/MuMu.lean x: 2 # changes y: 608 line churn Zeta23/PrimeSideB.lean x: 2 # changes y: 1726 line churn Zeta23/RvM/MainTerm.lean x: 2 # changes y: 1218 line churn Zeta23/Tail.lean x: 1 # changes y: 1382 line churn Zeta23/Tail/Count.lean x: 1 # changes y: 998 line churn Zeta23/Taper/Decay.lean x: 2 # changes y: 2370 line churn Zeta23/Taper/Fourier.lean x: 2 # changes y: 1062 line churn Zeta23/Taper/Gevrey.lean x: 2 # changes y: 1752 line churn Zeta23/Taper/GevreyPhi.lean x: 2 # changes y: 108 line churn Zeta23/Taper/GevreyRamps.lean x: 2 # changes y: 1048 line churn Zeta23/Taper/Norms.lean x: 2 # changes y: 1274 line churn Zeta23/ThmD/Concrete.lean x: 2 # changes y: 496 line churn Zeta23/ThmD/Limit.lean x: 2 # changes y: 738 line churn Zeta23/ThmD/PsiC.lean x: 2 # changes y: 1190 line churn Zeta23/ThmD/Window.lean x: 2 # changes y: 3624 line churn Zeta23/ThmE/AssemblyQ.lean x: 1 # changes y: 1118 line churn Zeta23/ThmE/IntMuChi.lean x: 2 # changes y: 2576 line churn Zeta23/ThmE/MainTermChi.lean x: 2 # changes y: 1892 line churn Zeta23/ThmE/PPChi.lean x: 2 # changes y: 2350 line churn Zeta23/ThmE/ReZeroCountChi.lean x: 2 # changes y: 966 line churn Zeta23/WeilEF/Effective.lean x: 2 # changes y: 3752 line churn Zeta23/WeilEF/FullLineAssembly.lean x: 2 # changes y: 196 line churn Zeta23/WeilEF/Landau.lean x: 2 # changes y: 1498 line churn Zeta23/WeilEF/ZeroSummability.lean x: 2 # changes y: 714 line churn Zeta23/XiPrime/Certificate/D1.lean x: 2 # changes y: 1364 line churn Zeta23/XiPrime/Coeff/DiagLaw.lean x: 2 # changes y: 1812 line churn Zeta23/XiPrime/Coeff/LT.lean x: 2 # changes y: 168 line churn Zeta23/XiPrime/Coeff/MainTerm/Squarefree.lean x: 2 # changes y: 940 line churn Zeta23/XiPrime/Coeff/NonSquarefree.lean x: 2 # changes y: 2260 line churn Zeta23/XiPrime/Coeff/ReexpansionW.lean x: 2 # changes y: 228 line churn Zeta23/XiPrime/Coeff/Upper.lean x: 2 # changes y: 1432 line churn Zeta23/XiPrime/ExplicitFormula/Contour.lean x: 2 # changes y: 520 line churn Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 2 # changes y: 4644 line churn Zeta23/XiPrime/ExplicitFormula/LitCorr.lean x: 2 # changes y: 1396 line churn Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 2 # changes y: 4544 line churn Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 2 # changes y: 5636 line churn Zeta23/XiPrime/Final.lean x: 2 # changes y: 2410 line churn Zeta23/XiPrime/Hardy/EFContour/Limit.lean x: 2 # changes y: 872 line churn Zeta23/XiPrime/Hardy/EFExpansion.lean x: 2 # changes y: 2908 line churn Zeta23/XiPrime/Hardy/EFMain.lean x: 2 # changes y: 1692 line churn Zeta23/XiPrime/PrimeSide/Traces.lean x: 2 # changes y: 2320 line churn Zeta23/XiPrime/QuarticWindow.lean x: 2 # changes y: 88 line churn Zeta23/XiPrime/QuarticWindow/ModWindow.lean x: 2 # changes y: 2012 line churn Zeta23/XiPrime/QuarticWindow/Moments.lean x: 2 # changes y: 2148 line churn Zeta23/XiPrime/Statement.lean x: 2 # changes y: 1592 line churn Zeta23/XiPrime/Transfer.lean x: 2 # changes y: 4148 line churn Zeta23/XiPrime/Window.lean x: 2 # changes y: 1652 line churn Zeta23/XiPrime/ZeroCount/Generic.lean x: 2 # changes y: 2288 line churn comparator/Challenge.lean x: 3 # changes y: 884 line churn comparator/Challenge/XiPrime.lean x: 4 # changes y: 428 line churn comparator/ChallengeDeps.lean x: 3 # changes y: 268 line churn comparator/PrintAxioms.lean x: 3 # changes y: 110 line churn comparator/PrintAxioms/XiPrime.lean x: 2 # changes y: 52 line churn comparator/README.md x: 5 # changes y: 280 line churn comparator/Solution.lean x: 3 # changes y: 512 line churn lean-toolchain x: 2 # changes y: 6 line churn zeta23/Zeta23/Assembly.lean x: 1 # changes y: 3266 line churn zeta23/Zeta23/Chebyshev.lean x: 1 # changes y: 2422 line churn zeta23/Zeta23/ExplicitFormula.lean x: 1 # changes y: 1468 line churn zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 1 # changes y: 7462 line churn zeta23/Zeta23/MV/Spacing.lean x: 1 # changes y: 1088 line churn zeta23/Zeta23/PrimeSideA/Basic.lean x: 1 # changes y: 2770 line churn zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 1 # changes y: 1802 line churn zeta23/Zeta23/PrimeSideA/EndsE2.lean x: 1 # changes y: 904 line churn zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 1 # changes y: 1642 line churn zeta23/Zeta23/PrimeSideB.lean x: 1 # changes y: 1652 line churn zeta23/Zeta23/PrimeSideB/PPKernel.lean x: 1 # changes y: 1428 line churn zeta23/Zeta23/Taper/Decay.lean x: 1 # changes y: 2008 line churn zeta23/Zeta23/Taper/Norms.lean x: 1 # changes y: 1250 line churn zeta23/Zeta23/ThmD/Functional.lean x: 1 # changes y: 1010 line churn zeta23/Zeta23/ThmD/Traces.lean x: 1 # changes y: 1334 line churn zeta23/Zeta23/ThmD/Window.lean x: 1 # changes y: 3584 line churn zeta23/Zeta23/ThmE/FullLineChiProof.lean x: 1 # changes y: 1302 line churn zeta23/Zeta23/ThmE/MainTermChi.lean x: 1 # changes y: 1082 line churn zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 1 # changes y: 2878 line churn zeta23/Zeta23/WeilEF/Effective.lean x: 1 # changes y: 1876 line churn zeta23/Zeta23/WeilEF/VerticalLine.lean x: 1 # changes y: 1576 line churn zeta23/Zeta23/XiPrime/Assembly.lean x: 1 # changes y: 1178 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 1 # changes y: 2272 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 1 # changes y: 2818 line churn zeta23/Zeta23/XiPrime/PrimeSide/Traces.lean x: 1 # changes y: 1160 line churn zeta23/Zeta23/XiPrime/Transfer.lean x: 1 # changes y: 2074 line churn zeta23/Zeta23/ZeroSide.lean x: 1 # changes y: 1994 line churn
7466.0
line churn
  min: 1.0
  average: 531.2
  25th percentile: 148.0
  median: 316.0
  75th percentile: 644.75
  max: 7466.0
0 8.0
# changes
min: 1.0 | average: 1.22 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 8.0

Number of Contributors vs. Line Churn: 769 points

3sum-apsp/Challenge/EndStatement.lean x: 1 # contributors y: 82 line churn 3sum-apsp/Challenge/PaperStatements.lean x: 1 # contributors y: 266 line churn 3sum-apsp/EndStatement.lean x: 1 # contributors y: 139 line churn 3sum-apsp/PaperStatements.lean x: 1 # contributors y: 4194 line churn 3sum-apsp/Solution/EndStatement.lean x: 1 # contributors y: 9 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 # contributors y: 362 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 # contributors y: 172 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 # contributors y: 203 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 # contributors y: 335 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Dispatcher.lean x: 1 # contributors y: 96 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 # contributors y: 259 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 # contributors y: 479 line churn 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 # contributors y: 390 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/CountSort.lean x: 1 # contributors y: 500 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/MergeSort.lean x: 1 # contributors y: 221 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 # contributors y: 422 line churn 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 # contributors y: 58 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 # contributors y: 568 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 # contributors y: 755 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 # contributors y: 648 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 # contributors y: 316 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 # contributors y: 705 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 # contributors y: 707 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 # contributors y: 543 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 # contributors y: 645 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 # contributors y: 456 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 # contributors y: 819 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 # contributors y: 783 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/GraphH/Fill.lean x: 1 # contributors y: 612 line churn zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 2 # contributors y: 414 line churn zeta23/Zeta23/LinAlg/Inertia.lean x: 2 # contributors y: 282 line churn zeta23/Zeta23/LinAlg/PosIndex.lean x: 2 # contributors y: 260 line churn zeta23/Zeta23/LinAlg/RankTrace.lean x: 2 # contributors y: 540 line churn zeta23/Zeta23/LinAlg/Sylvester.lean x: 2 # contributors y: 624 line churn zeta23/formalization.yaml x: 2 # contributors y: 944 line churn .github/dependabot.yml x: 2 # contributors y: 12 line churn zeta23/Challenge.lean x: 2 # contributors y: 462 line churn zeta23/Challenge/XiPrime.lean x: 2 # contributors y: 212 line churn zeta23/ChallengeDeps/XiPrime.lean x: 2 # contributors y: 88 line churn zeta23/Solution/XiPrime.lean x: 2 # contributors y: 104 line churn zeta23/scripts/PrintAxioms/PairCeiling.lean x: 2 # contributors y: 42 line churn zeta23/scripts/validate-formalization.rb x: 2 # contributors y: 352 line churn zeta23/Zeta23/Assembly.lean x: 1 # contributors y: 3266 line churn zeta23/Zeta23/Chebyshev.lean x: 1 # contributors y: 2422 line churn zeta23/Zeta23/ExplicitFormula.lean x: 1 # contributors y: 1468 line churn zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 1 # contributors y: 7462 line churn zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 1 # contributors y: 2096 line churn zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 1 # contributors y: 2306 line churn zeta23/Zeta23/FromPNTPlus/StrongPNTPrefix.lean x: 1 # contributors y: 964 line churn zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 1 # contributors y: 6120 line churn zeta23/Zeta23/GammaFacts/IntMu.lean x: 1 # contributors y: 1048 line churn zeta23/Zeta23/GammaFacts/Mu.lean x: 1 # contributors y: 928 line churn zeta23/Zeta23/GammaFacts/Series.lean x: 1 # contributors y: 998 line churn zeta23/Zeta23/GammaFacts/StirlingVert.lean x: 1 # contributors y: 1284 line churn zeta23/Zeta23/MV/Spacing.lean x: 1 # contributors y: 1088 line churn zeta23/Zeta23/PiFacts.lean x: 1 # contributors y: 854 line churn zeta23/Zeta23/PrimeSideA/Basic.lean x: 1 # contributors y: 2770 line churn zeta23/Zeta23/PrimeSideA/EndsCore.lean x: 1 # contributors y: 1396 line churn zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 1 # contributors y: 1802 line churn zeta23/Zeta23/PrimeSideA/EndsE2.lean x: 1 # contributors y: 904 line churn zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 1 # contributors y: 1642 line churn zeta23/Zeta23/PrimeSideB.lean x: 1 # contributors y: 1652 line churn zeta23/Zeta23/PrimeSideB/PPKernel.lean x: 1 # contributors y: 1428 line churn zeta23/Zeta23/RvM/Backlund.lean x: 1 # contributors y: 832 line churn zeta23/Zeta23/Taper/Decay.lean x: 1 # contributors y: 2008 line churn zeta23/Zeta23/Taper/Norms.lean x: 1 # contributors y: 1250 line churn zeta23/Zeta23/ThmD/Functional.lean x: 1 # contributors y: 1010 line churn zeta23/Zeta23/ThmD/PsiC.lean x: 1 # contributors y: 1146 line churn zeta23/Zeta23/ThmD/Traces.lean x: 1 # contributors y: 1334 line churn zeta23/Zeta23/ThmD/Window.lean x: 1 # contributors y: 3584 line churn zeta23/Zeta23/ThmE/AssemblyQ.lean x: 1 # contributors y: 1118 line churn zeta23/Zeta23/ThmE/FullLineChiProof.lean x: 1 # contributors y: 1302 line churn zeta23/Zeta23/ThmE/MainTermChi.lean x: 1 # contributors y: 1082 line churn zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 1 # contributors y: 2878 line churn zeta23/Zeta23/WeilEF/Effective.lean x: 1 # contributors y: 1876 line churn zeta23/Zeta23/WeilEF/VerticalLine.lean x: 1 # contributors y: 1576 line churn zeta23/Zeta23/XiPrime/Assembly.lean x: 1 # contributors y: 1178 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 1 # contributors y: 2322 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 1 # contributors y: 2272 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 1 # contributors y: 2818 line churn zeta23/Zeta23/XiPrime/Transfer.lean x: 1 # contributors y: 2074 line churn zeta23/Zeta23/ZeroSide.lean x: 1 # contributors y: 1994 line churn
7462.0
line churn
  min: 9.0
  average: 403.97
  25th percentile: 132.5
  median: 256.0
  75th percentile: 475.5
  max: 7462.0
0 2.0
# contributors
min: 1.0 | average: 1.03 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 2.0

File Size vs. Line Churn: 769 points

3sum-apsp/Challenge/EndStatement.lean x: 71 lines of code y: 82 line churn 3sum-apsp/Challenge/PaperStatements.lean x: 218 lines of code y: 266 line churn 3sum-apsp/EndStatement.lean x: 115 lines of code y: 139 line churn 3sum-apsp/PaperStatements.lean x: 3474 lines of code y: 4194 line churn 3sum-apsp/Solution/EndStatement.lean x: 8 lines of code y: 9 line churn 3sum-apsp/ThreeSumApsp.lean x: 20 lines of code y: 23 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes.lean x: 16 lines of code y: 19 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 57 lines of code y: 67 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 307 lines of code y: 362 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 150 lines of code y: 172 line churn 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 177 lines of code y: 203 line churn 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 104 lines of code y: 129 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 134 lines of code y: 151 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 273 lines of code y: 335 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Conditions.lean x: 127 lines of code y: 148 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Dispatcher.lean x: 79 lines of code y: 96 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 202 lines of code y: 259 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 427 lines of code y: 479 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/StartUp.lean x: 218 lines of code y: 255 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 294 lines of code y: 364 line churn 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 229 lines of code y: 265 line churn 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 338 lines of code y: 390 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/ArrayAt.lean x: 110 lines of code y: 142 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Copy.lean x: 66 lines of code y: 87 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/CountSort.lean x: 433 lines of code y: 500 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 240 lines of code y: 268 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Logs.lean x: 235 lines of code y: 273 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Merge.lean x: 166 lines of code y: 198 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/MergeSort.lean x: 195 lines of code y: 221 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 95 lines of code y: 115 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 159 lines of code y: 180 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 186 lines of code y: 235 line churn 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 371 lines of code y: 422 line churn 3sum-apsp/ThreeSumApsp/Lang/PolyBounded.lean x: 114 lines of code y: 147 line churn 3sum-apsp/ThreeSumApsp/Lang/Regions.lean x: 162 lines of code y: 210 line churn 3sum-apsp/ThreeSumApsp/Lang/RowMajor.lean x: 84 lines of code y: 103 line churn 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 316 lines of code y: 365 line churn 3sum-apsp/ThreeSumApsp/Lang/Syntax.lean x: 138 lines of code y: 164 line churn 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 346 lines of code y: 393 line churn 3sum-apsp/ThreeSumApsp/Lang/TopProcedure.lean x: 329 lines of code y: 368 line churn 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 50 lines of code y: 58 line churn 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 33 lines of code y: 43 line churn 3sum-apsp/ThreeSumApsp/Machine/Steps.lean x: 329 lines of code y: 419 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/AllInstances/Program.lean x: 25 lines of code y: 34 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/AllInstances/RegimeTest.lean x: 322 lines of code y: 358 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/AllInstances/Solver.lean x: 340 lines of code y: 372 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 502 lines of code y: 568 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/AllBands.lean x: 264 lines of code y: 293 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 669 lines of code y: 755 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArrayFacts.lean x: 175 lines of code y: 213 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/Step.lean x: 181 lines of code y: 216 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Instance.lean x: 140 lines of code y: 179 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/LibraryContracts.lean x: 56 lines of code y: 70 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Program.lean x: 75 lines of code y: 90 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Pruned/AllTiles.lean x: 433 lines of code y: 493 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Pruned/Recursion.lean x: 352 lines of code y: 391 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Pruned/SliceFacts.lean x: 302 lines of code y: 351 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Pruned/Union.lean x: 246 lines of code y: 282 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 601 lines of code y: 648 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Solver.lean x: 184 lines of code y: 205 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 286 lines of code y: 316 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 633 lines of code y: 705 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Sort.lean x: 309 lines of code y: 355 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/SortedFacts.lean x: 331 lines of code y: 384 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 461 lines of code y: 507 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ChoosePrime.lean x: 333 lines of code y: 376 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Count.lean x: 203 lines of code y: 231 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/CountPrime.lean x: 426 lines of code y: 496 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/RingOps.lean x: 281 lines of code y: 327 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/SizeTable.lean x: 94 lines of code y: 112 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 615 lines of code y: 707 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/StrassenFacts.lean x: 265 lines of code y: 302 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/StrassenTime.lean x: 49 lines of code y: 59 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 481 lines of code y: 543 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Arrays.lean x: 320 lines of code y: 346 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceCount.lean x: 40 lines of code y: 48 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 402 lines of code y: 471 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 580 lines of code y: 645 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/Classes.lean x: 452 lines of code y: 513 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 536 lines of code y: 622 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Parameters/Primes.lean x: 225 lines of code y: 260 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/TimeBound/Terms.lean x: 426 lines of code y: 524 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/TimeBound/Total.lean x: 212 lines of code y: 243 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Witnesses/ScanPairs.lean x: 199 lines of code y: 237 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 412 lines of code y: 456 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Buckets.lean x: 608 lines of code y: 681 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 440 lines of code y: 519 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Distinct.lean x: 362 lines of code y: 412 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 565 lines of code y: 632 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 740 lines of code y: 819 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeMemory.lean x: 148 lines of code y: 188 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 620 lines of code y: 686 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Prepare.lean x: 407 lines of code y: 446 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Reduction.lean x: 574 lines of code y: 654 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Round.lean x: 228 lines of code y: 253 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Time.lean x: 67 lines of code y: 89 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/TimeBound.lean x: 156 lines of code y: 195 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/Convolution/Fill.lean x: 342 lines of code y: 399 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 255 lines of code y: 284 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Passes.lean x: 381 lines of code y: 428 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 704 lines of code y: 783 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/BitSearch.lean x: 420 lines of code y: 487 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/ChoosingParameters/InnerProduct.lean x: 123 lines of code y: 143 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/ChoosingParameters/Limits.lean x: 271 lines of code y: 315 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/ChoosingParameters/Offline.lean x: 207 lines of code y: 232 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/Corollary26/Regime.lean x: 123 lines of code y: 151 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/Contracts.lean x: 499 lines of code y: 577 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/Insert.lean x: 366 lines of code y: 420 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 390 lines of code y: 449 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/Tile.lean x: 189 lines of code y: 218 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/GraphH/Fill.lean x: 534 lines of code y: 612 line churn 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 714 lines of code y: 807 line churn 3sum-apsp/ThreeSumApsp/RunningTimes/FromClaims.lean x: 102 lines of code y: 116 line churn 3sum-apsp/ThreeSumApsp/RunningTimes/Sec2/Theorem5.lean x: 27 lines of code y: 35 line churn 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 515 lines of code y: 561 line churn 3sum-apsp/ThreeSumApsp/RunningTimes/Sec5/Corollary40/UMvHintedTimes.lean x: 278 lines of code y: 303 line churn 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 525 lines of code y: 591 line churn 3sum-apsp/ThreeSumApsp/Sec2/Levels.lean x: 288 lines of code y: 347 line churn 3sum-apsp/ThreeSumApsp/Sec2/Theorem5.lean x: 172 lines of code y: 193 line churn 3sum-apsp/ThreeSumApsp/Sec3/MatrixLanguage.lean x: 292 lines of code y: 335 line churn 3sum-apsp/ThreeSumApsp/Sec4.lean x: 26 lines of code y: 29 line churn 3sum-apsp/ThreeSumApsp/Sec4/Boxes.lean x: 351 lines of code y: 415 line churn 3sum-apsp/ThreeSumApsp/Sec4/Corollary31.lean x: 427 lines of code y: 469 line churn 3sum-apsp/ThreeSumApsp/Sec4/Lemma27_28.lean x: 491 lines of code y: 558 line churn 3sum-apsp/ThreeSumApsp/Sec5/Corollary40/RoundingThreshold.lean x: 76 lines of code y: 86 line churn 3sum-apsp/ThreeSumApsp/Sec5/Lemma37.lean x: 393 lines of code y: 439 line churn 3sum-apsp/ThreeSumApsp/Spec/Sec4/Theorem30/StarBoxes.lean x: 152 lines of code y: 176 line churn 3sum-apsp/ThreeSumApsp/Spec/Sec4/Theorem30/TileTries.lean x: 410 lines of code y: 499 line churn 3sum-apsp/ThreeSumApsp/Spec/Sec4/Theorem30/Trie.lean x: 464 lines of code y: 532 line churn 3sum-apsp/ThreeSumApsp/Statements/Agreement.lean x: 235 lines of code y: 263 line churn 3sum-apsp/ThreeSumApsp/Util/Asymptotics/Dominated.lean x: 250 lines of code y: 300 line churn 3sum-apsp/ThreeSumApsp/Util/Asymptotics/Scale.lean x: 260 lines of code y: 316 line churn 3sum-apsp/ThreeSumApsp/Util/CountingSort.lean x: 100 lines of code y: 130 line churn 3sum-apsp/ThreeSumApsp/Util/PrimesInWindow.lean x: 308 lines of code y: 342 line churn 3sum-apsp/scripts/index.py x: 383 lines of code y: 516 line churn zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 167 lines of code y: 414 line churn zeta23/Zeta23/LinAlg/Inertia.lean x: 125 lines of code y: 282 line churn zeta23/Zeta23/LinAlg/PosIndex.lean x: 103 lines of code y: 260 line churn zeta23/Zeta23/LinAlg/RankTrace.lean x: 239 lines of code y: 540 line churn zeta23/Zeta23/LinAlg/Sylvester.lean x: 282 lines of code y: 624 line churn zeta23/Zeta23/LinAlg/VonNeumann.lean x: 181 lines of code y: 414 line churn zeta23/formalization.yaml x: 228 lines of code y: 944 line churn .github/dependabot.yml x: 6 lines of code y: 12 line churn zeta23/Challenge.lean x: 188 lines of code y: 462 line churn zeta23/Challenge/XiPrime.lean x: 86 lines of code y: 212 line churn zeta23/ChallengeDeps/XiPrime.lean x: 32 lines of code y: 88 line churn zeta23/Solution.lean x: 119 lines of code y: 284 line churn zeta23/Solution/XiPrime.lean x: 45 lines of code y: 104 line churn zeta23/lakefile.toml x: 25 lines of code y: 90 line churn zeta23/scripts/PrintAxioms.lean x: 30 lines of code y: 62 line churn zeta23/scripts/validate-formalization.rb x: 157 lines of code y: 352 line churn zeta23/Zeta23.lean x: 18 lines of code y: 36 line churn zeta23/Zeta23/Analytic/RectangleLogDeriv.lean x: 373 lines of code y: 772 line churn zeta23/Zeta23/Analytic/Stirling.lean x: 272 lines of code y: 560 line churn zeta23/Zeta23/Assembly.lean x: 1451 lines of code y: 3266 line churn zeta23/Zeta23/Assembly/Certificate.lean x: 94 lines of code y: 204 line churn zeta23/Zeta23/Assembly/CertificateC3.lean x: 95 lines of code y: 202 line churn zeta23/Zeta23/Assembly/Inputs.lean x: 59 lines of code y: 138 line churn zeta23/Zeta23/Assembly/SeamMult.lean x: 83 lines of code y: 184 line churn zeta23/Zeta23/Chebyshev.lean x: 1144 lines of code y: 2422 line churn zeta23/Zeta23/Defs.lean x: 252 lines of code y: 678 line churn zeta23/Zeta23/Defs/Counting.lean x: 53 lines of code y: 132 line churn zeta23/Zeta23/Defs/LeafIntegrals.lean x: 196 lines of code y: 412 line churn zeta23/Zeta23/ExplicitFormula.lean x: 662 lines of code y: 1468 line churn zeta23/Zeta23/ExplicitFormula/Bridge.lean x: 190 lines of code y: 408 line churn zeta23/Zeta23/Final.lean x: 299 lines of code y: 748 line churn zeta23/Zeta23/FinalMult.lean x: 345 lines of code y: 756 line churn zeta23/Zeta23/FromPNTPlus/Auxiliary.lean x: 73 lines of code y: 176 line churn zeta23/Zeta23/FromPNTPlus/EulerMaclaurin.lean x: 80 lines of code y: 184 line churn zeta23/Zeta23/FromPNTPlus/Fourier.lean x: 178 lines of code y: 398 line churn zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 3387 lines of code y: 7462 line churn zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 974 lines of code y: 2096 line churn zeta23/Zeta23/FromPNTPlus/Rectangle.lean x: 232 lines of code y: 560 line churn zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 1062 lines of code y: 2306 line churn zeta23/Zeta23/FromPNTPlus/SmoothExistence.lean x: 98 lines of code y: 206 line churn zeta23/Zeta23/FromPNTPlus/StrongPNTPrefix.lean x: 459 lines of code y: 964 line churn zeta23/Zeta23/FromPNTPlus/Tactic/AdditiveCombination.lean x: 172 lines of code y: 392 line churn zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 2788 lines of code y: 6120 line churn zeta23/Zeta23/GammaFacts.lean x: 109 lines of code y: 242 line churn zeta23/Zeta23/GammaFacts/IntMu.lean x: 515 lines of code y: 1048 line churn zeta23/Zeta23/GammaFacts/Mu.lean x: 444 lines of code y: 928 line churn zeta23/Zeta23/GammaFacts/Series.lean x: 478 lines of code y: 998 line churn zeta23/Zeta23/GammaFacts/StirlingVert.lean x: 581 lines of code y: 1284 line churn zeta23/Zeta23/Hypotheses.lean x: 140 lines of code y: 318 line churn zeta23/Zeta23/Hypotheses/GzGp.lean x: 130 lines of code y: 296 line churn zeta23/Zeta23/MV.lean x: 212 lines of code y: 480 line churn zeta23/Zeta23/MV/Duality.lean x: 182 lines of code y: 406 line churn zeta23/Zeta23/MV/Eigen.lean x: 132 lines of code y: 282 line churn zeta23/Zeta23/MV/Quadratic.lean x: 202 lines of code y: 426 line churn zeta23/Zeta23/MV/Spacing.lean x: 515 lines of code y: 1088 line churn zeta23/Zeta23/Main.lean x: 267 lines of code y: 634 line churn zeta23/Zeta23/PairCeiling/Bridge.lean x: 206 lines of code y: 446 line churn zeta23/Zeta23/PairCeiling/CeilingLaw256.lean x: 64 lines of code y: 144 line churn zeta23/Zeta23/PairCeiling/LawN256.lean x: 287 lines of code y: 582 line churn zeta23/Zeta23/PairCeiling/NumericCert.lean x: 286 lines of code y: 652 line churn zeta23/Zeta23/PairCeiling/RowCert.lean x: 150 lines of code y: 334 line churn zeta23/Zeta23/PairCeiling/Signed.lean x: 104 lines of code y: 234 line churn zeta23/Zeta23/PairCeiling/Stability.lean x: 295 lines of code y: 666 line churn zeta23/Zeta23/PiFacts.lean x: 408 lines of code y: 854 line churn zeta23/Zeta23/Poisson.lean x: 364 lines of code y: 808 line churn zeta23/Zeta23/Poisson/PaperFT.lean x: 140 lines of code y: 324 line churn zeta23/Zeta23/PrimeSideA.lean x: 456 lines of code y: 962 line churn zeta23/Zeta23/PrimeSideA/Basic.lean x: 1276 lines of code y: 2770 line churn zeta23/Zeta23/PrimeSideA/CrossMuPCore.lean x: 262 lines of code y: 562 line churn zeta23/Zeta23/PrimeSideA/EndsCore.lean x: 604 lines of code y: 1396 line churn zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 851 lines of code y: 1802 line churn zeta23/Zeta23/PrimeSideA/EndsE2.lean x: 431 lines of code y: 904 line churn zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 768 lines of code y: 1642 line churn zeta23/Zeta23/PrimeSideA/EndsWeighted.lean x: 218 lines of code y: 488 line churn zeta23/Zeta23/PrimeSideB.lean x: 746 lines of code y: 1652 line churn zeta23/Zeta23/PrimeSideB/PP.lean x: 440 lines of code y: 962 line churn zeta23/Zeta23/PrimeSideB/PPKernel.lean x: 642 lines of code y: 1428 line churn zeta23/Zeta23/PrimeSideB/PPOffDiag.lean x: 166 lines of code y: 346 line churn zeta23/Zeta23/PrimeSideB/Traces.lean x: 193 lines of code y: 418 line churn zeta23/Zeta23/RvM/Backlund.lean x: 383 lines of code y: 832 line churn zeta23/Zeta23/RvM/LocalCount.lean x: 278 lines of code y: 596 line churn zeta23/Zeta23/RvM/MainTerm.lean x: 468 lines of code y: 972 line churn zeta23/Zeta23/RvM/NcountWindow.lean x: 50 lines of code y: 118 line churn zeta23/Zeta23/RvM/ReZeroCount.lean x: 352 lines of code y: 728 line churn zeta23/Zeta23/Statement.lean x: 155 lines of code y: 380 line churn zeta23/Zeta23/Statement/SeamClosed.lean x: 41 lines of code y: 100 line churn zeta23/Zeta23/Tail.lean x: 615 lines of code y: 1382 line churn zeta23/Zeta23/Tail/Basic.lean x: 61 lines of code y: 150 line churn zeta23/Zeta23/Tail/Count.lean x: 472 lines of code y: 998 line churn zeta23/Zeta23/Tail/RankOne.lean x: 160 lines of code y: 356 line churn zeta23/Zeta23/Taper.lean x: 153 lines of code y: 344 line churn zeta23/Zeta23/Taper/Basic.lean x: 143 lines of code y: 372 line churn zeta23/Zeta23/Taper/Decay.lean x: 908 lines of code y: 2008 line churn zeta23/Zeta23/Taper/Fourier.lean x: 408 lines of code y: 960 line churn zeta23/Zeta23/Taper/Gevrey.lean x: 381 lines of code y: 876 line churn zeta23/Zeta23/Taper/GevreyRamps.lean x: 237 lines of code y: 524 line churn zeta23/Zeta23/Taper/Norms.lean x: 577 lines of code y: 1250 line churn zeta23/Zeta23/ThmD/AssemblyD.lean x: 66 lines of code y: 158 line churn zeta23/Zeta23/ThmD/Concrete.lean x: 231 lines of code y: 488 line churn zeta23/Zeta23/ThmD/Endgame.lean x: 414 lines of code y: 860 line churn zeta23/Zeta23/ThmD/Final.lean x: 132 lines of code y: 308 line churn zeta23/Zeta23/ThmD/Functional.lean x: 464 lines of code y: 1010 line churn zeta23/Zeta23/ThmD/PP.lean x: 344 lines of code y: 700 line churn zeta23/Zeta23/ThmD/ParamsD.lean x: 75 lines of code y: 194 line churn zeta23/Zeta23/ThmD/PsiC.lean x: 535 lines of code y: 1146 line churn zeta23/Zeta23/ThmD/Traces.lean x: 640 lines of code y: 1334 line churn zeta23/Zeta23/ThmD/Window.lean x: 1737 lines of code y: 3584 line churn zeta23/Zeta23/ThmD/WindowCore.lean x: 410 lines of code y: 1028 line churn zeta23/Zeta23/ThmDE/Concrete.lean x: 225 lines of code y: 484 line churn zeta23/Zeta23/ThmDE/Traces.lean x: 251 lines of code y: 552 line churn zeta23/Zeta23/ThmE/AssemblyQ.lean x: 515 lines of code y: 1118 line churn zeta23/Zeta23/ThmE/BacklundChi.lean x: 335 lines of code y: 730 line churn zeta23/Zeta23/ThmE/ChebCoprime.lean x: 407 lines of code y: 832 line churn zeta23/Zeta23/ThmE/ContourChi.lean x: 130 lines of code y: 274 line churn zeta23/Zeta23/ThmE/EFLitChi.lean x: 378 lines of code y: 794 line churn zeta23/Zeta23/ThmE/FullLineChi.lean x: 287 lines of code y: 598 line churn zeta23/Zeta23/ThmE/FullLineChiProof.lean x: 613 lines of code y: 1302 line churn zeta23/Zeta23/ThmE/GammaSideChi.lean x: 170 lines of code y: 366 line churn zeta23/Zeta23/ThmE/HorizontalChi.lean x: 153 lines of code y: 320 line churn zeta23/Zeta23/ThmE/LGrowth.lean x: 317 lines of code y: 694 line churn zeta23/Zeta23/ThmE/LocalCountChi.lean x: 244 lines of code y: 512 line churn zeta23/Zeta23/ThmE/Main.lean x: 313 lines of code y: 700 line churn zeta23/Zeta23/ThmE/MainTermChi.lean x: 520 lines of code y: 1082 line churn zeta23/Zeta23/ThmE/MuMuChi.lean x: 305 lines of code y: 640 line churn zeta23/Zeta23/ThmE/Mult.lean x: 322 lines of code y: 690 line churn zeta23/Zeta23/ThmE/PPChi.lean x: 946 lines of code y: 2014 line churn zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 1381 lines of code y: 2878 line churn zeta23/Zeta23/ThmE/ReZeroCountChi.lean x: 318 lines of code y: 668 line churn zeta23/Zeta23/ThmE/SeamL.lean x: 343 lines of code y: 744 line churn zeta23/Zeta23/ThmE/Statement.lean x: 121 lines of code y: 300 line churn zeta23/Zeta23/ThmE/TracesChi.lean x: 437 lines of code y: 940 line churn zeta23/Zeta23/ThmE/VerticalLineChi.lean x: 216 lines of code y: 456 line churn zeta23/Zeta23/WeilEF/Effective.lean x: 909 lines of code y: 1876 line churn zeta23/Zeta23/WeilEF/FullLine.lean x: 392 lines of code y: 852 line churn zeta23/Zeta23/WeilEF/GammaRBracket.lean x: 122 lines of code y: 262 line churn zeta23/Zeta23/WeilEF/Landau.lean x: 641 lines of code y: 1322 line churn zeta23/Zeta23/WeilEF/Main.lean x: 264 lines of code y: 546 line churn zeta23/Zeta23/WeilEF/VerticalLine.lean x: 763 lines of code y: 1576 line churn zeta23/Zeta23/XiPrime/Assembly.lean x: 545 lines of code y: 1178 line churn zeta23/Zeta23/XiPrime/Certificate/D1.lean x: 292 lines of code y: 682 line churn zeta23/Zeta23/XiPrime/Coeff/Abel.lean x: 168 lines of code y: 366 line churn zeta23/Zeta23/XiPrime/Coeff/Basic.lean x: 323 lines of code y: 754 line churn zeta23/Zeta23/XiPrime/Coeff/LSeries.lean x: 292 lines of code y: 660 line churn zeta23/Zeta23/XiPrime/Coeff/MainTerm/Asymp.lean x: 424 lines of code y: 900 line churn zeta23/Zeta23/XiPrime/Coeff/MainTerm/Squarefree.lean x: 210 lines of code y: 470 line churn zeta23/Zeta23/XiPrime/Coeff/NonSquarefree.lean x: 522 lines of code y: 1130 line churn zeta23/Zeta23/XiPrime/Defs.lean x: 187 lines of code y: 496 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 1035 lines of code y: 2322 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 1012 lines of code y: 2272 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/XiEFAssembly.lean x: 266 lines of code y: 570 line churn zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 1351 lines of code y: 2818 line churn zeta23/Zeta23/XiPrime/FamilyHyps.lean x: 256 lines of code y: 564 line churn zeta23/Zeta23/XiPrime/Final.lean x: 516 lines of code y: 1200 line churn zeta23/Zeta23/XiPrime/Hardy/Basic.lean x: 240 lines of code y: 578 line churn zeta23/Zeta23/XiPrime/Hardy/EFBasic.lean x: 297 lines of code y: 680 line churn zeta23/Zeta23/XiPrime/Hardy/EFContour/Analytic.lean x: 209 lines of code y: 510 line churn zeta23/Zeta23/XiPrime/Hardy/EFContour/Poles.lean x: 306 lines of code y: 692 line churn zeta23/Zeta23/XiPrime/Hardy/EFContour/Rectangle.lean x: 400 lines of code y: 904 line churn zeta23/Zeta23/XiPrime/Hardy/EFExpansion.lean x: 650 lines of code y: 1454 line churn zeta23/Zeta23/XiPrime/Hardy/ZFunction.lean x: 317 lines of code y: 742 line churn zeta23/Zeta23/XiPrime/Hardy/ZeroFree.lean x: 527 lines of code y: 1120 line churn zeta23/Zeta23/XiPrime/PrimeSide/Density.lean x: 222 lines of code y: 502 line churn zeta23/Zeta23/XiPrime/PrimeSide/PP.lean x: 605 lines of code y: 1288 line churn zeta23/Zeta23/XiPrime/PrimeSide/Traces.lean x: 528 lines of code y: 1160 line churn zeta23/Zeta23/XiPrime/QuarticWindow/Moments.lean x: 505 lines of code y: 1074 line churn zeta23/Zeta23/XiPrime/QuarticWindow/ZeroSide.lean x: 181 lines of code y: 442 line churn zeta23/Zeta23/XiPrime/Seam.lean x: 369 lines of code y: 862 line churn zeta23/Zeta23/XiPrime/Statement.lean x: 340 lines of code y: 796 line churn zeta23/Zeta23/XiPrime/Transfer.lean x: 982 lines of code y: 2074 line churn zeta23/Zeta23/XiPrime/Transfer/Dependence.lean x: 565 lines of code y: 1202 line churn zeta23/Zeta23/XiPrime/Window.lean x: 363 lines of code y: 826 line churn zeta23/Zeta23/XiPrime/ZeroCount/Generic.lean x: 556 lines of code y: 1144 line churn zeta23/Zeta23/XiPrime/ZeroCount/Y.lean x: 396 lines of code y: 832 line churn zeta23/Zeta23/ZeroSide.lean x: 830 lines of code y: 1994 line churn zeta23/Zeta23/ZeroSide/Final.lean x: 79 lines of code y: 206 line churn zeta23/Zeta23/ZeroSide/RankTraceMult.lean x: 386 lines of code y: 884 line churn zeta23/Zeta23/ZetaReflect.lean x: 307 lines of code y: 658 line churn
7462.0
line churn
  min: 9.0
  average: 403.97
  25th percentile: 132.5
  median: 256.0
  75th percentile: 475.5
  max: 7462.0
0 3474.0
lines of code
min: 6.0 | average: 238.52 | 25th percentile: 94.0 | median: 170.0 | 75th percentile: 306.5 | max: 3474.0