Large Signal Model · Lean source
Section88ProposedRotatedPosGap.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (2)
KomorebiLSM/Section88ProposedRotatedPosGap.lean215 lines
Original source path
Lean/KomorebiLSM/Section88ProposedRotatedPosGap.leanSkip declarations and read code
1 import KomorebiLSM.PerturbedOperatorFixture
2 import KomorebiLSM.RecordedBernsteinFixture
3
4 /-! Exact rational replay of robust_curved_certificate.json: rotated, chart 1, cone_gap. -/
5 set_option autoImplicit false
6 set_option maxRecDepth 4000
7 set_option maxHeartbeats 800000
8 namespace Komorebi.LSM.Section88ProposedRotatedPosGap
9 open TensorBernsteinCertificate RationalBernsteinMargin RationalLorentzMatrix
10 open PerturbedOperatorFixture RecordedBernsteinFixture
11 noncomputable section
12
13 def polynomial : Polynomial₂ := MvPolynomial.C (22581401164127/723394816000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^0 +
14 MvPolynomial.C (375194062058084096199/5883040532189312000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^2 +
15 MvPolynomial.C (23049642380303/13382804096000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (18039959352220757/52656437969920000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
17 MvPolynomial.C (1172698248997177007/4456473763968000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^0 +
18 MvPolynomial.C (7709588439980374761289/13236841197425952000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^2 +
19 MvPolynomial.C (22581401164127/723394816000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^4 +
20 MvPolynomial.C (-422260412679/334570102400000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^4 +
21 MvPolynomial.C (449987494681791241/1316410949248000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^3 +
22 MvPolynomial.C (47411116765089329/178258950558720000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^4 +
23 MvPolynomial.C (107281396030628911/11847698543232000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^1 +
24 MvPolynomial.C (-31103089579457/26765608192000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^0 +
25 MvPolynomial.C (-42370130525931607/11847698543232000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^3 +
26 MvPolynomial.C (-19955088271531/6691402048000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^4 +
27 MvPolynomial.C (230597885513430099/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^1 +
28 MvPolynomial.C (263362952468240247/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^3 +
29 MvPolynomial.C (10941963700703/2893579264000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^0 +
30 MvPolynomial.C (840595139279394971871/23532162128757248000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^2 +
31 MvPolynomial.C (-1553525873977/115743170560000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^4 +
32 MvPolynomial.C (10411802866661/17789337152000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^1 +
33 MvPolynomial.C (2673496386821411571/5883040532189312000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^2 +
34 MvPolynomial.C (-10411802866661/17789337152000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^3 +
35 MvPolynomial.C (145604130659645828443/11766081064378624000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^2 +
36 MvPolynomial.C (-606975135235679/35578674304000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^1 +
37 MvPolynomial.C (608104817709221/35578674304000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^3
38
39 theorem polynomial_source : polynomial=squareGapPolynomial (nominalProposed true) (1/16) false := by
40 apply MvPolynomial.funext
41 intro x
42 norm_num [polynomial,squareGapPolynomial,orientationPolynomial,squareGapPolynomial,outputPolynomial,
43 liftPolynomial,denominatorPolynomial,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
44 ring
45
46 def cell_0 : Rectangle := (square.quarter false false)
47 def leaf_0 : RecordedLeaf polynomial cell_0 := by
48 let c : Fin 5 → Fin 5 → ℚ := ![![(133626515252720363539/62995080059136000000 : ℚ),(7472387280057867477/6999453339904000000 : ℚ),(118663897900987445077/188985240177408000000 : ℚ),(26134461710837937/64215168256000000 : ℚ),(6311319910603999/21208679424000000 : ℚ)],![(1217302680351111677/984298125924000000 : ℚ),(1409181864820170328053/2295820695488512000000 : ℚ),(2768082619869669748939/7748394847273728000000 : ℚ),(9698052330839733073/42125150375936000000 : ℚ),(140682900349162363/869555856384000000 : ℚ)],![(15409568781091311823/23623155022176000000 : ℚ),(4655489197127814187/14348879346803200000 : ℚ),(353743423016970390883387/1906105132429337088000000 : ℚ),(4716414000854664373/40479636689376000000 : ℚ),(1984347987488880611/26738842583808000000 : ℚ)],![(103971709484028333/349972666995200000 : ℚ),(169804570862707184823/1147910347744256000000 : ℚ),(1974998975647045014833/23532162128757248000000 : ℚ),(44949717970454990569/863565582706688000000 : ℚ),(329594808753019/10706243276800000 : ℚ)],![(220845497244887971/1749863334976000000 : ℚ),(4506337293039581499/71744396734016000000 : ℚ),(48890994135310196837/1176608106437862400000 : ℚ),(9064390697739109/291745129292800000 : ℚ),(22581401164127/723394816000000 : ℚ)]]
49 refine ⟨⟨4,4,c,?_,?_⟩,(329594808753019/10706243276800000 : ℚ),?_,?_,?_⟩
50 · decide +kernel
51 · apply MvPolynomial.funext
52 intro x
53 norm_num [Rectangle.localPolynomial,cell_0,Rectangle.quarter,Rectangle.half,
54 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
55 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
56 ring
57 · norm_num
58 · decide +kernel
59 · decide +kernel
60
61 def cell_10 : Rectangle := ((square.quarter false true).quarter false false)
62 def leaf_10 : RecordedLeaf polynomial cell_10 := by
63 let c : Fin 5 → Fin 5 → ℚ := ![![(6311319910603999/21208679424000000 : ℚ),(374320329725780647/1541164038144000000 : ℚ),(653315672206969641337/3023763842838528000000 : ℚ),(136885421184277796563/671947520630784000000 : ℚ),(848427748026322834171/4031685123784704000000 : ℚ)],![(66574502780654387/289851952128000000 : ℚ),(843532627340032587/4554070310912000000 : ℚ),(26783644386519453052997/165299090075172864000000 : ℚ),(10943887726657859534143/73466262255632384000000 : ℚ),(16427966369446586495347/110199393383448576000000 : ℚ)],![(74373371745025430699/427821481340928000000 : ℚ),(1713231214477089927569/12435344390976307200000 : ℚ),(1794288702875830000838429/15248841059434696704000000 : ℚ),(2830218560908234612776481/27109050772328349696000000 : ℚ),(8109819596616109148448797/81327152316985049088000000 : ℚ)],![(6158044695962561447/47535720148992000000 : ℚ),(2780441627961062239371/27634098646614016000000 : ℚ),(90551065400337449921441/1084362030893133987840000 : ℚ),(853777977833479140259579/12048467009923710976000000 : ℚ),(1147608032260882256664487/18072700514885566464000000 : ℚ)],![(55059212954462042887/570428641787904000000 : ℚ),(61318274460545309891/829022959398420480000 : ℚ),(4891822420309990584652399/81327152316985049088000000 : ℚ),(445800388816875416842631/9036350257442783232000000 : ℚ),(4542333537043508283611983/108436203089313398784000000 : ℚ)]]
64 refine ⟨⟨4,4,c,?_,?_⟩,(4542333537043508283611983/108436203089313398784000000 : ℚ),?_,?_,?_⟩
65 · decide +kernel
66 · apply MvPolynomial.funext
67 intro x
68 norm_num [Rectangle.localPolynomial,cell_10,Rectangle.quarter,Rectangle.half,
69 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
70 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
71 ring
72 · norm_num
73 · decide +kernel
74 · decide +kernel
75
76 def cell_11 : Rectangle := ((square.quarter false true).quarter false true)
77 def leaf_11 : RecordedLeaf polynomial cell_11 := by
78 let c : Fin 5 → Fin 5 → ℚ := ![![(848427748026322834171/4031685123784704000000 : ℚ),(218885742236744722241/1007921280946176000000 : ℚ),(183665333742234451429/755940960709632000000 : ℚ),(18421485219307754359/62995080059136000000 : ℚ),(24451959701373395983/62995080059136000000 : ℚ)],![(16427966369446586495347/110199393383448576000000 : ℚ),(32880202297812767378959/220398786766897152000000 : ℚ),(419632079113722440903/2582798282424576000000 : ℚ),(5289131726358731004991/27549848345862144000000 : ℚ),(2676813495242860091/10499180009856000000 : ℚ)],![(8109819596616109148448797/81327152316985049088000000 : ℚ),(7728983510507514458568151/81327152316985049088000000 : ℚ),(3017323276588767966855889/30497682118869393408000000 : ℚ),(28059130882862253134651/247948635112759296000000 : ℚ),(113649882887552730143/755940960709632000000 : ℚ)],![(1147608032260882256664487/18072700514885566464000000 : ℚ),(2029098195543091605879211/36145401029771132928000000 : ℚ),(91588939254526095355421/1694315673270521856000000 : ℚ),(1279949234672736361267/22039878676689715200000 : ℚ),(39526132950713551/512155122432000000 : ℚ)],![(4542333537043508283611983/108436203089313398784000000 : ℚ),(1867531204142255782556197/54218101544656699392000000 : ℚ),(77187782313531263411051/2541473509905782784000000 : ℚ),(121116945633499568227/4031685123784704000000 : ℚ),(23950398268889311/599596240896000000 : ℚ)]]
79 refine ⟨⟨4,4,c,?_,?_⟩,(121116945633499568227/4031685123784704000000 : ℚ),?_,?_,?_⟩
80 · decide +kernel
81 · apply MvPolynomial.funext
82 intro x
83 norm_num [Rectangle.localPolynomial,cell_11,Rectangle.quarter,Rectangle.half,
84 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
85 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
86 ring
87 · norm_num
88 · decide +kernel
89 · decide +kernel
90
91 def cell_12 : Rectangle := ((square.quarter false true).quarter true false)
92 def leaf_12 : RecordedLeaf polynomial cell_12 := by
93 let c : Fin 5 → Fin 5 → ℚ := ![![(55059212954462042887/570428641787904000000 : ℚ),(61318274460545309891/829022959398420480000 : ℚ),(4891822420309990584652399/81327152316985049088000000 : ℚ),(445800388816875416842631/9036350257442783232000000 : ℚ),(4542333537043508283611983/108436203089313398784000000 : ℚ)],![(3622188955737334841/57042864178790400000 : ℚ),(3922330008225875260087/82902295939842048000000 : ℚ),(2992314935594672425196723/81327152316985049088000000 : ℚ),(1005069177034565913962311/36145401029771132928000000 : ℚ),(549754720130430756809261/27109050772328349696000000 : ℚ)],![(4465350388439836817/106955370335232000000 : ℚ),(968831879449741225403/31088360977440768000000 : ℚ),(23103630583708836327917/953052566214668544000000 : ℚ),(247910713104713676275921/13554525386164174848000000 : ℚ),(53993781352537668966199/4066357615849252454400000 : ℚ)],![(3318997729910493/107062432768000000 : ℚ),(88845899700985466019/3454262330826752000000 : ℚ),(8695860907570411447581/376514594060115968000000 : ℚ),(6558008049041452508607/301211675248092774400000 : ℚ),(8417804996381860643131/376514594060115968000000 : ℚ)],![(22581401164127/723394816000000 : ℚ),(182568465707381483/5834902585856000000 : ℚ),(1601105177427255733277/47064324257514496000000 : ℚ),(741526794556704650097/18825729703005798400000 : ℚ),(1857355187831486828147/37651459406011596800000 : ℚ)]]
94 refine ⟨⟨4,4,c,?_,?_⟩,(53993781352537668966199/4066357615849252454400000 : ℚ),?_,?_,?_⟩
95 · decide +kernel
96 · apply MvPolynomial.funext
97 intro x
98 norm_num [Rectangle.localPolynomial,cell_12,Rectangle.quarter,Rectangle.half,
99 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
100 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
101 ring
102 · norm_num
103 · decide +kernel
104 · decide +kernel
105
106 def cell_13 : Rectangle := ((square.quarter false true).quarter true true)
107 def leaf_13 : RecordedLeaf polynomial cell_13 := by
108 let c : Fin 5 → Fin 5 → ℚ := ![![(4542333537043508283611983/108436203089313398784000000 : ℚ),(1867531204142255782556197/54218101544656699392000000 : ℚ),(77187782313531263411051/2541473509905782784000000 : ℚ),(121116945633499568227/4031685123784704000000 : ℚ),(23950398268889311/599596240896000000 : ℚ)],![(549754720130430756809261/27109050772328349696000000 : ℚ),(276566045987949662517431/21687240617862679756800000 : ℚ),(33984311490546767577941/5082947019811565568000000 : ℚ),(663940563802883770223/330598180150345728000000 : ℚ),(33339138207336527/12291722938368000000 : ℚ)],![(53993781352537668966199/4066357615849252454400000 : ℚ),(336143487736612350496217/40663576158492524544000000 : ℚ),(5117328052495589799841/1219907284754775736320000 : ℚ),(128091974215005330739/123974317556379648000000 : ℚ),(267363104137180103/188985240177408000000 : ℚ)],![(8417804996381860643131/376514594060115968000000 : ℚ),(34552399725847622602013/1506058376240463872000000 : ℚ),(957704064789059147707/37651459406011596800000 : ℚ),(139796117237172565919/4591641390977024000000 : ℚ),(56751066268165981/1399890667980800000 : ℚ)],![(1857355187831486828147/37651459406011596800000 : ℚ),(22316567865495643561/376514594060115968000 : ℚ),(1736306585508821686521/23532162128757248000000 : ℚ),(13602993481041232123/143488793468032000000 : ℚ),(220845497244887971/1749863334976000000 : ℚ)]]
109 refine ⟨⟨4,4,c,?_,?_⟩,(128091974215005330739/123974317556379648000000 : ℚ),?_,?_,?_⟩
110 · decide +kernel
111 · apply MvPolynomial.funext
112 intro x
113 norm_num [Rectangle.localPolynomial,cell_13,Rectangle.quarter,Rectangle.half,
114 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
115 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
116 ring
117 · norm_num
118 · decide +kernel
119 · decide +kernel
120
121 def cell_20 : Rectangle := ((square.quarter true false).quarter false false)
122 def leaf_20 : RecordedLeaf polynomial cell_20 := by
123 let c : Fin 5 → Fin 5 → ℚ := ![![(220845497244887971/1749863334976000000 : ℚ),(1356100268007998831/14348879346803200000 : ℚ),(1725976848472355708523/23532162128757248000000 : ℚ),(691797471568653123199/11766081064378624000000 : ℚ),(9204138042865706316751/188257297030057984000000 : ℚ)],![(17834743039315281/437465833744000000 : ℚ),(140096350673519321817/4591641390977024000000 : ℚ),(239183902747208189939/9412864851502899200000 : ℚ),(932147355664514529569/40704280438931456000000 : ℚ),(8417919071183657553183/376514594060115968000000 : ℚ)],![(6524602698230509/4609396101888000000 : ℚ),(24364129554701534077/24794863511275929600000 : ℚ),(125900123276058192613783/30497682118869393408000000 : ℚ),(67110978824571056734367/8132715231698504908800000 : ℚ),(271992479152296479861471/20331788079246262272000000 : ℚ)],![(20024913021464779/7874385007392000000 : ℚ),(589123536941621464057/330598180150345728000000 : ℚ),(261217743069254453286511/40663576158492524544000000 : ℚ),(1361200660434980533257611/108436203089313398784000000 : ℚ),(548881575298353279390557/27109050772328349696000000 : ℚ)],![(40491398816798028031/1007921280946176000000 : ℚ),(5045653811411400912607/165299090075172864000000 : ℚ),(9802859380699189480249/317684188738222848000000 : ℚ),(1892623210118128213160297/54218101544656699392000000 : ℚ),(919600289235795216673571/21687240617862679756800000 : ℚ)]]
124 refine ⟨⟨4,4,c,?_,?_⟩,(24364129554701534077/24794863511275929600000 : ℚ),?_,?_,?_⟩
125 · decide +kernel
126 · apply MvPolynomial.funext
127 intro x
128 norm_num [Rectangle.localPolynomial,cell_20,Rectangle.quarter,Rectangle.half,
129 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
130 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
131 ring
132 · norm_num
133 · decide +kernel
134 · decide +kernel
135
136 def cell_21 : Rectangle := ((square.quarter true false).quarter false true)
137 def leaf_21 : RecordedLeaf polynomial cell_21 := by
138 let c : Fin 5 → Fin 5 → ℚ := ![![(9204138042865706316751/188257297030057984000000 : ℚ),(3669758270316481331159/94128648515028992000000 : ℚ),(1587332194711967762613/47064324257514496000000 : ℚ),(181714697872315281/5834902585856000000 : ℚ),(22581401164127/723394816000000 : ℚ)],![(8417919071183657553183/376514594060115968000000 : ℚ),(32853900409882222831411/1506058376240463872000000 : ℚ),(8749580235035920216239/376514594060115968000000 : ℚ),(89827816466142466419/3454262330826752000000 : ℚ),(3365097014671099/107062432768000000 : ℚ)],![(271992479152296479861471/20331788079246262272000000 : ℚ),(752415022486330635774049/40663576158492524544000000 : ℚ),(5868674342353681412243/238263141553667136000000 : ℚ),(23714949554151106399/746120663458578432000 : ℚ),(911491351878305521/21391074067046400000 : ℚ)],![(548881575298353279390557/27109050772328349696000000 : ℚ),(605970388390369140373369/21687240617862679756800000 : ℚ),(3025412408413806659486873/81327152316985049088000000 : ℚ),(11963426269079720077477/248706887819526144000000 : ℚ),(3691731120966703799/57042864178790400000 : ℚ)],![(919600289235795216673571/21687240617862679756800000 : ℚ),(1352689118030423935103779/27109050772328349696000000 : ℚ),(4947797079287151478085527/81327152316985049088000000 : ℚ),(4660184425448848972463/62176721954881536000000 : ℚ),(55875963650000731063/570428641787904000000 : ℚ)]]
139 refine ⟨⟨4,4,c,?_,?_⟩,(271992479152296479861471/20331788079246262272000000 : ℚ),?_,?_,?_⟩
140 · decide +kernel
141 · apply MvPolynomial.funext
142 intro x
143 norm_num [Rectangle.localPolynomial,cell_21,Rectangle.quarter,Rectangle.half,
144 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
145 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
146 ring
147 · norm_num
148 · decide +kernel
149 · decide +kernel
150
151 def cell_22 : Rectangle := ((square.quarter true false).quarter true false)
152 def leaf_22 : RecordedLeaf polynomial cell_22 := by
153 let c : Fin 5 → Fin 5 → ℚ := ![![(40491398816798028031/1007921280946176000000 : ℚ),(5045653811411400912607/165299090075172864000000 : ℚ),(9802859380699189480249/317684188738222848000000 : ℚ),(1892623210118128213160297/54218101544656699392000000 : ℚ),(919600289235795216673571/21687240617862679756800000 : ℚ)],![(522797391778990429/6719475206307840000 : ℚ),(6531163902901327395457/110199393383448576000000 : ℚ),(749438086129912684552411/13554525386164174848000000 : ℚ),(2069764060012510773127859/36145401029771132928000000 : ℚ),(1166746098527423174862247/18072700514885566464000000 : ℚ)],![(114854664692661412433/755940960709632000000 : ℚ),(28750193553190556424241/247948635112759296000000 : ℚ),(1553272448128391796584933/15248841059434696704000000 : ℚ),(214682353179717249906287/2198031143702298624000000 : ℚ),(1659079070313174963372553/16265430463397009817600000 : ℚ)],![(293515714989763901/1135046487552000000 : ℚ),(147574710935057857181/744590495834112000000 : ℚ),(573120134612120229059219/3388631346541043712000000 : ℚ),(1402766765595475236954247/9036350257442783232000000 : ℚ),(696545608145143551518603/4518175128721391616000000 : ℚ)],![(18195693709165387/46015398144000000 : ℚ),(1152238659919359443/3773262647808000000 : ℚ),(883647338978578997809/3434423662034841600000 : ℚ),(10553511768487346892361/45792315493797888000000 : ℚ),(1502057300303240426879851/6777262693082087424000000 : ℚ)]]
154 refine ⟨⟨4,4,c,?_,?_⟩,(5045653811411400912607/165299090075172864000000 : ℚ),?_,?_,?_⟩
155 · decide +kernel
156 · apply MvPolynomial.funext
157 intro x
158 norm_num [Rectangle.localPolynomial,cell_22,Rectangle.quarter,Rectangle.half,
159 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
160 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
161 ring
162 · norm_num
163 · decide +kernel
164 · decide +kernel
165
166 def cell_23 : Rectangle := ((square.quarter true false).quarter true true)
167 def leaf_23 : RecordedLeaf polynomial cell_23 := by
168 let c : Fin 5 → Fin 5 → ℚ := ![![(919600289235795216673571/21687240617862679756800000 : ℚ),(1352689118030423935103779/27109050772328349696000000 : ℚ),(4947797079287151478085527/81327152316985049088000000 : ℚ),(4660184425448848972463/62176721954881536000000 : ℚ),(55875963650000731063/570428641787904000000 : ℚ)],![(1166746098527423174862247/18072700514885566464000000 : ℚ),(2597220334097181926321129/36145401029771132928000000 : ℚ),(2290060583386832098894727/27109050772328349696000000 : ℚ),(8439349711503690567409/82902295939842048000000 : ℚ),(3118109003763934339/23767860074496000000 : ℚ)],![(1659079070313174963372553/16265430463397009817600000 : ℚ),(8647543635482211387192911/81327152316985049088000000 : ℚ),(726953464426257689733017/6099536423773878681600000 : ℚ),(41537074698695686459/298448265383431372800 : ℚ),(75105784358567189639/427821481340928000000 : ℚ)],![(696545608145143551518603/4518175128721391616000000 : ℚ),(276683133397019793824033/1807270051488556646400000 : ℚ),(223442724261735211273463/1355452538616417484800000 : ℚ),(3877256892345540117077/20725573984960512000000 : ℚ),(1374055771774611047/5941965018624000000 : ℚ)],![(1502057300303240426879851/6777262693082087424000000 : ℚ),(721097429435176756845137/3388631346541043712000000 : ℚ),(1128210737389636177188589/5082947019811565568000000 : ℚ),(1910823251531114025949/7772090244360192000000 : ℚ),(2129855726737580651/7130358022348800000 : ℚ)]]
169 refine ⟨⟨4,4,c,?_,?_⟩,(919600289235795216673571/21687240617862679756800000 : ℚ),?_,?_,?_⟩
170 · decide +kernel
171 · apply MvPolynomial.funext
172 intro x
173 norm_num [Rectangle.localPolynomial,cell_23,Rectangle.quarter,Rectangle.half,
174 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
175 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
176 ring
177 · norm_num
178 · decide +kernel
179 · decide +kernel
180
181 def cell_3 : Rectangle := (square.quarter true true)
182 def leaf_3 : RecordedLeaf polynomial cell_3 := by
183 let c : Fin 5 → Fin 5 → ℚ := ![![(22581401164127/723394816000000 : ℚ),(22874418703114323/729362823232000000 : ℚ),(247898216355372976851/5883040532189312000000 : ℚ),(142135252937525791/2242012397938000000 : ℚ),(220845497244887971/1749863334976000000 : ℚ)],![(1694073328525701/53531216384000000 : ℚ),(45946106911392682353/863565582706688000000 : ℚ),(125620514444219681571/1470760133047328000000 : ℚ),(171595379954659257897/1147910347744256000000 : ℚ),(1041317652128497921/3499726669952000000 : ℚ)],![(406080234592945201/5347768516761600000 : ℚ),(695307575928524022551/5829067683270144000000 : ℚ),(3313421964722875881727/17487203049810432000000 : ℚ),(11691910178091297569/35543095629696000000 : ℚ),(283932450422364539/433452385728000000 : ℚ)],![(5839390627607429309/35651790111744000000 : ℚ),(3649445269998353288737/15544180488720384000000 : ℚ),(464461998249265769741699/1270736754952891392000000 : ℚ),(12928922819569065014051/20662386259396608000000 : ℚ),(1917028899354466771/1536465367296000000 : ℚ)],![(2129855726737580651/7130358022348800000 : ℚ),(392872715421207584609/971511280545024000000 : ℚ),(24853926967200996241823/39710523592277856000000 : ℚ),(33918210777997071521/31497540029568000000 : ℚ),(80590727441636119/37474765056000000 : ℚ)]]
184 refine ⟨⟨4,4,c,?_,?_⟩,(22581401164127/723394816000000 : ℚ),?_,?_,?_⟩
185 · decide +kernel
186 · apply MvPolynomial.funext
187 intro x
188 norm_num [Rectangle.localPolynomial,cell_3,Rectangle.quarter,Rectangle.half,
189 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
190 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
191 ring
192 · norm_num
193 · decide +kernel
194 · decide +kernel
195
196 def witness : SubdivisionWitness polynomial square :=
197 .of_quarters (fun
198 | false,false => .leaf leaf_0.certificate
199 | false,true => .of_quarters (fun
200 | false,false => .leaf leaf_10.certificate
201 | false,true => .leaf leaf_11.certificate
202 | true,false => .leaf leaf_12.certificate
203 | true,true => .leaf leaf_13.certificate)
204 | true,false => .of_quarters (fun
205 | false,false => .leaf leaf_20.certificate
206 | false,true => .leaf leaf_21.certificate
207 | true,false => .leaf leaf_22.certificate
208 | true,true => .leaf leaf_23.certificate)
209 | true,true => .leaf leaf_3.certificate)
210
211 def certifiedWitness : SubdivisionWitness (squareGapPolynomial (nominalProposed true) (1/16) false) square :=
212 polynomial_source ▸ witness
213
214 end
215 end Komorebi.LSM.Section88ProposedRotatedPosGap
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 76525fc2fe8d88f1ae6d7ce4e918f246a8e897094b196479eee05bdac54523a7