Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Eventual joint fractional certificate and guarded prime-marked paths

Open
Erdos390.eventual_guarded_marked_bank_data_exists

by doctosil · Sep 16, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricserdos390prime-valuations

For every c>C0c>C_0c>C0​, put hn=⌈cn/log⁡n⌉h_n=\lceil cn/\log n\rceilhn​=⌈cn/logn⌉. For all sufficiently large nnn, there is a simultaneous central anchor, charged fractional certificate, and family of guarded prime-marked integer paths described by the accompanying definition:

∃ GuardedMarkedBankData(n,hn).\exists\,\mathrm{GuardedMarkedBankData}(n,h_n).∃GuardedMarkedBankData(n,hn​).

For each prime up to the cutoff, the paths provide the prescribed number of positive and negative slots. Their cores start at that prime and end at 111, with positive common edge scales. Prime markers are globally distinct and exceed the endpoint cofactors. Every endpoint lies in the allowed interval and avoids the anchor, fixed factors, and all candidates. The initial bank contains every slot's zero state and is charged in the exact fractional valuation balance.

This is the remaining joint geometric and analytic existence assertion. Signed-unit changes and cross-slot disjointness follow from the separate marked-path theorem, while bounded-error universality follows from the finite signed-bank theorem. Neither conclusion is assumed as a field of this construction datum.

Preamble
import Definitions.Def_erdos390_marked_bank_data
open Filter
open Erdos390
Formal statement
theorem Erdos390.eventual_guarded_marked_bank_data_exists :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        Nonempty (GuardedMarkedBankData n (Nat.ceil (c * secondOrderScale n))) := by sorry
Source
Shouqiao Wang, A Proposed Solution to Erdos Problem 390, pinned commit 61325b10bbdc29f4fb5e0618b414b9f2189333ad, Section 5, complete-rough-signature, bank-ordinary-cell, bank-four-bottom-pools, bank-unit-ratio, bank-unit-vector, Lemma bank-donor-injection, and the distinct-marker argument immediately before subsection bank-precharge. https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex . See also BankPathAlgebra.lean, BankPaperComponents.lean, and BankPaperExactificationState.lean in 390/lean/Erdos390/WholePaper/. Joint analytic output: Sections 9-10, post-tangent-certificate and assembly-valuation-certificate. Existence of the joint marked-path and fractional construction remains open.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me