module

public import Rupert.Basic
public import Rupert.Convex
public import Rupert.FinCases
public meta import Rupert.MatrixSimps
public import Rupert.Quaternion
public import Rupert.Equivalences.RupertEquivRupertPrime

@[expose] public section

/- Tom7's "nopert" #214 (https://tom7.org/ruperts/) is Rupert after all.

   The vertices below are the twenty published STL coordinates, read as
   exact rationals.  The polyhedron is (up to the printed precision) the
   orbit of its first four vertices under rotation by 72° about the z
   axis.  Its Rupert passage is astronomically tight: the inner shadow
   clears the outer shadow boundary by about 1.8e-8, tight enough to elude
   tom7's stochastic search.

   The witness pose was found by following a failing formal *non*-Rupert
   proof attempt (in the Noperthedron project) to the exact spot where
   its local certificate margins crossed zero. -/

namespace Nopert214

open scoped Matrix

private theorem sum_univ_twenty {β : Type} [AddCommMonoid β] (f : Fin 20 → β) :
    ∑ i, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8 + f 9 +
      f 10 + f 11 + f 12 + f 13 + f 14 + f 15 + f 16 + f 17 + f 18 + f 19 := by
  repeat rw [Fin.sum_univ_castSucc]
  simp only [Finset.univ_eq_empty, Finset.sum_empty, zero_add]
  rfl

noncomputable def vertices : Fin 20 → ℝ³ :=
  ![
    !₂[0.5542570167628148, 0.13498214234883502, 0.5670539264866502],
    !₂[0.839503072954794, 0.4526456900329921, 0.3005768949769993],
    !₂[0.7619849874129984, 0.5429603653859462, -0.04074876955046458],
    !₂[0.591853727475924, 0.13110932665305655, -0.7653829489805983],
    !₂[0.04289919136693016, 0.5688415234175154, 0.5670539264866502],
    !₂[-0.17107091670577093, 0.9382900786342319, 0.3005768949769993],
    !₂[-0.2809196830211049, 0.8924747677745009, -0.04074876955046458],
    !₂[0.05820048051375984, 0.6034013542664042, -0.7653829489805983],
    !₂[-0.5277438584081657, 0.2165812533354586, 0.5670539264866502],
    !₂[-0.9452307139655625, 0.1272494698697746, 0.3005768949769993],
    !₂[-0.9356028996288878, 0.008619375200364626, -0.04074876955046458],
    !₂[-0.5558838523568445, 0.2418132191412975, -0.7653829489805983],
    !₂[-0.36906283321718863, -0.4349869475301504, 0.5670539264866502],
    !₂[-0.41311379173527674, -0.8596455812043055, 0.3005768949769993],
    !₂[-0.2973147089225043, -0.8871477009388876, -0.04074876955046458],
    !₂[-0.40175559506751807, -0.45395256590805566, -0.7653829489805983],
    !₂[0.29965048349560947, -0.4854179715716587, 0.5670539264866502],
    !₂[0.6899123494518161, -0.6585396573326932, 0.3005768949769993],
    !₂[0.7518523041594987, -0.5569068074219243, -0.04074876955046458],
    !₂[0.3075852394346786, -0.5223713341527026, -0.7653829489805983]]

def inner_quat : Quaternion ℝ :=
  ⟨0.513409524171, -0.357274843179, -0.445838043814, -0.640307571101⟩

def inner_offset : ℝ² := !₂[-0.000068618674499, 0.00004658859372]

def outer_quat : Quaternion ℝ :=
  ⟨0.513670889522, -0.357385492934, -0.445478171674, -0.640286674279⟩

noncomputable def inner_rot := matrix_of_quat inner_quat

lemma inner_rot_so3 : inner_rot ∈ SO3 := by
  have h : inner_quat.normSq ≠ 0 := by
    norm_num [inner_quat, Quaternion.normSq_def]
  exact matrix_of_quat_is_s03 h

noncomputable def outer_rot := matrix_of_quat outer_quat

lemma outer_rot_so3 : outer_rot ∈ SO3 := by
  have h : outer_quat.normSq ≠ 0 := by
    norm_num [outer_quat, Quaternion.normSq_def]
  exact matrix_of_quat_is_s03 h

