Eventual joint fractional certificate and guarded prime-marked paths
OpenErdos390.eventual_guarded_marked_bank_data_existsFor every , put . For all sufficiently large , there is a simultaneous central anchor, charged fractional certificate, and family of guarded prime-marked integer paths described by the accompanying definition:
For each prime up to the cutoff, the paths provide the prescribed number of positive and negative slots. Their cores start at that prime and end at , with positive common edge scales. Prime markers are globally distinct and exceed the endpoint cofactors. Every endpoint lies in the allowed interval and avoids the anchor, fixed factors, and all candidates. The initial bank contains every slot's zero state and is charged in the exact fractional valuation balance.
This is the remaining joint geometric and analytic existence assertion. Signed-unit changes and cross-slot disjointness follow from the separate marked-path theorem, while bounded-error universality follows from the finite signed-bank theorem. Neither conclusion is assumed as a field of this construction datum.
import Definitions.Def_erdos390_marked_bank_data open Filter open Erdos390
theorem Erdos390.eventual_guarded_marked_bank_data_exists :
∀ c : ℝ, C0 < c →
∀ᶠ n : ℕ in atTop,
Nonempty (GuardedMarkedBankData n (Nat.ceil (c * secondOrderScale n))) := by sorry