/-
Copyright (c) 2026 Terence Tao. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Tao
-/
import Sendov.LargeDegree.Monotone

/-!
# The large-degree claim

`Sendov.U_le_Ut` removed the degree from the bound; what is left is the single inequality
`Ut α < 1` on `0 ≤ α ≤ 17`, and then `R n α < 1` for every `n ≥ 101`.

`Ut` is a rational function of `α` times `(α/(3+α)) ^ 48`, so multiplying by

  `D = 865200 · (3+α) ^ 49 · γ ^ 4`,   `γ = 300 + 47α - α²`,

which is positive on `[0,17]`, turns the claim into positivity of the single polynomial
`F = D (1 - Ut)` of degree `58`.  The two closed forms used are

  `c 101 α = γ / (100 (3+α))`,
  `T1 101 α = 1600000 (100-2α)² (3+α)³ / (721 γ⁴)`.

A Bernstein certificate on `[0,17]` settles it: all 59 coefficients of `F` in the basis
`α^m (17-α)^(58-m)` are positive, so no subdivision of the `α`-range is needed.  (The
informal write-up splits at `α = 16` and estimates the two pieces separately; that is not
necessary once the sharp Beta constant is used, which is what leaves the margin — `Ut` peaks
at `α = 17` with value `0.9229`.)

## Why the multiplication is distributed by hand

`D (1 - Ut)` must not be handed to `field_simp`: it would clear `(3+α) ^ 49` and `γ ⁴` from
both sides at once, leaving `ring` a degree-115 identity that it does not close.  `D` already
*contains* exactly those denominators, so each of the six terms of `Ut` cancels against it
separately.  Doing that first (`Sendov.Ut_lt_one`, steps `t1`–`t6`, and `h48` for the `48`-th
power) keeps every `ring` call at degree at most `62`, which is the same size as the
certificate identity itself.  `865200` rather than `865200` is used as the multiplier so that
each term separately, not merely their sum, comes out with integer coefficients.

## Main statements

* `Sendov.Ut_lt_one`: `Ut α < 1` on `0 ≤ α ≤ 17`;
* `Sendov.large_degree`: `R n α < 1` for `n ≥ 101`.
-/

namespace Sendov

variable {α : ℝ}

