Lean evidence record
Power-Law Phase Gap for Multiples of log₂ 3: Lean evidence
This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.
Exact formal proposition
Hypotheses and conclusion
This is the exact recorded theorem statement, followed by the source definitions that give its named predicates and quantities their full meaning.
theorem existsPhaseGapRhin : ∃ c : ℝ, PhaseGap c (143 / 10 : ℝ)Definitions used in this proposition
PhaseGap
structure PhaseGap (c kappa : ℝ) : Prop where
c_pos : 0 < c
c_le_one : c ≤ 1
two_lt_kappa : 2 < kappa
gap : ∀ q : ℕ, 0 < q →
c * Real.rpow (q : ℝ) (1 - kappa) ≤
nearestIntegerNorm ((q : ℝ) * logTwoThree)Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Technical evidence record
Source identity, checker results, and assumptions
- Main Lean declaration
existsPhaseGapRhin- Source commit
a7e937d2c870
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.known-rhin-phase-gap.exists.v001- Accepted-result title
- Accepted Result: A Power-Law Gap from Integers for Multiples of log₂ 3
- Accepted-result status
- Accepted formalization of a known theorem
- Accepted-result boundary
- This target records the exact existential theorem ∃ c, PhaseGap c (143/10), which supplies a positive global power-law lower bound for the nearest-integer distance of positive multiples of log₂ 3. Non-claim: The witness c is existential; no numerical value is exposed. Non-claim: The gap shrinks like q^(-133/10), so it is not a uniform fixed separation from the integers. Non-claim: This theorem does not itself prove a Collatz or density theorem. Non-claim: Downstream rates require the strict inequality d < 5/143; the cap is not attained. Non-claim: It formalizes the specific Rhin-style large-height specialization needed by this route, not every theorem in Rhin's work. Non-claim: No priority claim is asserted.
- Declarations covered by recorded evidence
Erdos1135.ND.existsPhaseGapRhin- Lean build
- passed
- Recorded build time
- 1.3 s one machine-dependent evidence run, not a benchmark
- Evidence collected
- · clean-source provenance recorded
- Unfinished proof check
- passed
- Lean toolchain
leanprover/lean4:v4.30.0-rc2- Recorded source commit
a7e937d2c87047b2275323c5f186e6e8bdefceb3- Source SHA-256
sha256:223b9cc07b21fbfd22d0bf53683f76b2a046ed083b1986210478c3f36c5e360e- Statement alignment
- accepted
Lean foundations
Standard foundations used by the proof
Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.
Classical.choiceQuot.soundpropext
Files and machine-readable evidence
Reproduce or inspect the recorded check
Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.
Review results
Publication reviews accepted
All four required publication-review gates are accepted for the reviewed presentation of this exact theorem. The review results are separate from the Lean build and do not broaden the formal statement.
Read the publication-review details