A common depth for guarded bank capacity and post-tangent continuation
ProvedErdos390.SourceJointConstruction.exists_common_depthLet
For every real number , there is a natural number such that both the fixed-depth guarded bank capacity assertion and the canonical post-tangent continuation assertion hold at :
Here capacity asserts that, for all sufficiently large , there are a compatible signed bank and guarded central-anchor certificate with the specified precharge and upper-tail divisibility identities. Continuation asserts that eventual capacity at this depth can be refined to eventual compatible fractional selections with integral complete rough-row sums, exact prime-valuation balance, the prescribed interval support, and all collision exclusions. The predicates retain the literal objects and conditions defined in the accompanying source interface.
The same depth must serve both assertions. This statement is obtained from the source's distributed Section 9 terminal by retaining its depth and projecting its capacity and continuation fields; its auxiliary width and tangent parameters are discarded.
import Definitions.Def_erdos390_source_bank_interface
theorem Erdos390.SourceJointConstruction.exists_common_depth
{c : ℝ} (hc : Erdos390.WholePaper.C0 < c) :
∃ depth : ℕ, 201 ≤ depth ∧
Erdos390.WholePaper.BankPaperCanonicalCapacityAtDepth c depth ∧
Erdos390.WholePaper.BankPaperCanonicalPostTangentContinuationAtDepth c depth := by sorry