Coherent source and bridge families can be chosen after fixed pre-mesh data
ProvedErdos390.WholePaper.BankPaperRealization.exists_bankPaperCanonicalSectionNinePostHeight_sourceFirstPreMeshEventualCoherentBridgeSourceObligation_compactWrite , , , and . Fix , a paper combined-charge exponent , , protected and active coefficients , with , and multiplicity , where is the rough-head density; assume . Let be a guarded tail family whose certificates satisfy the combined anchor/bank capacity divisibility, base-bank and selector-charge divisibilities into the precharged target, and both exact target-product identities. For each prime , require the precharged target valuation to exceed the selector-charge valuation by at least . Then one can choose a positive head exponent , positive source-cell and post-head margins, positive mass and density constants, and total scalar ledger families , all before the final mesh. Put equal to the guarded smooth-mass family, equal to half the canonical physical tolerance, and . These families satisfy
For every later regular relative mesh of positive width there is a total fresh bridge family satisfying the eventual coherent bridge/source obligation: eventually it arises from the literal fiber of , has the canonical guarded sample, carries source and primitive-gap packages with the fixed margins, and has exactly the chosen cutoff, coefficients, smooth mass, mass bound, and cell-density bound.
import Definitions.Def_erdos390_remaining_analytic_propositions_005
theorem Erdos390.WholePaper.BankPaperRealization.exists_bankPaperCanonicalSectionNinePostHeight_sourceFirstPreMeshEventualCoherentBridgeSourceObligation_compact : Erdos390.RemainingAnalyticGoal005_002 := by sorry