Eventual guarded post-tangent certificate with complete prime signatures
OpenErdos390.eventual_guarded_prime_power_bank_data_existsLet and set and . For all sufficiently large , there is a jointly guarded central anchor, fixed factor set, fractional candidate selector, and correction bank with exact charged valuation balance, in the sense of the accompanying definition.
The candidates are distinct legal positive factors, the fractional weights lie in , and every row has integer total weight and a fixed complete rough signature above a cutoff . The universal bank has a finite prime budget satisfying
The anchor and its divisor are part of the simultaneous datum, with
This is the remaining post-tangent existence obligation. Column sparsity and the effect of rounding are conclusions to be proved from positive factor bounds and complete signatures, rather than additional existence assumptions.
import Definitions.Def_erdos390_prime_power_bank_data open Filter open Erdos390
theorem Erdos390.eventual_guarded_prime_power_bank_data_exists :
∀ c : ℝ, C0 < c →
∀ᶠ n : ℕ in atTop,
Nonempty (GuardedPrimePowerBankData n (Nat.ceil (c * secondOrderScale n))) := by sorry