Eventual joint guarded fractional certificate and universal bank

Open

Erdos390.eventual_guarded_fractional_bank_data_exists

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

erdos390prime-valuationsrounding

Let $C_0=4029639598/25970038185$ and $c>C_0$ . Put

h_n=\left\lceil c\frac{n}{\log n}\right\rceil,\qquad T_n=\prod_{2n<a\le2n+h_n}a.

For all sufficiently large $n$ , there is a joint guarded fractional certificate and correction bank, in the sense of the accompanying definition, with legal factors in $(n,2n+h_n]$ .

In particular the datum includes a central set $A\subseteq(n,2n]$ , its divisor $D$ , a positive integer $Y$ , fixed factors $F$ , an initial bank $B_0$ , distinct candidates $a_i$ , and weights $x_i\in[0,1]$ satisfying

\prod A=\binom{2n}{n}D,\qquad YD=T_n,

v_p\!\left(\prod F\right)+v_p\!\left(\prod B_0\right)+\sum_i x_i v_p(a_i)=v_p(Y)\quad\text{for every prime }p.

The row sums are integers, the incidence columns are sparse, every row-preserving rounding with the specified discrepancy lies in the finite prime-error budget, and the jointly guarded bank realizes every signed correction in that budget.

This is the pre-rounding analytic and combinatorial existence obligation for the corrected upper-bound construction. The anchor, divisor, quotas, and bank are chosen simultaneously; the statement makes no assertion for an independently prescribed divisor. The rounding and final product assembly are separate finite steps.

Preamble

import Definitions.Def_erdos390_guarded_fractional_bank
open Filter
open Erdos390

Formal statement

theorem Erdos390.eventual_guarded_fractional_bank_data_exists :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        Nonempty (GuardedFractionalBankData n (Nat.ceil (c * secondOrderScale n))) := by sorry

Source

Shouqiao Wang, A Proposed Solution to Erdos Problem 390, Sections 5 and 8-10; Lemma precharged-universal-bank, equations post-tangent-certificate, assembly-base-product, assembly-pre-solve-divisibility, assembly-integer-row-certificate, assembly-valuation-certificate, rounding-error-box, rounding-no-rough-error; hypotheses of Proposition guarded-integral-exactification. https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex . This packages the simultaneous construction asserted there, leaving its existence open.

View graph