Head version
a93551347dce
a93551347dce924b1db75d40218841bf085a465f
- Toolchain
- leanprover/lean4:v4.32.0
- Revision date
- 22 Jul 2026
- Dependencies
- 13
- Versions
- 9
All packages
AlexKontorovich/PrimeNumberTheoremAnd
PrimeNumberTheoremAnd
Blueprint for the PNT+ Project
Therefore indexed 1,644 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.
External build observation
Exact head commit and toolchain
No Reservoir build observation was found for this exact commit and toolchain. This is not evidence of failure.
Pin this source in lakefile.lean
require PrimeNumberTheoremAnd from git "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git" @ "a93551347dce924b1db75d40218841bf085a465f"
Source declarations
1,644 indexed proofs
Showing 501 to 520 of 1,644 declarations.
theorem
FKS2.floor_row11
Row-11 floor (Buthe) [e^3.5, e^10] via floor_xpow_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row11 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean:414
theorem
FKS2.corollary_24_row11
FKS2 Corollary 24, row 11 (table7 entry (x ↦ x^{-1/100}, Icc 1 3757.6)):
Eπ x ≤ x^{-1/100} whenever log x ∈ [1, 3757.6]. For x > 0 this splits into
the four segments above; for x ≤ 0 (possible since log is even) Eπ x ≤ 0 < x^{-1/100}.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row11 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean:461
theorem
FKS2.floor_row2
Row-2 Buthe floor [e^8, e^43] via floor_xhalf_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row2 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row2.lean:44
theorem
FKS2.corollary_24_row2
FKS2 Corollary 24, row 2 (table7 entry (x ↦ (log x)^{3/2}·x^{-1/2}, Icc 1 65.65)):
Eπ x ≤ (log x)^{3/2}·x^{-1/2} whenever log x ∈ [1, 65.65]. For x > 0 this splits into
the three segments above; for x < 0 (possible since log is even) the exponent
-(1)/2 gives cos((-(1)/2)·π) = cos(-π/2) = 0, so x^{-1/2} = 0 and the RHS is 0,
while Eπ x ≤ 0.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row2 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row2.lean:97
theorem
FKS2.floor_row3
Row-3 Buthe floor [e^9, e^43] via floor_xhalf_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row3 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row3.lean:54
theorem
FKS2.corollary_24_row3
FKS2 Corollary 24, row 3
(table7 entry (x ↦ (1/(8π))·(log x)²·x^{-1/2}, Icc 8 60.8)):
Eπ x ≤ (1/(8π))·(log x)²·x^{-1/2} whenever log x ∈ [8, 60.8]. For x > 0 this
splits into the three segments above; for x < 0 (possible since log is even) the
exponent -(1)/2 gives cos((-(1)/2)·π) = cos(-π/2) = 0, so x^{-1/2} = 0 and the RHS
is 0, while Eπ x ≤ 0.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row3 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row3.lean:112
theorem
FKS2.Table4Ext.Epi_le_evalLhsE_wide
Buthe Eπ-upper-bound as eval FloorButhe.lhsE on the WIDE range [2, e^43]
(vs Epi_le_evalLhsE_low's [2, e^10]): identical reconciliation, but taking the
x ≤ 10^19 hypothesis directly (e^43 ≈ 4.7e18 < 10^19), which extends the Buthe
reread to the full x^{-1/2}-floor range. Curve-independent, so reusable by every
x^{-1/2} row (rows 1–5). Bottoms out at Buthe theorem_2e/2f + li.two_approx.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row4 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean:48
lemma
FKS2.Table4Ext.xhalfCurve_sub_supported
Support of lhsE - xhalfCurveE c twoK for the dyadic slab kernel.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row4 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean:118
theorem
FKS2.floor_row4
Row-4 Buthe floor [e^3, e^43] via floor_xhalf_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row4 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean:203
theorem
FKS2.corollary_24_row4
FKS2 Corollary 24, row 4 (table7 entry (x ↦ (log x)²·x^{-1/2}, Icc 1 70.6)):
Eπ x ≤ (log x)²·x^{-1/2} whenever log x ∈ [1, 70.6]. For x > 0 this splits into
the three segments above; for x < 0 (possible since log is even) the exponent
-(1)/2 gives cos((-(1)/2)·π) = cos(-π/2) = 0, so x^{-1/2} = 0 and the RHS is 0,
while Eπ x ≤ 0.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row4 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean:256
theorem
FKS2.floor_xhalf_row5
Row-5 Buthe floor [e^3, e^43] via floor_xhalf_of_check. (Named floor_xhalf_row5,
not floor_row5, since FKS2.floor_row5 is already taken by Corollary 23's row 5 in the
imported FKS2Cor23.lean base file - unrelated corollary, same row index.)
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row5 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row5.lean:42
theorem
FKS2.corollary_24_row5
FKS2 Corollary 24, row 5 (table7 entry (x ↦ (log x)³·x^{-1/2}, Icc 1 80)):
Eπ x ≤ (log x)³·x^{-1/2} whenever log x ∈ [1, 80]. For x > 0 this splits into
the three segments above; for x < 0 (possible since log is even) the exponent
-(1)/2 gives cos((-(1)/2)·π) = cos(-π/2) = 0, so x^{-1/2} = 0 and the RHS is 0,
while Eπ x ≤ 0.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row5 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row5.lean:91
theorem
FKS2.floor_row6
Row-6 floor (Buthe) [e^8, e^10] via floor_xpow_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row6 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean:74
theorem
FKS2.corollary_24_row6
FKS2 Corollary 24, row 6 (table7 entry (x ↦ x^{-1/3}, Icc 1 80.55)):
Eπ x ≤ x^{-1/3} whenever log x ∈ [1, 80.55]. For x > 0 this splits into
the four segments above; for x ≤ 0 (possible since log is even) Eπ x ≤ 0 < x^{-1/3}.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row6 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean:121
theorem
FKS2.floor_row7
Row-7 floor (Buthe) [e^6, e^10] via floor_xpow_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row7 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean:74
theorem
FKS2.corollary_24_row7
FKS2 Corollary 24, row 7 (table7 entry (x ↦ x^{-1/4}, Icc 1 107.6)):
Eπ x ≤ x^{-1/4} whenever log x ∈ [1, 107.6]. For x > 0 this splits into
the four segments above; for x ≤ 0 (possible since log is even) Eπ x ≤ 0 < x^{-1/4}.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row7 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean:121
theorem
FKS2.floor_row8
Row-8 floor (Buthe) [e^5, e^10] via floor_xpow_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row8 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean:74
theorem
FKS2.corollary_24_row8
FKS2 Corollary 24, row 8 (table7 entry (x ↦ x^{-1/5}, Icc 1 134.8)):
Eπ x ≤ x^{-1/5} whenever log x ∈ [1, 134.8]. For x > 0 this splits into
the four segments above; for x ≤ 0 (possible since log is even) Eπ x ≤ 0 < x^{-1/5}.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row8 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean:121
theorem
FKS2.floor_row9
Row-9 floor (Buthe) [e^4, e^10] via floor_xpow_of_check.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row9 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean:74
theorem
FKS2.corollary_24_row9
FKS2 Corollary 24, row 9 (table7 entry (x ↦ x^{-1/10}, Icc 1 270.8)):
Eπ x ≤ x^{-1/10} whenever log x ∈ [1, 270.8]. For x > 0 this splits into
the four segments above; for x ≤ 0 (possible since log is even) Eπ x ≤ 0 < x^{-1/10}.
PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row9 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean:121
Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.