set_option maxHeartbeats 4000000 in
-- a degree-58 identity in one variable; `ring` needs more than the default budget
/-- The Bernstein certificate: `F` is positive on `[0,17]`. -/
lemma F_pos (hα : 0 ≤ α) (hα' : α ≤ 17) :
    0 < 1122702787291394736448332031899900000000 + 19046325083555631071589567727384404000000 * α + 158421799401305511319831453323336122340000 * α ^ 2 + 861086144839783899262522290902928965732400 * α ^ 3 + 3439408019860839882261371580238947745811319 * α ^ 4 + 10763976190978343059270128976319908699279230 * α ^ 5 + 27482264870203746404049226779511973140100922 * α ^ 6 + 58851751350273881387953189525455032864879976 * α ^ 7 + 107855247587877306122230293103712405510570475 * α ^ 8 + 171759728691636266490365540891679381811794330 * α ^ 9 + 240529488382582584529650966973246412375404200 * α ^ 10 + 299026713527922503750214218383542861883052640 * α ^ 11 + 332584383792637363818110693156644176263245770 * α ^ 12 + 333049929303875184857821696251322094451555300 * α ^ 13 + 301880762905153988961008260011013859110924020 * α ^ 14 + 248778383542817950458457719347804130388393200 * α ^ 15 + 187098708657492312991354787006951375606496810 * α ^ 16 + 128821377534531366266108990532541378516293180 * α ^ 17 + 81419630849957631346647265524754482691775400 * α ^ 18 + 47345231058420765609063602657623737762737040 * α ^ 19 + 25377634631717199993415818405387727249820325 * α ^ 20 + 12558381461678887884336588690871882873720170 * α ^ 21 + 5744808624780589326694261819822529221060710 * α ^ 22 + 2431706095253331452737540626239749451182200 * α ^ 23 + 953157993950838580367703259303917955151865 * α ^ 24 + 346144642670223976596034179062502690180750 * α ^ 25 + 116495518414609472010567246197077176778320 * α ^ 26 + 36336281152740288609221052030650841399360 * α ^ 27 + 10502010275079971287850469706276099760700 * α ^ 28 + 2811408048396859598615803016678577566616 * α ^ 29 + 696637045577195749563697260889295071320 * α ^ 30 + 159631247175312590035611267009797954208 * α ^ 31 + 33785522480785269776966858820750983964 * α ^ 32 + 6594450665275339854415586104207300200 * α ^ 33 + 1184779969344702509178802875319571760 * α ^ 34 + 195478905533580848831244517654808400 * α ^ 35 + 29535092351319878473338799170306705 * α ^ 36 + 4072478636506932555839271140088690 * α ^ 37 + 510306927013451786184096375133350 * α ^ 38 + 57808428584128470185954723726040 * α ^ 39 + 5881482509330352987406470588525 * α ^ 40 + 532894392271418064251604942870 * α ^ 41 + 42515012647728027357611076360 * α ^ 42 + 2939585612233076406278632800 * α ^ 43 + 171946491190832176774496730 * α ^ 44 + 8163588014241841361016900 * α ^ 45 + 287999399301298111575540 * α ^ 46 + 5555726484083859953520 * α ^ 47 - 536551383276446293350 * α ^ 48 - 269167118332858968420 * α ^ 49 - 48279425158933803000 * α ^ 50 - 1759012112154436560 * α ^ 51 + 273395914772406495 * α ^ 52 + 6240162359537050 * α ^ 53 - 1129204084343291 * α ^ 54 + 41554143448524 * α ^ 55 - 721404477395 * α ^ 56 + 6229533730 * α ^ 57 - 21627837 * α ^ 58 := by
  have hu : (0 : ℝ) ≤ 17 - α := by linarith
  have h0 : (0:ℝ) ≤ 1122702787291394736448332031899900000000 * (17 - α) ^ 58 :=
    mul_nonneg (by norm_num) (pow_nonneg hu 58)
  have h1 : (0:ℝ) ≤ 388904288083346622931025909215729068000000 * α ^ 1 * (17 - α) ^ 57 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 1)) (pow_nonneg hu 57)
  have h2 : (0:ℝ) ≤ 66095616740335374779150673987010161532260000 * α ^ 2 * (17 - α) ^ 56 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 2)) (pow_nonneg hu 56)
  have h3 : (0:ℝ) ≤ 7345821640480281350499142140546658776321841200 * α ^ 3 * (17 - α) ^ 55 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 3)) (pow_nonneg hu 55)
  have h4 : (0:ℝ) ≤ 600398748030850807066041679815685800572608040199 * α ^ 4 * (17 - α) ^ 54 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 4)) (pow_nonneg hu 54)
  have h5 : (0:ℝ) ≤ 38479987967757849353019399973163199134827376858856 * α ^ 5 * (17 - α) ^ 53 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 5)) (pow_nonneg hu 53)
  have h6 : (0:ℝ) ≤ 2013648131786096177205150562840212460891734276215217 * α ^ 6 * (17 - α) ^ 52 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 6)) (pow_nonneg hu 52)
  have h7 : (0:ℝ) ≤ 88459088337848664272764574750756035751708812314589560 * α ^ 7 * (17 - α) ^ 51 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 7)) (pow_nonneg hu 51)
  have h8 : (0:ℝ) ≤ 3328752627388631431253304215842302161184427248710824200 * α ^ 8 * (17 - α) ^ 50 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 8)) (pow_nonneg hu 50)
  have h9 : (0:ℝ) ≤ 108955148579598077254581984889507974501857717600550300000 * α ^ 9 * (17 - α) ^ 49 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 9)) (pow_nonneg hu 49)
  have h10 : (0:ℝ) ≤ 3139320986827193043298955183356728835782414071606732250000 * α ^ 10 * (17 - α) ^ 48 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 10)) (pow_nonneg hu 48)
  have h11 : (0:ℝ) ≤ 80389849002074687648105368735226451202772917094058768000000 * α ^ 11 * (17 - α) ^ 47 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 11)) (pow_nonneg hu 47)
  have h12 : (0:ℝ) ≤ 1843869779817877110104286469976591396926664444962705440000000 * α ^ 12 * (17 - α) ^ 46 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 12)) (pow_nonneg hu 46)
  have h13 : (0:ℝ) ≤ 38126021284745149595963616317393007484187425284263404800000000 * α ^ 13 * (17 - α) ^ 45 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 13)) (pow_nonneg hu 45)
  have h14 : (0:ℝ) ≤ 714519722771974812940511821448225512188719319523829280000000000 * α ^ 14 * (17 - α) ^ 44 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 14)) (pow_nonneg hu 44)
  have h15 : (0:ℝ) ≤ 12192162072496626088921760868440507818256588279501222400000000000 * α ^ 15 * (17 - α) ^ 43 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 15)) (pow_nonneg hu 43)
  have h16 : (0:ℝ) ≤ 190149195298252798424521646382266997826378949113808102400000000000 * α ^ 16 * (17 - α) ^ 42 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 16)) (pow_nonneg hu 42)
  have h17 : (0:ℝ) ≤ 2719453325782140875058402865898661993411332371079473152000000000000 * α ^ 17 * (17 - α) ^ 41 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 17)) (pow_nonneg hu 41)
  have h18 : (0:ℝ) ≤ 35765156781668343145270939254204039481078844597447447040000000000000 * α ^ 18 * (17 - α) ^ 40 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 18)) (pow_nonneg hu 40)
  have h19 : (0:ℝ) ≤ 433581369383490123337920330591320005197369743601113088000000000000000 * α ^ 19 * (17 - α) ^ 39 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 19)) (pow_nonneg hu 39)
  have h20 : (0:ℝ) ≤ 4855120840322429070915669670313005676027625016591872000000000000000000 * α ^ 20 * (17 - α) ^ 38 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 20)) (pow_nonneg hu 38)
  have h21 : (0:ℝ) ≤ 50303800927352895844904371767120477621293024508175810560000000000000000 * α ^ 21 * (17 - α) ^ 37 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 21)) (pow_nonneg hu 37)
  have h22 : (0:ℝ) ≤ 482953904720497092819809519030958414936076990756461772800000000000000000 * α ^ 22 * (17 - α) ^ 36 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 22)) (pow_nonneg hu 36)
  have h23 : (0:ℝ) ≤ 4301697515309799266557277840727716853246295229412212736000000000000000000 * α ^ 23 * (17 - α) ^ 35 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 23)) (pow_nonneg hu 35)
  have h24 : (0:ℝ) ≤ 35582005974740842580199098139010545771216816653126860800000000000000000000 * α ^ 24 * (17 - α) ^ 34 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 24)) (pow_nonneg hu 34)
  have h25 : (0:ℝ) ≤ 273535549248031302586908863638264651412739231630163968000000000000000000000 * α ^ 25 * (17 - α) ^ 33 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 25)) (pow_nonneg hu 33)
  have h26 : (0:ℝ) ≤ 1955426273644204648009173651834541693843095232637140992000000000000000000000 * α ^ 26 * (17 - α) ^ 32 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 26)) (pow_nonneg hu 32)
  have h27 : (0:ℝ) ≤ 13004222926412994888311248631808734105341900865415413760000000000000000000000 * α ^ 27 * (17 - α) ^ 31 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 27)) (pow_nonneg hu 31)
  have h28 : (0:ℝ) ≤ 80470387643773112884644249468688475191473557588882227200000000000000000000000 * α ^ 28 * (17 - α) ^ 30 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 28)) (pow_nonneg hu 30)
  have h29 : (0:ℝ) ≤ 463355476918012102672652719197790300193712035699097600000000000000000000000000 * α ^ 29 * (17 - α) ^ 29 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 29)) (pow_nonneg hu 29)
  have h30 : (0:ℝ) ≤ 2482344082055683113128185595725000998635940934141870080000000000000000000000000 * α ^ 30 * (17 - α) ^ 28 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 30)) (pow_nonneg hu 28)
  have h31 : (0:ℝ) ≤ 12369353793584370842106405783534323328114720329863004160000000000000000000000000 * α ^ 31 * (17 - α) ^ 27 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 31)) (pow_nonneg hu 27)
  have h32 : (0:ℝ) ≤ 57300834405504520484711032055319485636127102860053708800000000000000000000000000 * α ^ 32 * (17 - α) ^ 26 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 32)) (pow_nonneg hu 26)
  have h33 : (0:ℝ) ≤ 246613403330189144932245957910378250136137902552252416000000000000000000000000000 * α ^ 33 * (17 - α) ^ 25 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 33)) (pow_nonneg hu 25)
  have h34 : (0:ℝ) ≤ 985246695411671462829426238732411673050896371023872000000000000000000000000000000 * α ^ 34 * (17 - α) ^ 24 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 34)) (pow_nonneg hu 24)
  have h35 : (0:ℝ) ≤ 3649974776445129628396257437653948413551102593597440000000000000000000000000000000 * α ^ 35 * (17 - α) ^ 23 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 35)) (pow_nonneg hu 23)
  have h36 : (0:ℝ) ≤ 12522828085409243337307923676013931236910302987550720000000000000000000000000000000 * α ^ 36 * (17 - α) ^ 22 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 36)) (pow_nonneg hu 22)
  have h37 : (0:ℝ) ≤ 39731340789062838384502107867195079108983927708057600000000000000000000000000000000 * α ^ 37 * (17 - α) ^ 21 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 37)) (pow_nonneg hu 21)
  have h38 : (0:ℝ) ≤ 116365100653574128528674694068315721419971773857792000000000000000000000000000000000 * α ^ 38 * (17 - α) ^ 20 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 38)) (pow_nonneg hu 20)
  have h39 : (0:ℝ) ≤ 313971050757264181615490913824916376724876505907200000000000000000000000000000000000 * α ^ 39 * (17 - α) ^ 19 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 39)) (pow_nonneg hu 19)
  have h40 : (0:ℝ) ≤ 778602881203434272472350446775468799876667539456000000000000000000000000000000000000 * α ^ 40 * (17 - α) ^ 18 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 40)) (pow_nonneg hu 18)
  have h41 : (0:ℝ) ≤ 1769823234178269115425193251412793044953817153536000000000000000000000000000000000000 * α ^ 41 * (17 - α) ^ 17 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 41)) (pow_nonneg hu 17)
  have h42 : (0:ℝ) ≤ 3676061908648613727975384722760757591726652129280000000000000000000000000000000000000 * α ^ 42 * (17 - α) ^ 16 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 42)) (pow_nonneg hu 16)
  have h43 : (0:ℝ) ≤ 6952202666310032877475473290777345311129573785600000000000000000000000000000000000000 * α ^ 43 * (17 - α) ^ 15 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 43)) (pow_nonneg hu 15)
  have h44 : (0:ℝ) ≤ 11922241592723733002313059523572394705939333120000000000000000000000000000000000000000 * α ^ 44 * (17 - α) ^ 14 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 44)) (pow_nonneg hu 14)
  have h45 : (0:ℝ) ≤ 18450845478651168634684539530259247984017408000000000000000000000000000000000000000000 * α ^ 45 * (17 - α) ^ 13 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 45)) (pow_nonneg hu 13)
  have h46 : (0:ℝ) ≤ 25626302281194153741004424813630605199042150400000000000000000000000000000000000000000 * α ^ 46 * (17 - α) ^ 12 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 46)) (pow_nonneg hu 12)
  have h47 : (0:ℝ) ≤ 31735356381499745521943376637135285074788352000000000000000000000000000000000000000000 * α ^ 47 * (17 - α) ^ 11 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 47)) (pow_nonneg hu 11)
  have h48 : (0:ℝ) ≤ 34773986078859125604170241648646078618789153800477215677912265790935664780750000000000 * α ^ 48 * (17 - α) ^ 10 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 48)) (pow_nonneg hu 10)
  have h49 : (0:ℝ) ≤ 33406510810664082686608872230111026353099051641531587806834322064288344554180000000000 * α ^ 49 * (17 - α) ^ 9 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 49)) (pow_nonneg hu 9)
  have h50 : (0:ℝ) ≤ 27820946523539616021999756980494999341031737804699133246948994617042670678045550000000 * α ^ 50 * (17 - α) ^ 8 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 50)) (pow_nonneg hu 8)
  have h51 : (0:ℝ) ≤ 19791944456596303161181417657916215477628661862047060146272089595047078222827061000000 * α ^ 51 * (17 - α) ^ 7 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 51)) (pow_nonneg hu 7)
  have h52 : (0:ℝ) ≤ 11779484527176566489160923853925282151874607361320815965499241151163816336970531507500 * α ^ 52 * (17 - α) ^ 6 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 52)) (pow_nonneg hu 6)
  have h53 : (0:ℝ) ≤ 5685451710206041407628952698706724254113808400301600724661558108213464738446593549500 * α ^ 53 * (17 - α) ^ 5 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 53)) (pow_nonneg hu 5)
  have h54 : (0:ℝ) ≤ 2124220422337628714954562682925792634155465583908214661397004639843167881489238854787 * α ^ 54 * (17 - α) ^ 4 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 54)) (pow_nonneg hu 4)
  have h55 : (0:ℝ) ≤ 572909076732572616057605734230328840239193993814061157407956440967916397115623518120 * α ^ 55 * (17 - α) ^ 3 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 55)) (pow_nonneg hu 3)
  have h56 : (0:ℝ) ≤ 99530623246032452139763064572679576747235355843313027086842616874975359183988464200 * α ^ 56 * (17 - α) ^ 2 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 56)) (pow_nonneg hu 2)
  have h57 : (0:ℝ) ≤ 8820861539641882551843091227900257872626927159038875775406157756108783934565132000 * α ^ 57 * (17 - α) ^ 1 :=
    mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 57)) (pow_nonneg hu 1)
  have h58 : (0:ℝ) ≤ 161598081294237579548393327166198311182821276785721838823669379905701080186270000 * α ^ 58 :=
    mul_nonneg (by norm_num) (pow_nonneg hα 58)
  have hid : (17 : ℝ) ^ 58 * (1122702787291394736448332031899900000000 + 19046325083555631071589567727384404000000 * α + 158421799401305511319831453323336122340000 * α ^ 2 + 861086144839783899262522290902928965732400 * α ^ 3 + 3439408019860839882261371580238947745811319 * α ^ 4 + 10763976190978343059270128976319908699279230 * α ^ 5 + 27482264870203746404049226779511973140100922 * α ^ 6 + 58851751350273881387953189525455032864879976 * α ^ 7 + 107855247587877306122230293103712405510570475 * α ^ 8 + 171759728691636266490365540891679381811794330 * α ^ 9 + 240529488382582584529650966973246412375404200 * α ^ 10 + 299026713527922503750214218383542861883052640 * α ^ 11 + 332584383792637363818110693156644176263245770 * α ^ 12 + 333049929303875184857821696251322094451555300 * α ^ 13 + 301880762905153988961008260011013859110924020 * α ^ 14 + 248778383542817950458457719347804130388393200 * α ^ 15 + 187098708657492312991354787006951375606496810 * α ^ 16 + 128821377534531366266108990532541378516293180 * α ^ 17 + 81419630849957631346647265524754482691775400 * α ^ 18 + 47345231058420765609063602657623737762737040 * α ^ 19 + 25377634631717199993415818405387727249820325 * α ^ 20 + 12558381461678887884336588690871882873720170 * α ^ 21 + 5744808624780589326694261819822529221060710 * α ^ 22 + 2431706095253331452737540626239749451182200 * α ^ 23 + 953157993950838580367703259303917955151865 * α ^ 24 + 346144642670223976596034179062502690180750 * α ^ 25 + 116495518414609472010567246197077176778320 * α ^ 26 + 36336281152740288609221052030650841399360 * α ^ 27 + 10502010275079971287850469706276099760700 * α ^ 28 + 2811408048396859598615803016678577566616 * α ^ 29 + 696637045577195749563697260889295071320 * α ^ 30 + 159631247175312590035611267009797954208 * α ^ 31 + 33785522480785269776966858820750983964 * α ^ 32 + 6594450665275339854415586104207300200 * α ^ 33 + 1184779969344702509178802875319571760 * α ^ 34 + 195478905533580848831244517654808400 * α ^ 35 + 29535092351319878473338799170306705 * α ^ 36 + 4072478636506932555839271140088690 * α ^ 37 + 510306927013451786184096375133350 * α ^ 38 + 57808428584128470185954723726040 * α ^ 39 + 5881482509330352987406470588525 * α ^ 40 + 532894392271418064251604942870 * α ^ 41 + 42515012647728027357611076360 * α ^ 42 + 2939585612233076406278632800 * α ^ 43 + 171946491190832176774496730 * α ^ 44 + 8163588014241841361016900 * α ^ 45 + 287999399301298111575540 * α ^ 46 + 5555726484083859953520 * α ^ 47 - 536551383276446293350 * α ^ 48 - 269167118332858968420 * α ^ 49 - 48279425158933803000 * α ^ 50 - 1759012112154436560 * α ^ 51 + 273395914772406495 * α ^ 52 + 6240162359537050 * α ^ 53 - 1129204084343291 * α ^ 54 + 41554143448524 * α ^ 55 - 721404477395 * α ^ 56 + 6229533730 * α ^ 57 - 21627837 * α ^ 58) = 1122702787291394736448332031899900000000 * (17 - α) ^ 58 + 388904288083346622931025909215729068000000 * α ^ 1 * (17 - α) ^ 57 + 66095616740335374779150673987010161532260000 * α ^ 2 * (17 - α) ^ 56 + 7345821640480281350499142140546658776321841200 * α ^ 3 * (17 - α) ^ 55 + 600398748030850807066041679815685800572608040199 * α ^ 4 * (17 - α) ^ 54 + 38479987967757849353019399973163199134827376858856 * α ^ 5 * (17 - α) ^ 53 + 2013648131786096177205150562840212460891734276215217 * α ^ 6 * (17 - α) ^ 52 + 88459088337848664272764574750756035751708812314589560 * α ^ 7 * (17 - α) ^ 51 + 3328752627388631431253304215842302161184427248710824200 * α ^ 8 * (17 - α) ^ 50 + 108955148579598077254581984889507974501857717600550300000 * α ^ 9 * (17 - α) ^ 49 + 3139320986827193043298955183356728835782414071606732250000 * α ^ 10 * (17 - α) ^ 48 + 80389849002074687648105368735226451202772917094058768000000 * α ^ 11 * (17 - α) ^ 47 + 1843869779817877110104286469976591396926664444962705440000000 * α ^ 12 * (17 - α) ^ 46 + 38126021284745149595963616317393007484187425284263404800000000 * α ^ 13 * (17 - α) ^ 45 + 714519722771974812940511821448225512188719319523829280000000000 * α ^ 14 * (17 - α) ^ 44 + 12192162072496626088921760868440507818256588279501222400000000000 * α ^ 15 * (17 - α) ^ 43 + 190149195298252798424521646382266997826378949113808102400000000000 * α ^ 16 * (17 - α) ^ 42 + 2719453325782140875058402865898661993411332371079473152000000000000 * α ^ 17 * (17 - α) ^ 41 + 35765156781668343145270939254204039481078844597447447040000000000000 * α ^ 18 * (17 - α) ^ 40 + 433581369383490123337920330591320005197369743601113088000000000000000 * α ^ 19 * (17 - α) ^ 39 + 4855120840322429070915669670313005676027625016591872000000000000000000 * α ^ 20 * (17 - α) ^ 38 + 50303800927352895844904371767120477621293024508175810560000000000000000 * α ^ 21 * (17 - α) ^ 37 + 482953904720497092819809519030958414936076990756461772800000000000000000 * α ^ 22 * (17 - α) ^ 36 + 4301697515309799266557277840727716853246295229412212736000000000000000000 * α ^ 23 * (17 - α) ^ 35 + 35582005974740842580199098139010545771216816653126860800000000000000000000 * α ^ 24 * (17 - α) ^ 34 + 273535549248031302586908863638264651412739231630163968000000000000000000000 * α ^ 25 * (17 - α) ^ 33 + 1955426273644204648009173651834541693843095232637140992000000000000000000000 * α ^ 26 * (17 - α) ^ 32 + 13004222926412994888311248631808734105341900865415413760000000000000000000000 * α ^ 27 * (17 - α) ^ 31 + 80470387643773112884644249468688475191473557588882227200000000000000000000000 * α ^ 28 * (17 - α) ^ 30 + 463355476918012102672652719197790300193712035699097600000000000000000000000000 * α ^ 29 * (17 - α) ^ 29 + 2482344082055683113128185595725000998635940934141870080000000000000000000000000 * α ^ 30 * (17 - α) ^ 28 + 12369353793584370842106405783534323328114720329863004160000000000000000000000000 * α ^ 31 * (17 - α) ^ 27 + 57300834405504520484711032055319485636127102860053708800000000000000000000000000 * α ^ 32 * (17 - α) ^ 26 + 246613403330189144932245957910378250136137902552252416000000000000000000000000000 * α ^ 33 * (17 - α) ^ 25 + 985246695411671462829426238732411673050896371023872000000000000000000000000000000 * α ^ 34 * (17 - α) ^ 24 + 3649974776445129628396257437653948413551102593597440000000000000000000000000000000 * α ^ 35 * (17 - α) ^ 23 + 12522828085409243337307923676013931236910302987550720000000000000000000000000000000 * α ^ 36 * (17 - α) ^ 22 + 39731340789062838384502107867195079108983927708057600000000000000000000000000000000 * α ^ 37 * (17 - α) ^ 21 + 116365100653574128528674694068315721419971773857792000000000000000000000000000000000 * α ^ 38 * (17 - α) ^ 20 + 313971050757264181615490913824916376724876505907200000000000000000000000000000000000 * α ^ 39 * (17 - α) ^ 19 + 778602881203434272472350446775468799876667539456000000000000000000000000000000000000 * α ^ 40 * (17 - α) ^ 18 + 1769823234178269115425193251412793044953817153536000000000000000000000000000000000000 * α ^ 41 * (17 - α) ^ 17 + 3676061908648613727975384722760757591726652129280000000000000000000000000000000000000 * α ^ 42 * (17 - α) ^ 16 + 6952202666310032877475473290777345311129573785600000000000000000000000000000000000000 * α ^ 43 * (17 - α) ^ 15 + 11922241592723733002313059523572394705939333120000000000000000000000000000000000000000 * α ^ 44 * (17 - α) ^ 14 + 18450845478651168634684539530259247984017408000000000000000000000000000000000000000000 * α ^ 45 * (17 - α) ^ 13 + 25626302281194153741004424813630605199042150400000000000000000000000000000000000000000 * α ^ 46 * (17 - α) ^ 12 + 31735356381499745521943376637135285074788352000000000000000000000000000000000000000000 * α ^ 47 * (17 - α) ^ 11 + 34773986078859125604170241648646078618789153800477215677912265790935664780750000000000 * α ^ 48 * (17 - α) ^ 10 + 33406510810664082686608872230111026353099051641531587806834322064288344554180000000000 * α ^ 49 * (17 - α) ^ 9 + 27820946523539616021999756980494999341031737804699133246948994617042670678045550000000 * α ^ 50 * (17 - α) ^ 8 + 19791944456596303161181417657916215477628661862047060146272089595047078222827061000000 * α ^ 51 * (17 - α) ^ 7 + 11779484527176566489160923853925282151874607361320815965499241151163816336970531507500 * α ^ 52 * (17 - α) ^ 6 + 5685451710206041407628952698706724254113808400301600724661558108213464738446593549500 * α ^ 53 * (17 - α) ^ 5 + 2124220422337628714954562682925792634155465583908214661397004639843167881489238854787 * α ^ 54 * (17 - α) ^ 4 + 572909076732572616057605734230328840239193993814061157407956440967916397115623518120 * α ^ 55 * (17 - α) ^ 3 + 99530623246032452139763064572679576747235355843313027086842616874975359183988464200 * α ^ 56 * (17 - α) ^ 2 + 8820861539641882551843091227900257872626927159038875775406157756108783934565132000 * α ^ 57 * (17 - α) ^ 1 + 161598081294237579548393327166198311182821276785721838823669379905701080186270000 * α ^ 58 := by
    ring
  rcases le_total α (17 / 2) with h | h
  · have hpos : (0 : ℝ) < 1122702787291394736448332031899900000000 * (17 - α) ^ 58 :=
      mul_pos (by norm_num) (pow_pos (by linarith) 58)
    linarith
  · have hpos : (0 : ℝ) < 161598081294237579548393327166198311182821276785721838823669379905701080186270000 * α ^ 58 :=
      mul_pos (by norm_num) (pow_pos (by linarith) 58)
    linarith

