ProofAtlas

First-party checked source

Source for Power-Law Phase Gap for Multiples of log₂ 3

This pinned Lean source formalizes the following mathematical result: There exists a positive constant c such that every positive integer q satisfies c · q⁻¹³³ᐟ¹⁰ ≤ ‖q log₂ 3‖, the distance to the nearest integer. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Immutable source commit: a7e937d2c87047b2275323c5f186e6e8bdefceb3

Checked source + agent continuation package · 40 Lean files · 1 evidence record · Download ZIP

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Formalization at a glance

What is checked—and how much source supports it

Browse the counted source
Declarations covered by evidence
1
First-party Lean files
40
Lean source lines
8,926
Main recorded file
56 lines

How counting works: Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence; it is not a count of every declaration in the source. Source footprint is not a difficulty or proof-quality score.

Exact theorem evidence

Power-Law Phase Gap for Multiples of log₂ 3

Erdos1135.ND.existsPhaseGapRhin

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit
a7e937d2c87047b2275323c5f186e6e8bdefceb3
Main Lean file
Erdos1135/ND/RhinPhaseGap.lean
Main-file footprint
56 lines
File SHA-256
sha256:223b9cc07b21fbfd22d0bf53683f76b2a046ed083b1986210478c3f36c5e360e
Complete Lean closure
40 files · 8,926 lines
Toolchain
leanprover/lean4:v4.30.0-rc2
Open main Lean file Download main Lean fileDownload checker evidence (JSON)Download Apache-2.0 licenseDownload Advameg, Inc. notice

Deduplicated checked source

Complete Lean import closure

This closure supports the theorem evidence record above.

Complete checked Lean closure

40 Lean files are available here

Start with the principal theorem and proof-architecture files below, or search the complete commit-pinned closure.

40Lean files
Search and browse all 40 checked Lean files

Every listed file is read from the same pinned Git commit. File links open raw source in a new tab; use the ZIP download for the complete package. External Mathlib modules are dependency-locked but are not copied into this first-party source tree.

Showing all 40 files

Erdos11354 files · 114 lines
Erdos1135/ND4 files · 301 lines
Erdos1135/NumberTheory/Rhin14 files · 5,960 lines
Erdos1135/Tao2 files · 118 lines
Erdos1135/Tao/Density1 file · 353 lines
Erdos1135/Tao/Probability6 files · 1,146 lines
Erdos1135/Tao/Section51 file · 180 lines
Erdos1135/Tao/Syracuse4 files · 255 lines
Erdos1135/Terras/Core1 file · 58 lines
Erdos1135/Terras/Density1 file · 358 lines
FormalConjectures/Util1 file · 37 lines
FormalConjectures/Wikipedia1 file · 46 lines
Source hashMatches checked record
Lean buildPassed in recorded evidence
LicenseApache-2.0 · Advameg, Inc.

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Advameg, Inc.; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.