Joint guarded certificate with explicit signed bank states

Definition

erdos390_signed_bank_data

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

combinatoricserdos390prime-valuations

Fix $n,h$ and let $M=2n+h$ . This datum records the joint central anchor, divisor, charged fractional certificate, complete rough-signature rows, and the finite bank capacity from the upper-bound construction.

The bank is given as literal two-state factor sets indexed by $\beta_p$ copies of each sign for every prime $p\le y$ . Its initial set is exactly

B_0=\bigcup_gG_g^0.

Every state is legal, avoids the central anchor, fixed factors and all candidates, and is disjoint from every state of a different slot. The local product-valuation changes are

v\!\left(\prod G_g^1\right)-v\!\left(\prod G_g^0\right)=\pm e_p.

The capacities dominate the logarithmic rounding-error bound. This interface records explicit states and local identities, so universal realization of bounded integer corrections can be derived by a separate finite theorem.

Definition code

import Definitions.Def_erdos390_prime_power_bank_data
import Definitions.Def_erdos390_signed_bank
open scoped BigOperators
namespace Erdos390
open WholePaper
noncomputable section

/-- The literal finite prime support of the correction bank. -/
def bankPrimeSupport (cutoff : ℕ) : Finset ℕ := Nat.primesBelow (cutoff + 1)

structure GuardedSignedBankData (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 : ℝ)
  state : SignedBankSlot (fun p : ↑(bankPrimeSupport cutoff) ↦ budget p.1) →
    Bool → Finset ℕ
  bank0_eq : bank0 = baseBankFactors state
  state_subset : ∀ g b, state g b ⊆ factorInterval n (2 * n + h)
  state_guard : ∀ g b,
    Disjoint ((central ∪ fixed) ∪ Finset.univ.image value) (state g b)
  state_disjoint : ∀ g k, g ≠ k → ∀ b c, Disjoint (state g b) (state k c)
  state_change : ∀ g,
    integerValuationVector ((state g true).prod id) -
        integerValuationVector ((state g false).prod id) =
      embeddedSignedBankSlotChange (fun p : ↑(bankPrimeSupport cutoff) ↦ p.1) g

end
end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdos Problem 390, Section 5, Lemma precharged-universal-bank and bank-base-product; Section 10, guarded-integral-exactification and bank-state-replacement. https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex . Literal signed-state interface in BankPaperExactificationState.lean.

View graph