YukonModule.ProximityPrize.SubmissionLower.MovingSourcePersistentSeeds6814.part0

import Definitions.Def_Yukon_c71a73feb87d242e88d6b4dc















































































































































































































































































































































































set_option backward.isDefEq.respectTransparency.types false
/-! The old persistent/tangent engine works with the new frame's pole
bound. It does not require a second global budget family to be built. -/
namespace ProximityPrize.SubmissionLower.MovingSourcePersistentSeeds6814
noncomputable section
set_option autoImplicit false
set_option maxRecDepth 20000
set_option maxHeartbeats 500000
open scoped BigOperators Classical
open RCN002 RCN022 RCN042 RCN074 RCN086 RCN095 RCN135 RCN136 RCN159 RCN174
open RCN238 RCN243 RCN244 RCN264 RCN312 RCN341
open MovingSourceProjectionFamily6814 MovingSourceGammaProjections6814 MovingSourceLinearCycleFamily6814
open MovingSourceFrameZeroCount6814 MovingSourceProperSeedCount6814 MovingSourceReducedGamma6814
open MovingSourceLinearFlow6814 MovingSourceReducedRoutes6814

variable {K I : Type} [Field K]
variable {Gamma : Finset K} {x : I → K} {p : ℕ} {flag : FlagDegree}
  [CharP (GenericField K) p] {errorCap : ℕ}
  {stageSupport : RCN275.ResidualSupportParameters}

abbrev PersistentComponent (S : Stage K I Gamma x p flag errorCap stageSupport) :=
  {C : FirstTailComponent S //
    Transcendental (GenericField K) (coordinate (GenericField K) C.1 2) ∧
      ∀ delay, globalTailCut (polynomialEmbedding K) S.F (RCN326.w+1+delay)∈C.1}




theorem persistent_checked_budget :
    (80889+1)*flagMixed ⟨3504,45,12⟩ reducedFirstFlag unitYZFlag=497878763753400 := by decide +kernel



end
end ProximityPrize.SubmissionLower.MovingSourcePersistentSeeds6814