/-
  第1112コマ — 38 段のデータ（ブロックの最大元の証明書 `(p,q,r,t,桁)` と offset `a`）と、倍加税の鎖の検査。
  `erdos1112.py` が生成。sorry 0・native_decide 不使用。
-/
import Shioriproofs.Erdos1112c
import Shioriproofs.Erdos1112kd

namespace Shiori1112

set_option maxRecDepth 100000

/-- 38 段。`a₁ = 2r₀+1`、`a_{j+1} = 2(a_j + t_j) + 1`（`bin-111-f4-stages.txt`）。 -/
def stages4 : List Stage :=
  [(((68, 15, 2833, 45079234413531728106229468079524, [67, 67, 67, 67, 67, 41, 34, 34, 34, 34, 34, 34, 34, 34, 34]), 4527528777914432254565203631367)),
   (((84, 15, 4318, 1095764109589853867455541979581793, [83, 83, 83, 83, 83, 46, 44, 42, 42, 42, 42, 42, 42, 42, 42]), 99213526382892320721589343421783)),
   (((104, 15, 6628, 27448915242869489768604076604692222, [103, 103, 103, 103, 102, 61, 54, 53, 52, 52, 52, 52, 52, 52, 52]), 2389955271945492376354262646007153)),
   (((128, 15, 10033, 626718782969314078886467039252282234, [127, 127, 127, 127, 126, 69, 65, 64, 64, 64, 64, 64, 64, 64, 64]), 59677741029629964289916678501398751)),
   (((112, 16, 8203, 18700267246515141336403113860918209254, [111, 111, 111, 111, 111, 87, 59, 57, 56, 56, 56, 56, 56, 56, 56, 56]), 1372793047997888086352767435507361971)),
   (((138, 16, 12463, 534925258992769834799973765248297252794, [137, 137, 137, 137, 137, 106, 76, 70, 70, 69, 69, 69, 69, 69, 69, 69]), 40146120589026058845511762592851142451)),
   (((172, 16, 19363, 18351684108646178281789616053847273803479, [171, 171, 171, 171, 171, 132, 89, 87, 86, 86, 86, 86, 86, 86, 86, 86]), 1150142759163591787290971055682296790491)),
   (((152, 17, 16078, 764706336545583977468980532399607738875860, [151, 151, 151, 151, 151, 135, 86, 78, 76, 76, 76, 76, 76, 76, 76, 76, 76]), 39003653735619540138161174219059141187941)),
   (((190, 17, 25129, 34342869042165732285654051764909993709691381, [189, 189, 189, 189, 189, 169, 102, 96, 95, 95, 95, 95, 95, 95, 95, 95, 95]), 1607419980562407035214283413237333760127603)),
   (((240, 17, 40093, 1839389624354791037011939623979236199835494231, [239, 239, 239, 239, 239, 213, 126, 121, 120, 120, 120, 120, 120, 120, 120, 120, 120]), 71900578045456278641736670356294654939637969)),
   (((200, 18, 29509, 32845972633058271982629272770386230472247701595, [199, 199, 199, 199, 199, 197, 103, 100, 100, 100, 100, 100, 100, 100, 100, 100, 100, 100]), 3822580404800494631307352588671061709550264401)),
   (((240, 18, 42494, 881067630065948261289922201876005728624587269594, [239, 239, 239, 239, 239, 236, 123, 121, 121, 120, 120, 120, 120, 120, 120, 120, 120, 120]), 73337106075717533227873250718114584363595931993)),
   (((280, 18, 57839, 14203080426400475230937214102544894780179680506075, [279, 279, 279, 279, 279, 275, 143, 142, 140, 140, 140, 140, 140, 140, 140, 140, 140, 140]), 1908809472283331589035590905188240625976366403175)),
   (((360, 18, 95614, 1318530047522003047779994600833125204052560365372552, [359, 359, 359, 359, 359, 353, 184, 182, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180]), 32223779797367613639945610015466270812312093818501)),
   (((320, 19, 79814, 100805983088944688760495814614834242302692765922303600, [319, 319, 319, 319, 319, 319, 243, 163, 161, 161, 160, 160, 160, 160, 160, 160, 160, 160, 160]), 2701507654638741322839880421697182949729744918382107)),
   (((400, 19, 124715, 7036534337263148755835000979038871657548290607252214694, [399, 399, 399, 399, 399, 399, 302, 210, 203, 201, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 207014981487166860166671390073062850504845021681371415)),
   (((360, 20, 106415, 681628611897022278640824342322775303677200125840466665146, [359, 359, 359, 359, 359, 359, 319, 186, 182, 181, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180]), 14487098637500631232003344738223869016106271257867172219)),
   (((320, 21, 88355, 41161199820860984393764149534243441403695318228135342337582, [319, 319, 319, 319, 319, 319, 314, 173, 163, 162, 160, 160, 160, 160, 160, 160, 160, 160, 160, 160, 160]), 1392231421069045819745655374121998345386612794196667674731)),
   (((400, 21, 138050, 4492130557443131432763623404661355293680735431307170339607577, [399, 399, 399, 399, 399, 399, 392, 215, 201, 201, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 85106862483860060427019609816730879498163862044664020024627)),
   (((360, 22, 117221, 352375408834896534473085352780551172358884266040151726621012302, [359, 359, 359, 359, 359, 359, 359, 273, 192, 181, 181, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180]), 9154474839853982986381286028956172346357798586703668719264409)),
   (((400, 22, 144726, 3589212315397062015023651584642625759824067865028502632804215894, [399, 399, 399, 399, 399, 399, 399, 303, 211, 202, 201, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 723059767349501034918933277619014689410484129253710790680553423)),
   (((360, 23, 122622, 253357918952290608286474753940345327937450375198526815231831467035, [359, 359, 359, 359, 359, 359, 359, 319, 195, 181, 181, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180]), 8624544165493126099885169724523280898469103988564426846969538635)),
   (((400, 23, 151386, 2867780640002252550005658883103090236952460226419170934788297096256, [399, 399, 399, 399, 399, 399, 399, 354, 216, 205, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 523964926235567468772719847329737217671838958374182484157602011341)),
   (((360, 24, 128022, 182164343726696947358153822096475743708693448165555408428949964908472, [359, 359, 359, 359, 359, 359, 359, 354, 186, 183, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180]), 6783491132475640037556757460865654909248598369586706837891798215195)),
   (((400, 24, 158052, 2291356731361799787455597138689821689618841562271264257965808388615189, [399, 399, 399, 399, 399, 399, 399, 393, 207, 202, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 377895669718345174791421159114682797235884093070284230533683526247335)),
   (((360, 25, 133428, 130976163139495105150531385433702347181168377778837441921662523989212824, [359, 359, 359, 359, 359, 359, 359, 359, 274, 192, 182, 181, 181, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180]), 5338504802160289924494036595609008973709451310683096976998983829725049)),
   (((400, 25, 164727, 1830794028358078030177157055809919951120841881578722420294118625875273094, [399, 399, 399, 399, 399, 399, 399, 399, 304, 211, 201, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 272629335883310790150050844058622712309755658179041077797323015637875747)),
   (((360, 26, 138828, 94171861297296980603232234839981031791709640652598439388810842765640921152, [359, 359, 359, 359, 359, 359, 359, 359, 320, 192, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180, 180]), 4206846728482777640654415799737085326861195079515526996182883283026297683)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 196757416051559516487773301279436234237141671464227932769987452097334437671)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 3319123689419327725198645826366780336138745299520434744163388161825582607851)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 9563856236154864142620390876541468539941952555632848366950189581282078948211)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 22053321329625936977463880976890844947548367067857675612523792420195071628931)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 47032251516568082647150861177589597762761196092307330103670998098021056990371)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 96990111890452373986524821578987103393186854141206639085965409453673027713251)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 196905832638220956665272742381782114654038170239005257050554232164976969159011)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 396737274133758122022768583987372137175740802434602492979731877587584852050531)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 796400157124832452737760267198552182219146066825796964838087168432800617833571)),
   (((400, 26, 171391, 1462804428658104346111549611903953933832230978295989439311706628815456866254, [399, 399, 399, 399, 399, 399, 399, 399, 355, 213, 204, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200, 200]), 1595725923106981114167743633620912272305956595608185908554797750123232149399651))]

theorem stages4_length : stages4.length = 38 := by decide

/-- **鎖の機械検査**：全段で `2·r_{j−1} < a_j`、`t_j = max B(p_j,q_j,r_j)`（証明書）。 -/
theorem chain4 : chainChk4 stages4 (r0 : ℤ) = true := by decide +kernel

/-- 38 段の窓 `(p, q, r, a)`。 -/
def wins4 : List (ℕ × ℕ × ℕ × ℕ) := stages4.map winOf

theorem wins4_length : wins4.length = 38 := by decide

/- 以後 `wins4` は展開しない（`head4` と同じ理由。窓の `BlkF` を評価されると終わらない）。 -/
attribute [irreducible] wins4

end Shiori1112