Joint guarded fractional certificate with prime-marked paths

Definition

erdos390_marked_bank_data

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

combinatoricserdos390prime-valuations

For integers $n,h\ge0$ , this datum contains the central anchor, fixed factors, charged initial bank, candidate integers, complete rough-signature rows, fractional weights, cutoff and budgets of the preceding signed-bank certificate. The anchor product is $\binom{2n}{n}D$ , and $YD$ is the product of the tail $(2n,2n+h]$ . The fractional weights lie in $[0,1]$ , have integer row sums, and balance every prime valuation after the fixed factors and initial bank are charged.

Instead of assuming arbitrary state sets with signed-unit changes and collision guarantees, the datum supplies prime-marked integer paths. Every endpoint factor belongs to $(n,2n+h]$ and avoids the central anchor, fixed factors, and entire candidate universe. The charged initial bank is precisely the union of the zero states of these paths. Its prime markers are distinct and larger than every endpoint cofactor, as required in the path definition. The budget obeys

\beta_p\ge4\lfloor\log_2(2n+h)\rfloor\lfloor\log_p(2n+h)\rfloor\quad(p\le y\text{ prime}),

and vanishes above $y$ .

Existence means that all these objects can be chosen simultaneously. It remains a construction obligation; the finite path theorem derives signed-unit changes and disjointness from the arithmetic data.

Definition code

import Definitions.Def_erdos390_signed_bank_data
import Definitions.Def_erdos390_marked_bank_paths
open scoped BigOperators
namespace Erdos390
open WholePaper
noncomputable section

structure GuardedMarkedBankData (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 : ℝ)
  paths : MarkedBankPaths (bankPrimeSupport cutoff) (fun p ↦ budget p.1)
  bank0_eq : bank0 = baseBankFactors paths.signedState
  endpoint_legal : ∀ g b i, paths.endpoint g b i ∈ factorInterval n (2 * n + h)
  endpoint_guard : ∀ g b i,
    paths.endpoint g b i ∉ ((central ∪ fixed) ∪ Finset.univ.image value)

end
end Erdos390

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 fractional ledger: Sections 9-10, post-tangent-certificate and assembly-valuation-certificate. This is an arithmetic specialization of the joint interface, with no assertion that the analytic construction is already proved.

View graph