Eventual bank precharge with a retained one-twelfth reserve
ProvedErdos390.WholePaper.exists_eventually_bankPaperPrechargedTailTarget_with_twelfthReserve_compactanalytic-number-theoryerdos-390erdos390-source-construction
Let , and write . There exists a depth such that, for all sufficiently large , there are a paper bank and a compatible guarded central-anchor certificate. Let be its central-anchor divisor, the bank's precharge base-state product, the central tail product, and the certificate's precharged tail target. Then
For every prime , both reserves hold:
This preserves a visible positive reserve after charging both the central anchors and the bank.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_008
Formal statement
theorem Erdos390.WholePaper.exists_eventually_bankPaperPrechargedTailTarget_with_twelfthReserve_compact : Erdos390.RemainingAnalyticGoal008_011 := by sorry
Source