set_option maxHeartbeats 16000000 in
theorem rupert : IsRupert vertices := by
  rw [rupert_iff_rupert']
  use inner_rot, inner_rot_so3, inner_offset, outer_rot, outer_rot_so3
  intro inner_shadow outer_shadow
  let ε₀ : ℝ := 1/20
  have hε₀ : ε₀ ∈ Set.Ioo 0 1 := by norm_num
  have hb : Metric.ball 0 ε₀ ⊆ convexHull ℝ outer_shadow := by
    refine Convex.ball_in_hull_of_corners_in_hull hε₀ ?_ ?_ ?_ ?_ <;>
      apply mem_convexHull_iff_exists_fintype.mpr <;>
      use Fin 20, Fin.fintype 20
  <;> [
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          237815257157828420210236963925270048667785457003896330525/752977974707565513995623989966686078640577859246698540547,
          278070583987879755791721149886689055001797903373812341837/752977974707565513995623989966686078640577859246698540547,
          0,
          0,
          0,
          0,
          0,
          237092133561857337993665876154726974970994498868989868185/752977974707565513995623989966686078640577859246698540547,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          42417018702820227123283772237281895191844189886837066611/129254271613160451419408577707675095749102687904270738802,
          0,
          21056358921630973943822305916890863592459161995004762181/64627135806580225709704288853837547874551343952135369401,
          0,
          0,
          0,
          0,
          0,
          44724535067078276408480193636611473372340174027424147829/129254271613160451419408577707675095749102687904270738802,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          1071356924497169599060868027691320793869633089816445619593/3123634563231684770933248948266122562149673172502015740466,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          501153087954226471078697056453190287786428797665184418042/1561817281615842385466624474133061281074836586251007870233,
          1049971462826062229714986807668421192707182487355201284789/3123634563231684770933248948266122562149673172502015740466,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          493329149517741785327585328798531860618193067276300113030/1497708018952248912282026219053482361240366723505356980757,
          0,
          1458797791965717353841813163356870136986635379115452591154/4493124056856746736846078657160447083721100170516070942271,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          1554338816337804027021509507407981364879885589571718012027/4493124056856746736846078657160447083721100170516070942271,
          0,
          0,
          0,
          0,
          0,
          0]
  ]
    all_goals
      use fun i ↦ proj_xy (outer_rot.toEuclideanLin (vertices i))
      refine ⟨?_, ?_, ?_, ?_⟩
      · apply all_fin_20_vec <;> norm_num
      · simp only [sum_univ_twenty, Matrix.cons_val]; norm_num
      · exact fun i ↦ ⟨i, rfl⟩
      · simp only [proj_xy, outer_rot, matrix_of_quat, outer_quat, vertices,
                   sum_univ_twenty, ε₀, matrix_simps]
        ext i; fin_cases i <;> norm_num
  intro v hv
  let ε₁ : ℝ := 1/100000000000
  have hε₁ : ε₁ ∈ Set.Ioo 0 1 := by norm_num
  refine Convex.mem_interior_hull hε₀.1 hε₁ hb ?_
  simp only [inner_shadow] at hv
  obtain ⟨y, hy⟩ := hv
  rw [mem_convexHull_iff_exists_fintype]
  fin_cases y <;>
    simp only [vertices, Fin.reduceFinMk, Matrix.cons_val] at hy <;>
    use Fin 20, Fin.fintype 20
  <;> [
    use ![0,
          1231685023754697378065682637953882284812822323789887478992612437140666364800860928128919076/3588583333189680175876466621302598052071493139730528645193738718499174618129338900563811575,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          1139714435315636046443352747527186564670701891761764372648264935792018023253209758386124949/3588583333189680175876466621302598052071493139730528645193738718499174618129338900563811575,
          0,
          0,
          0,
          0,
          0,
          0,
          48687354964773870054697249432861168103518756967155071742114453822659609203010728561950702/143543333327587207035058664852103922082859725589221145807749548739966984725173556022552463,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          179136015852723588468853983195405924358961450978488861169906602716480502004126853010962690355/532206275423991698462702129992276048722101077349760691742715085930682846582654690083433268462,
          0,
          0,
          0,
          0,
          59981912765099611568130580892641759551073094547211145090109693739935944259857540597834294669/177402091807997232820900709997425349574033692449920230580905028643560948860884896694477756154,
          0,
          0,
          0,
          0,
          86562260637984637644728202059472422854960171364819197651239700997197255899477607639483847050/266103137711995849231351064996138024361050538674880345871357542965341423291327345041716634231,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          74803048251160362227266686674157982104191590623887175230955004939565272087894598406369961165/191407106473107873328925427074335292917339965453216345775569443942497092649741046487535704786,
          0,
          0,
          0,
          0,
          58217074320237799034101831071083110090711026603853996626300958154233223985246821602198049521/191407106473107873328925427074335292917339965453216345775569443942497092649741046487535704786,
          0,
          0,
          0,
          29193491950854856033778454664547100361218674112737586959156740424349298288299813239483847050/95703553236553936664462713537167646458669982726608172887784721971248546324870523243767852393,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          8383889320330561381252684182533052945473572682623038826508940662686661932178602539184028020/8395561221810716520979401323839688587282509582606247982479024035496094011854306773887661811,
          0,
          0,
          0,
          174242746661360844148518711022470620458130079456397353152400558219701187859308082444565/399788629610034120046638158278080408918214742028868951546620192166480667231157465423221991,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          8012803800266561999598248375163758779316168314624811553882961086818354730658764972297926/8395561221810716520979401323839688587282509582606247982479024035496094011854306773887661811];
    use ![0,
          0,
          0,
          0,
          0,
          14853880319826111466297071123340110650390714630341421815551732463434924683462534928210661718/28812751159852278696295211276964420108031489611582858166356179091784114234954824942663872241,
          0,
          0,
          3169893375637251920102563064146143616901292396889839304832841043339075018865516377080010237/9604250386617426232098403758988140036010496537194286055452059697261371411651608314221290747,
          0,
          0,
          0,
          4449190713114411469690450961185878606936897790571918436305923498331964494895740883213179812/28812751159852278696295211276964420108031489611582858166356179091784114234954824942663872241,
          0,
          0,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          489877065752454407560972122834918125411769057347607381131929552760452784654622954434/247177851221956038418908747285791263259596647517930473412926256807077260000782870591250185,
          2223981854178656225721496665096224102461312864793075464137806333161537989349309649049983102/2224600660997604345770178725572121369336369827661374260716336311263695340007045835321251665,
          0,
          0,
          614397925356347959014011726791752611928256946782668112099790736182506582674294664678657/2224600660997604345770178725572121369336369827661374260716336311263695340007045835321251665,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          13670372663927133574409253435791293886595424162328148517643722390644501332016296147156/1980970019241505155405975370804355934823572003737661991936573959192342713508959677635245013,
          41599986925188391195952646369947680638753129969733637238794538415817150180265659534004695210/41600370404071608263525482786891474631295012078490901830668053143039196983688153230340145273,
          7415465944199828290294047818644259251046526911976981126477619372559145732411855104599/3200028492620892943348114060530113433176539390653146294666773318695322844899088710026165021,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          15243702554733182051232643995805382226678381423334886552381151799185628322401325310772/16791122443621436870271758785826211901939913921506250160269989654807851596171861832746170269,
          0,
          0,
          0,
          16791087262258324789030170547705118827175343509595739601128720522673787626600118801476263645/16791122443621436870271758785826211901939913921506250160269989654807851596171861832746170269,
          0,
          0,
          0,
          19937660557348059537005477097269382343733529087224254716750982264783943420629944595852/16791122443621436870271758785826211901939913921506250160269989654807851596171861832746170269,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          683516884014883752080053480115590830427630797849313286504459710162472783241606589906/2224600660997604345770178725572121369336369827661374260716336311263695340007045835321251665,
          408751259885822896553976277886320393393372373054462303204638806574294971163849049983102/2224600660997604345770178725572121369336369827661374260716336311263695340007045835321251665,
          0,
          0,
          2224191226220834507989872669240754933352146027657521949099845167997410882563098744664678657/2224600660997604345770178725572121369336369827661374260716336311263695340007045835321251665,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          296741396707489135700742732121396154179357916267090198899773013939697001505054649052637466/1252728311297925160708487446824540004697021287460124268102442569208004966737166301854950967,
          0,
          0,
          76168391229693534047406467712263706865660926189770455306171175304821695887831498218550873/139192034588658351189831938536060000521891254162236029789160285467556107415240700206105663,
          0,
          0,
          0,
          270471393523194218581086505292770488726715035485099971447128977524912702241628168835355644/1252728311297925160708487446824540004697021287460124268102442569208004966737166301854950967,
          0,
          0,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          28766369505012643646020162159863802399570773075545960424084670694676881599906295812618531/85929890166028720122782961880294079731863346318425565354164377282293290942417350701594920,
          3409361410073704800442909079136449217367713010449399330989943558833203363376728597509899759/10698271325670575655286478754096612926616986616643982886593464971645514722330960162348567540,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          7414993824445593441828118972114240621005424716578222965609959822650079199531795472335321343/21396542651341151310572957508193225853233973233287965773186929943291029444661920324697135080,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          4844797321370980423208621349113680072341471191363925246413720573925204755827719414577132850/15912365645605781481520555367414107391612408354491060824886806731730523007777567540184753897,
          6545893470227073175616010206496843467966153341812639037782036660776584044788703613385510680/15912365645605781481520555367414107391612408354491060824886806731730523007777567540184753897,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          1507224951335909294231974603934527950434927940438165513563683165676244735720381504074036789/5304121881868593827173518455804702463870802784830353608295602243910174335925855846728251299];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          1681139420274149644298347948740777666794493526853013306582722347659898688231936215696691/4470558170676475949882229677262920749198378637804356442294952519805273502172257757461520039,
          0,
          0,
          0,
          13401785506455093617737698330153943788926873262487914073149047852973508147770559635526808326/13411674512029427849646689031788762247595135913413069326884857559415820506516773272384560117,
          4845587313511782976095657788596125667879170344596213816061539399332662681517828210661718/13411674512029427849646689031788762247595135913413069326884857559415820506516773272384560117,
          0,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          17811095458451350927470826289396209329951103864821457581095281324870980345951667266728458/22358413730977189141387780010536211064863691774996259258902764122552048503676232452655818257,
          66956832107717527542675682969659627296154695190197969317121456768278110209624081812931819032/67075241192931567424163340031608633194591075324988777776708292367656145511028697357967454771,
          64975798838685828705244583080817270446526823196344086843549755403422360366760543235450365/67075241192931567424163340031608633194591075324988777776708292367656145511028697357967454771,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          4527911339161310272339729848872891168832009275315961266355725188343996687030983670157961/2684653342403492207362024972377512076521738960723243088457010734046355576876768018718812084,
          1114380585412280413476970591705481729903567777152003900588200891801230616311313622861931494/1118605559334788419734177071823963365217391233634684620190421139185981490365320007799505035,
          0,
          0,
          0,
          28060130374289523724779112177415167921721431415588828894864342675290505212921700900092687/13423266712017461036810124861887560382608694803616215442285053670231777884383840093594060420,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          411242312095442166541350465925682627535777747098605651934620184545931600252781207621659168/1462252613404371414354824964928772019232509852622990572342673047435730942826578484184620223,
          0,
          0,
          0,
          0,
          0,
          0,
          4187300197319718622639918647729859522253208341658557996585447990061381567489942008068361030/13160273520639342729193424684358948173092588673606915151084057426921578485439206357661582007,
          405522501112357277513950141792149615616721585235454329775925213534370193513402575461406805/1012328732356872517630263437258380628699429897969762703929542878993967575803015873666275539];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          19053726605020249543753826141399840639993528929826286652273890237191735821843147250900092687/93359786111496952431696597683594376724185900019942465267268408399718975812146133698062040722,
          0,
          0,
          0,
          0,
          29001411528184222554788696601777738339477741896110174260281812267053560801701942517989484425/46679893055748476215848298841797188362092950009971232633634204199859487906073066849031020361,
          1811470716678695308707264259848784378359654144210647788270099292046679820766566823464775465/10373309567944105825744066409288264080465100002215829474140934266635441756905125966451337858,
          0,
          0,
          0,
          0,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          2543493825193827782561932832413829056426976021921487955121783125008437136971949568726409/6809812650254862905572828286896273188772316574157354207189843109694989146052885956096092,
          0,
          0,
          12114381362825046756655678383466628464329734006483372887082488079814270560176583670157961/20429437950764588716718484860688819566316949722472062621569529329084967438158657868288276,
          171143778089514653094251994995175983176571912556056467280422968561346366766556372987772/5107359487691147179179621215172204891579237430618015655392382332271241859539664467072069,
          0];
    use ![0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          1216370003618652994645563539236980913554888973179711386846950260328878108029634756681664/4819583638431490610555331122371273857676800868881616784356415917855660150904620833163641,
          0,
          0,
          0,
          24606210856041636441871234887065330219555044627956681982849278668087887559006858358495754/43376252745883415494997980101341464719091207819934551059207743260700941358141587498472769,
          7822711857273902101316673361143306277542162433360466594735912249653150826868016329842039/43376252745883415494997980101341464719091207819934551059207743260700941358141587498472769];
    use ![0,
          0,
          0,
          328555748633871438773073419560426609048642882535128865254761123779886995871459910016/9573709761155597750313387758485671400249973836242346289517031882265729401762393947251628567,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          0,
          51059748431739891858597965612912312052861617688297116017452010526160877116164889130/1367672823022228250044769679783667342892853405177478041359575983180818485966056278178804081,
          3191236358393870031420901991742164183145726805856046645436118168446843979583086087545831547/3191236587051865916771129252828557133416657945414115429839010627421909800587464649083876189]
  ]
  all_goals
    use fun i ↦ (1 - ε₁) • (proj_xy (outer_rot.toEuclideanLin (vertices i)))
    refine ⟨?_, ?_, ?_, ?_⟩
    · apply all_fin_20_vec <;> norm_num
    · simp only [sum_univ_twenty, matrix_simps]; norm_num
    · exact fun i ↦ ⟨proj_xy (outer_rot.toEuclideanLin (vertices i)),
        by simp [outer_shadow]⟩
    · rw [←hy]
      simp only [proj_xy, outer_rot, matrix_of_quat, outer_quat, vertices,
        sum_univ_twenty, inner_offset, inner_rot, inner_quat, ε₁,
        matrix_simps]
      ext i; fin_cases i <;> norm_num

end Nopert214