Coherent paper targets give the frozen-top residual inputs
ProvedErdos390.WholePaper.BankPaperRealization.eventually_bankPaperCanonicalTopFrozenRoundedSourceResidualInputsAt_of_coherentTarget_compactFix head patterns, physical intervals, a ledger family, depth , cutoff , and rough level . Assume , , , , , and . Eventually consider any bridge with the canonical sample data and guarded bank certificate. Require equal the actual guarded smooth base mass, and require its target to be the literal barycentric target constructed from a head reserve and physical interpolation target, with reserve active mass . Its patterns must be the prime-head simplex at the reserve exponent, contain all primes up to , and be head-separated. Require physical lower endpoints at least one, upper endpoints at most two and contained in the broad region , with . Samples must avoid the guard set. Head-reserve targets at primes up to must equal the selector-tail factorizations, and the fixed exceptional charge must divide the precharged target. For the prescribed balanced alpha and total coefficient ,
The target is constrained by actual constructors and exact identities; feasibility and support are conclusions, not assumptions.
import Definitions.Def_erdos390_remaining_analytic_propositions_004 universe u_1
theorem Erdos390.WholePaper.BankPaperRealization.eventually_bankPaperCanonicalTopFrozenRoundedSourceResidualInputsAt_of_coherentTarget_compact : Erdos390.RemainingAnalyticGoal004_014.{u_1} := by sorry