Guarded fractional certificate with complete rough-signature rows

Definition

erdos390_prime_power_bank_data

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

erdos390prime-valuationsrounding

Fix $n,h$ and put $M=2n+h>0$ . The datum consists of a central anchor $A$ , its divisor $D$ , a positive target $Y$ , fixed and initial bank factors, distinct legal candidates $a_i$ , weights $x_i\in[0,1]$ , and a bank universal for a finitely supported prime budget. The charged valuation equation is

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

Every row has integer total weight and a constant complete signature $(v_p(a_i))_{p>y}$ . The prime budget satisfies

\beta_p\ge4\lfloor\log_2M\rfloor\lfloor\log_pM\rfloor\quad(p\le y,\ p\text{ prime}),\qquad\beta_p=0\quad(p>y).

All interval and disjointness guards, the anchor product, and the identity $YD=\prod_{2n<a\le M}a$ are included. This is a concrete pre-rounding interface: the prime-power columns and their rounding-error estimates can be constructed from the recorded factor bounds and row signatures.

Definition code

import Definitions.Def_erdos390_guarded_fractional_bank
import Definitions.Def_erdos390_prime_power_rounding
open scoped BigOperators
namespace Erdos390
open WholePaper
noncomputable section

structure GuardedPrimePowerBankData (n h : ℕ) where
  D : ℕ
  Y : ℕ
  central : Finset ℕ
  fixed : Finset ℕ
  bank0 : Finset ℕ
  coordinateCount : ℕ
  rowCount : ℕ
  value : Fin coordinateCount → ℕ
  value_injective : Function.Injective value
  row : Fin coordinateCount → Fin rowCount
  rowSignature : Fin rowCount → ℕ →₀ ℕ
  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)
  endpoint_pos : 0 < 2 * n + h
  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 : ℝ)
  complete_rows : ∀ a, completeRoughSignature cutoff (value a) = rowSignature (row a)
  budget_capacity : ∀ p : ℕ, p.Prime → p ≤ cutoff →
    4 * Nat.log 2 (2 * n + h) * Nat.log p (2 * n + h) ≤ budget p
  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 : ℝ)
  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, assembly-integer-row-certificate, assembly-valuation-certificate, rounding-prime-power-column, rounding-error-box and rounding-no-rough-error; https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex. Interface for the hypotheses of guarded-integral-exactification; it asserts no existence result.

View graph