set_option maxHeartbeats 4000000 in
/-- **The bound in `α` alone is below `1`.** -/
theorem Ut_lt_one (hα : 0 ≤ α) (hα' : α ≤ 17) : Ut α < 1 := by
  have h3 : (0 : ℝ) < 3 + α := three_add_pos hα
  have hg : (0 : ℝ) < 300 + 47 * α - α ^ 2 := by nlinarith
  have hgne : (300 : ℝ) + 47 * α - α ^ 2 ≠ 0 := hg.ne'
  have hc : c 101 α = (300 + 47 * α - α ^ 2) / (100 * (3 + α)) := by
    simp only [c, M]
    norm_num
    field_simp
    ring
  have hT1 : T1 101 α
      = 1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3 / (721 * (300 + 47 * α - α ^ 2) ^ 4) := by
    simp only [T1, hc]
    norm_num
    field_simp
    ring
  -- `(α/(3+α)) ^ 48` cancels against `(3+α) ^ 49` without expanding either
  have h48 : (α / (3 + α)) ^ 48 * (3 + α) ^ 49 = α ^ 48 * (3 + α) := by
    rw [div_pow, show (3 + α) ^ 49 = (3 + α) ^ 48 * (3 + α) from by ring, ← mul_assoc,
      div_mul_cancel₀ _ (pow_ne_zero 48 h3.ne')]
  -- the six terms of `Ut`, each multiplied by `D`
  have t1 : (1 / 6 : ℝ) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 144200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4 := by
    ring
  have t2 : 1 / (4 * (3 + α)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 216300 * (3 + α) ^ 48 * (300 + 47 * α - α ^ 2) ^ 4 := by
    field_simp
    ring
  have t3 : (1 / 200 : ℝ) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 4326 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4 := by
    ring
  have t4 : 1 / (400 * (3 + α)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 2163 * (3 + α) ^ 48 * (300 + 47 * α - α ^ 2) ^ 4 := by
    field_simp
    ring
  have t5 : 101 / 100 * (1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3
        / (721 * (300 + 47 * α - α ^ 2) ^ 4)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4)
      = 1939200000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 52 := by
    -- cancel the γ⁴ syntactically; `field_simp` leaves a stray γ⁻¹ here
    have hne : (721 : ℝ) * (300 + 47 * α - α ^ 2) ^ 4 ≠ 0 :=
      mul_ne_zero (by norm_num) (pow_ne_zero 4 hg.ne')
    rw [show 101 / 100 * (1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3
            / (721 * (300 + 47 * α - α ^ 2) ^ 4)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4)
          = 1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3
              / (721 * (300 + 47 * α - α ^ 2) ^ 4) * (721 * (300 + 47 * α - α ^ 2) ^ 4)
              * (1212 * (3 + α) ^ 49) from by ring,
      div_mul_cancel₀ _ hne]
    ring
  have t6 : (100 - 2 * α) ^ 2 / 100 * 101 * 99 / (16 * (3 + α)) * (α / (3 + α)) ^ 48
        * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4)
      = (21627837 / 4) * (100 - 2 * α) ^ 2 * α ^ 48 * (300 + 47 * α - α ^ 2) ^ 4 := by
    rw [show (100 - 2 * α) ^ 2 / 100 * 101 * 99 / (16 * (3 + α)) * (α / (3 + α)) ^ 48
          * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4)
        = ((100 - 2 * α) ^ 2 / 100 * 101 * 99 / (16 * (3 + α)) * (865200 * (300 + 47 * α - α ^ 2) ^ 4))
          * ((α / (3 + α)) ^ 48 * (3 + α) ^ 49) from by ring, h48]
    field_simp
    ring
  have hD : (0 : ℝ) < 865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4 := by
    have h49 := pow_pos h3 49
    have hg4 := pow_pos hg 4
    positivity
  have hmul : (1 - Ut α) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 1122702787291394736448332031899900000000 + 19046325083555631071589567727384404000000 * α + 158421799401305511319831453323336122340000 * α ^ 2 + 861086144839783899262522290902928965732400 * α ^ 3 + 3439408019860839882261371580238947745811319 * α ^ 4 + 10763976190978343059270128976319908699279230 * α ^ 5 + 27482264870203746404049226779511973140100922 * α ^ 6 + 58851751350273881387953189525455032864879976 * α ^ 7 + 107855247587877306122230293103712405510570475 * α ^ 8 + 171759728691636266490365540891679381811794330 * α ^ 9 + 240529488382582584529650966973246412375404200 * α ^ 10 + 299026713527922503750214218383542861883052640 * α ^ 11 + 332584383792637363818110693156644176263245770 * α ^ 12 + 333049929303875184857821696251322094451555300 * α ^ 13 + 301880762905153988961008260011013859110924020 * α ^ 14 + 248778383542817950458457719347804130388393200 * α ^ 15 + 187098708657492312991354787006951375606496810 * α ^ 16 + 128821377534531366266108990532541378516293180 * α ^ 17 + 81419630849957631346647265524754482691775400 * α ^ 18 + 47345231058420765609063602657623737762737040 * α ^ 19 + 25377634631717199993415818405387727249820325 * α ^ 20 + 12558381461678887884336588690871882873720170 * α ^ 21 + 5744808624780589326694261819822529221060710 * α ^ 22 + 2431706095253331452737540626239749451182200 * α ^ 23 + 953157993950838580367703259303917955151865 * α ^ 24 + 346144642670223976596034179062502690180750 * α ^ 25 + 116495518414609472010567246197077176778320 * α ^ 26 + 36336281152740288609221052030650841399360 * α ^ 27 + 10502010275079971287850469706276099760700 * α ^ 28 + 2811408048396859598615803016678577566616 * α ^ 29 + 696637045577195749563697260889295071320 * α ^ 30 + 159631247175312590035611267009797954208 * α ^ 31 + 33785522480785269776966858820750983964 * α ^ 32 + 6594450665275339854415586104207300200 * α ^ 33 + 1184779969344702509178802875319571760 * α ^ 34 + 195478905533580848831244517654808400 * α ^ 35 + 29535092351319878473338799170306705 * α ^ 36 + 4072478636506932555839271140088690 * α ^ 37 + 510306927013451786184096375133350 * α ^ 38 + 57808428584128470185954723726040 * α ^ 39 + 5881482509330352987406470588525 * α ^ 40 + 532894392271418064251604942870 * α ^ 41 + 42515012647728027357611076360 * α ^ 42 + 2939585612233076406278632800 * α ^ 43 + 171946491190832176774496730 * α ^ 44 + 8163588014241841361016900 * α ^ 45 + 287999399301298111575540 * α ^ 46 + 5555726484083859953520 * α ^ 47 - 536551383276446293350 * α ^ 48 - 269167118332858968420 * α ^ 49 - 48279425158933803000 * α ^ 50 - 1759012112154436560 * α ^ 51 + 273395914772406495 * α ^ 52 + 6240162359537050 * α ^ 53 - 1129204084343291 * α ^ 54 + 41554143448524 * α ^ 55 - 721404477395 * α ^ 56 + 6229533730 * α ^ 57 - 21627837 * α ^ 58 := by
    rw [Ut, hT1, sub_mul, one_mul, add_mul, add_mul, add_mul, add_mul, add_mul,
      t1, t2, t3, t4, t5, t6]
    ring
  rw [← sub_pos]
  have hF := F_pos hα hα'
  nlinarith [hmul, hF, hD]

/-- **The large-degree claim.**  Every degree `n ≥ 101`. -/
theorem large_degree {n : ℕ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17)
    (hfeas : c n α ^ 2 ≤ A n α) : R n α < 1 := by
  have hcpos : (0 : ℝ) < c n α := by
    have := c_ge_of_large hn hα hα'
    linarith
  exact lt_of_le_of_lt
    (le_trans (R_le_U (by omega) hα hfeas hcpos) (U_le_Ut hn hα hα'))
    (Ut_lt_one hα hα')

end Sendov
