Joint guarded fractional certificate and correction bank

Definition

erdos390_guarded_fractional_bank

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

erdos390prime-valuationsrounding

Fix natural numbers $n,h$ , and write $T=\prod_{2n<a\le 2n+h}a$ . A guarded fractional bank datum consists of a central anchor $A\subseteq(n,2n]$ , a divisor $D$ , a nonzero target $Y$ , fixed factors $F$ , an initial bank $B_0$ , and distinct candidates $a_i\in(n,2n+h]$ , together with a fractional vector $x_i\in[0,1]$ .

The anchor and target satisfy

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

The candidates have integer row sums and belong to at most $d$ incidence columns each. At every prime $p$ , the fractional certificate is

v_p\!\left(\prod F\right)+v_p\!\left(\prod B_0\right)+\sum_i x_i v_p(a_i)=v_p(Y).

A finitely supported prime budget $\beta_p$ bounds the valuation error of every zero-one vector with the same row sums and column discrepancies at most $4d$ . The reserved bank realizes every integer correction $e_p$ with $|e_p|\le\beta_p$ , relative to $B_0$ , using legal factors disjoint from the anchor, fixed factors and all candidates. The anchor, fixed factors and candidates also obey their pairwise guards.

This packages the simultaneous pre-rounding certificate and universal correction bank of Section 10. The anchor divisor is chosen as part of the datum. It is not quantified independently over all divisors of the tail.

Definition code

import Definitions.Def_erdos390_problem
import Definitions.Def_erdos390_floating_rounding

open scoped BigOperators

namespace Erdos390
open WholePaper
noncomputable section

/-- Integer-valued prime exponent, used for signed bank corrections. -/
def primeExponent (p m : ℕ) : ℤ := m.factorization p

/-- The distinct candidate values chosen by a zero-one vector. -/
def roundedValues {k : ℕ} (value : Fin k → ℕ) (X : Fin k → ℝ) : Finset ℕ := by
  classical
  exact (Finset.univ.filter fun a ↦ X a = 1).image value

/-- The joint data immediately before the rounding and bank-replacement steps
in Section 10. The central anchor and its divisor are part of this data. -/
structure GuardedFractionalBankData (n h : ℕ) where
  D : ℕ
  Y : ℕ
  central : Finset ℕ
  fixed : Finset ℕ
  bank0 : Finset ℕ
  coordinateCount : ℕ
  rowCount : ℕ
  columnCount : ℕ
  value : Fin coordinateCount → ℕ
  value_injective : Function.Injective value
  row : Fin coordinateCount → Fin rowCount
  inc : Fin columnCount → Fin coordinateCount → Prop
  degree : ℕ
  cutoff : ℕ
  budget : ℕ → ℕ
  x : Fin coordinateCount → ℝ
  central_subset : central ⊆ factorInterval n (2 * n)
  central_product : central.prod id = Nat.choose (2 * n) n * D
  fixed_subset : fixed ⊆ factorInterval n (2 * n + h)
  bank0_subset : bank0 ⊆ factorInterval n (2 * n + h)
  candidate_subset : Finset.univ.image value ⊆ factorInterval n (2 * n + h)
  central_fixed : Disjoint central fixed
  central_candidates : Disjoint central (Finset.univ.image value)
  fixed_candidates : Disjoint fixed (Finset.univ.image value)
  target_pos : Y ≠ 0
  target_product : Y * D = (factorInterval (2 * n) (2 * n + h)).prod id
  weights_unit : ∀ a, 0 ≤ x a ∧ x a ≤ 1
  integer_rows : ∀ r, ∃ k : ℤ, ∑ a ∈ rowSet row r, x a = (k : ℝ)
  column_sparse : ∀ a, (columnsContaining Finset.univ inc a).card ≤ degree
  budget_support : ∀ p, cutoff < p → budget p = 0
  fractional_balance : ∀ p : ℕ, p.Prime →
    (primeExponent p (fixed.prod id) : ℝ) +
      (primeExponent p (bank0.prod id) : ℝ) +
      ∑ a, x a * (primeExponent p (value a) : ℝ) =
        (primeExponent p Y : ℝ)
  rounding_error_bound : ∀ X : Fin coordinateCount → ℝ,
    (∀ a, X a = 0 ∨ X a = 1) →
    (∀ r, ∑ a ∈ rowSet row r, X a = ∑ a ∈ rowSet row r, x a) →
    (∀ c, |∑ a, (X a - x a) * zeroOneColumn inc c a| ≤ (4 * degree : ℝ)) →
    ∀ p : ℕ, p.Prime →
      |(primeExponent p ((roundedValues value X).prod id) : ℝ) -
        ∑ a, x a * (primeExponent p (value a) : ℝ)| ≤ (budget p : ℝ)
  bank_universal : ∀ e : ℕ → ℤ,
    (∀ p : ℕ, p.Prime → |e p| ≤ (budget p : ℤ)) →
    ∃ bank : Finset ℕ,
      bank ⊆ factorInterval n (2 * n + h) ∧
      Disjoint central bank ∧ Disjoint fixed bank ∧
      Disjoint (Finset.univ.image value) bank ∧
      ∀ p : ℕ, p.Prime →
        primeExponent p (bank.prod id) = primeExponent p (bank0.prod id) + e p

end
end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdos Problem 390, Section 10: post-tangent fractional certificate, floating rounding, rounding-error box, no-rough-error, and final bank replacement. https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex (lines 9750-10050). This interface packages those simultaneous hypotheses; existence remains a separate theorem.

View graph