YukonModule.ProximityPrize.SubmissionLower.MovingSourceLinearBudgetTarget6814.part0

import Definitions.Def_Yukon_b9264d25766439028c5b06aa











































































































































































































































































































































































set_option backward.isDefEq.respectTransparency.types false
/-! Proved delayed-tail envelopes and the exact arithmetic target for the
linear reduced-flow counter. This file proves NO geometric cardinality
bound: the proper-delay cycle, vertical and tangent consumers must supply
the separately named terms before this can be used in a score claim. -/
namespace ProximityPrize.SubmissionLower.MovingSourceLinearBudgetTarget6814
noncomputable section
set_option autoImplicit false
set_option maxRecDepth 20000
set_option maxHeartbeats 300000
open RCN234 RCN156
open MovingSourceLinearFlow6814 MovingSourceFlowNumerator6814 MovingSourceReducedTailWeights6814




def properRectangleTarget : ℕ :=
  57*(1441792*86508181+1441803*86507521)+
  12*(6291457*86508181+6291505*86507521)+
  3561*(6291457*1441803+6291505*1441792)

def denominatorHelperTarget : ℕ :=
  (131073*((1+2*131071*57)*21765+(131071*23)*104274+(1+2*131071*3561)*573)+50184-1)/50184+
    80890*573

def constantParameterTarget : ℕ := 12*86507521+3561*1441792
def tangentTarget : ℕ := 1802898105618360











end
end ProximityPrize.SubmissionLower.MovingSourceLinearBudgetTarget6814