YukonModule.ProximityPrize.SubmissionLower.RelativeCertifiedOffers6814.part0 — offer table

import Definitions.Def_Yukon_acb5a197f811d10dcf0b8b9d

set_option backward.isDefEq.respectTransparency.types false
/-! Checked count offers for every saved complete relative-interpolation record.
Numerical certificates are imported in two bounded parallel build lanes. -/
namespace ProximityPrize.SubmissionLower.RelativeCertifiedOffers6814
noncomputable section
set_option autoImplicit false
set_option maxHeartbeats 2000000
set_option maxRecDepth 30000
open RelativeCertificate6814 MvPolynomial RCN100 RCN119 ContactOrderBridge
open RCN234 (wt)

def offer (i : Fin 74) : Band := ![
  ⟨10,56,3902,3917,12314372801839158⟩,
  ⟨10,57,3839,3887,13001470909723472⟩,
  ⟨10,58,3778,3857,13815262346775253⟩,
  ⟨10,59,3720,3826,15142263455696441⟩,
  ⟨10,60,3663,3794,28071367303838939⟩,
  ⟨10,61,3607,3762,25623191491887557⟩,
  ⟨10,62,3553,3729,25429572464128480⟩,
  ⟨10,63,3501,3695,25818239135729719⟩,
  ⟨10,64,3450,3660,30852343176758710⟩,
  ⟨10,65,3365,3382,29942600766848928⟩,
  ⟨10,65,3401,3526,29120250030593851⟩,
  ⟨11,52,3910,3939,15557768288906582⟩,
  ⟨11,53,3843,3910,15920488015804283⟩,
  ⟨11,54,3777,3881,16579153454940115⟩,
  ⟨11,55,3714,3852,17203165831889032⟩,
  ⟨11,56,3653,3822,21365995913629089⟩,
  ⟨11,57,3594,3792,29852491993091276⟩,
  ⟨11,58,3593,3648,31497735569814201⟩,
  ⟨11,58,3649,3760,24048096188955155⟩,
  ⟨11,59,3481,3729,30802988920566145⟩,
  ⟨11,60,3427,3696,33521411871134215⟩,
  ⟨11,61,3342,3663,33078648536786900⟩,
  ⟨11,62,3291,3629,32519066574844031⟩,
  ⟨11,63,3243,3453,33242252433776975⟩,
  ⟨12,49,3885,3924,11380060537880462⟩,
  ⟨12,50,3814,3896,11887928042267056⟩,
  ⟨12,51,3746,3868,12456861955597707⟩,
  ⟨12,52,3680,3840,13454343594378053⟩,
  ⟨12,53,3616,3811,14309438150475707⟩,
  ⟨12,54,3554,3781,45250040799475385⟩,
  ⟨12,55,3569,3622,43635301424197579⟩,
  ⟨12,55,3623,3751,16595982557763940⟩,
  ⟨12,56,3579,3720,45323634816865846⟩,
  ⟨12,57,3562,3604,44327286260835128⟩,
  ⟨12,57,3605,3689,34129398216919554⟩,
  ⟨12,58,3294,3657,37250082627013846⟩,
  ⟨12,59,3242,3624,35744153477019664⟩,
  ⟨12,60,3192,3562,36513206755580898⟩,
  ⟨12,61,3143,3230,36906415880582464⟩,
  ⟨13,46,3891,3902,29834286854120794⟩,
  ⟨13,47,3816,3875,30250102705817801⟩,
  ⟨13,48,3743,3848,30263617675957735⟩,
  ⟨13,49,3673,3820,33595668368951999⟩,
  ⟨13,50,3606,3792,35521311516555975⟩,
  ⟨13,51,3540,3763,35942556125440015⟩,
  ⟨13,52,3477,3734,36220912882672232⟩,
  ⟨13,53,3561,3704,37490083844189941⟩,
  ⟨13,54,3429,3499,43529310385779473⟩,
  ⟨13,54,3500,3673,37547057277830775⟩,
  ⟨13,55,3269,3642,38264302020204984⟩,
  ⟨13,56,3215,3610,38998155752837401⟩,
  ⟨13,57,3162,3521,38189126221457976⟩,
  ⟨13,58,3111,3170,38681762068485816⟩,
  ⟨14,44,3847,3847,31401086485671265⟩,
  ⟨14,45,3769,3820,30916619969042350⟩,
  ⟨14,46,3694,3792,38417668916827212⟩,
  ⟨14,47,3622,3764,38868901089933472⟩,
  ⟨14,48,3552,3736,38930904320711343⟩,
  ⟨14,49,3486,3707,39776287235706232⟩,
  ⟨14,50,3420,3678,40036978180364100⟩,
  ⟨14,51,3326,3648,42696548203814196⟩,
  ⟨14,52,3267,3618,42465170915191208⟩,
  ⟨14,53,3210,3418,41280379768223620⟩,
  ⟨15,43,3743,3756,34235134238621216⟩,
  ⟨15,44,3665,3728,24686100989165518⟩,
  ⟨15,45,3591,3700,24797592955066327⟩,
  ⟨15,46,3519,3672,32050357149758057⟩,
  ⟨15,47,3450,3569,31668756403961290⟩,
  ⟨18,19,3871,3955,1359136408997686⟩,
  ⟨9,62,3819,3822,24778021202031104⟩,
  ⟨9,63,3763,3789,25653739537571487⟩,
  ⟨9,64,3709,3755,24348315935019910⟩,
  ⟨9,65,3656,3720,25575436343300081⟩,
  ⟨9,66,3605,3684,27171955951741397⟩] i

end
end ProximityPrize.SubmissionLower.RelativeCertifiedOffers6814