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 521 to 540 of 1,644 declarations.
theorem
FKS2.Floor.etheta_le_floor
Eθ ≤ 4/5 on [2, e^10], via the θ engine + ⌊x⌋ stitching.
checkAllThetaRelErrorReal start limit checks real unit intervals for
N < limit; since exp 10 < 22027, the relevant floors satisfy
N < 22027 and use the [N, N+1) real certificate branch.
PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:17
theorem
FKS2.Floor.delta_two
δ(2) = 1 exactly.
PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:42
theorem
FKS2.Floor.etheta_integrand_intble
Integrability of the eq_30 integrand on [2,x] (mirrors lemma_12).
PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:57
theorem
FKS2.Floor.integral_etheta_bound
∫₂ˣ Eθ/log²t ≤ (4/5)/(log 2)²·(x−2) on the floor (crude: Eθ ≤ 4/5, log t ≥ log 2).
PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:74
theorem
FKS2.Floor.linear_le_curve
The curve comparison on the floor. After setting s = sqrt (log x),
the affine cover verifies 0.8 + (5/3) * s^2 ≤ 9.2211 * s^3 * exp (-0.8476 * s),
which rewrites to 4/5 + (5/3) * log x ≤ admissible_bound ... x.
PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:115
theorem
FKS2.Floor.corollary_22_floor
The Corollary 22 small-x floor: Eπ ≤ the admissible curve on [2, e^10], ungated - via the Chebyshev θ engine (Eθ bound), eq_30, and the affine-cover curve comparison.
PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:159
theorem
FKS2.Floor.corollary_22_of_midrange
Full Corollary 22, reduced to the remaining mid-range table-data theorem.
The small range is corollary_22_floor; the asymptotic tail is
FKS2.corollary_22_tail.
PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:202
theorem
FKS2.Table4Ext.allCells_checked
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:38
theorem
FKS2.Table4Ext.cover_of_chainOk
A nonempty chained cell list covers its full range: every point of
[exp lo, exp (lastB lo cells)] lies in some cell.
PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:71
theorem
FKS2.Table4Ext.Epi_le_admissible_on_midrange
The Corollary 22 mid-range: on [exp 10, exp 20000] the prime counting
error Eπ is bounded by the Corollary 22 admissible curve. The trusted
input is allCells_trusted (paper table data); everything else is
machine-checked: the cell inequalities by dyadic interval arithmetic
(allCells_checked), the grid contiguity by evaluation (allCells_chain,
allCells_last), and the transport to the curve by
cell_Epi_le_admissible.
PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:127
theorem
FKS2.Table4Ext.cell_eps_le_admissible
Transport: a checked cell dominates the table value by the Corollary 22
curve on the whole cell [exp b, exp b'].
PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean:99
theorem
FKS2.Table4Ext.cell_eps_le_admissible_gen
Transport: a checked cell dominates its table value by the row admissible
curve on the whole cell [exp b, exp b']. The two transcendental constants are
supplied as rational over-estimates (hCge, hrB).
PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtGenCore · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtGenCore.lean:80
theorem
FKS2.Table4Ext.cell_eps_le_admissible_quarter
Transport for a B = 1/4 row via the squared check. hCge carries the
DOUBLED rate 2·(C/√R), hrB carries √R = R^{1/2} ≤ rB. Recovers the
half-power curve by taking square roots outside the kernel.
PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtGenQuarterCore · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtGenQuarterCore.lean:40
theorem
FKS.remark_2_6_a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky · PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:265
theorem
FKS.remark_2_6_b
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky · PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:304
theorem
FKS.remark_3_7
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky · PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:427
theorem
Goldbach.even_to_odd_goldbach
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Goldbach · PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:92
theorem
Goldbach.ramare_saouter_odd_goldbach
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Goldbach · PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:157
theorem
Goldbach.helfgott_odd_goldbach_finite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Goldbach · PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:184
theorem
Goldbach.e_silva_herzog_piranian_goldbach_ext
The arguments in \cite[Appendix C]{helfgott-goldbach-arxiv} push the bound further than this, but require unpublished estimates of Ramare. However, similar arguments were established in \cite{kadiri-lumley}, and we present them here.
PrimeNumberTheoremAnd.IEANTN.Goldbach · PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:206
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.