Large Signal Model · Lean source
Section88ProposedDirectNegGap.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/Section88ProposedDirectNegGap.lean264 lines
Original source path
Lean/KomorebiLSM/Section88ProposedDirectNegGap.leanSkip declarations and read code
1 import KomorebiLSM.PerturbedOperatorFixture
2 import KomorebiLSM.RecordedBernsteinFixture
3
4 /-! Exact rational replay of robust_curved_certificate.json: direct, chart -1, cone_gap. -/
5 set_option autoImplicit false
6 set_option maxRecDepth 4000
7 set_option maxHeartbeats 800000
8 namespace Komorebi.LSM.Section88ProposedDirectNegGap
9 open TensorBernsteinCertificate RationalBernsteinMargin RationalLorentzMatrix
10 open PerturbedOperatorFixture RecordedBernsteinFixture
11 noncomputable section
12
13 def polynomial : Polynomial₂ := MvPolynomial.C (201708959642143/6510553344000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^0 +
14 MvPolynomial.C (2449683880064423839/38675942140032000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^2 +
15 MvPolynomial.C (-531352814559833/4014841228800000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (-21452330597546779/106736022912000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
17 MvPolynomial.C (15431789372628797/59419650186240000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^0 +
18 MvPolynomial.C (557086117785234212147/1103070099785496000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^2 +
19 MvPolynomial.C (201708959642143/6510553344000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^4 +
20 MvPolynomial.C (1769118374654253/13382804096000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^4 +
21 MvPolynomial.C (-856100969275951/4269440916480000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^3 +
22 MvPolynomial.C (388856298069010919/1485491254656000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^4 +
23 MvPolynomial.C (104251184003445269/3949232847744000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^1 +
24 MvPolynomial.C (-398310922888487/13382804096000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^0 +
25 MvPolynomial.C (-70516418707807037/3949232847744000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^3 +
26 MvPolynomial.C (892881998260693/26765608192000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^4 +
27 MvPolynomial.C (-77469101614088247/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^1 +
28 MvPolynomial.C (-62326278926060499/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^3 +
29 MvPolynomial.C (1427106941687/115743170560000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^0 +
30 MvPolynomial.C (-74499466744462809/1980655006208000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^2 +
31 MvPolynomial.C (5834773688303/2893579264000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^4 +
32 MvPolynomial.C (-4320788058223/4327136064000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^1 +
33 MvPolynomial.C (72607478835873583/159001095464576000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^2 +
34 MvPolynomial.C (4320788058223/4327136064000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^3 +
35 MvPolynomial.C (-1756873837797262373/107945697838336000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^2 +
36 MvPolynomial.C (-6942302319869/326409856000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^1 +
37 MvPolynomial.C (-2036718627769/326409856000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^3
38
39 theorem polynomial_source : polynomial=squareGapPolynomial (nominalProposed false) (1/16) true := 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 → ℚ := ![![(44429662622260048183/62995080059136000000 : ℚ),(55125535027467662857/107616595101024000000 : ℚ),(139449529964951728079629/317684188738222848000000 : ℚ),(263276563339071936113/647674187030016000000 : ℚ),(16582729794157037851/35651790111744000000 : ℚ)],![(20336541388301493559/62995080059136000000 : ℚ),(120536129335009610503/459164139097702400000 : ℚ),(29945313441200807116753/127073675495289139200000 : ℚ),(388541306427083571983/1727131165413376000000 : ℚ),(953817989440123429/3565179011174400000 : ℚ)],![(296268148788642659/3149754002956800000 : ℚ),(288216508715553519461/2582798282424576000000 : ℚ),(71822338675489786858357/635368377476445696000000 : ℚ),(2040472907895297689/17825895055872000000 : ℚ),(208622654037871387/1485491254656000000 : ℚ)],![(194084107017749/7809952896000000 : ℚ),(39247352496919207/853888183296000000 : ℚ),(7874315729110681223/157542369818112000000 : ℚ),(3623944369571019301/70018831030272000000 : ℚ),(7716761862578393/120445236864000000 : ℚ)],![(1441459854126331/11503849536000000 : ℚ),(9928469986254313/157219276992000000 : ℚ),(975505393958251831/23205565284019200000 : ℚ),(738780963712691/23655010483200000 : ℚ),(201708959642143/6510553344000000 : ℚ)]]
49 refine ⟨⟨4,4,c,?_,?_⟩,(194084107017749/7809952896000000 : ℚ),?_,?_,?_⟩
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_1 : Rectangle := (square.quarter false true)
62 def leaf_1 : RecordedLeaf polynomial cell_1 := by
63 let c : Fin 5 → Fin 5 → ℚ := ![![(16582729794157037851/35651790111744000000 : ℚ),(50884392877295065871/97151128054502400000 : ℚ),(53489787686707972387279/79421047184555712000000 : ℚ),(1245679775126532569143/1291399141212288000000 : ℚ),(99315266031470684539/62995080059136000000 : ℚ)],![(953817989440123429/3565179011174400000 : ℚ),(130281651623624977109/420112986181632000000 : ℚ),(515853453501673894015441/1270736754952891392000000 : ℚ),(12235099868322504443707/20662386259396608000000 : ℚ),(30243085772232156989/31497540029568000000 : ℚ)],![(208622654037871387/1485491254656000000 : ℚ),(2966470789013615599/17825895055872000000 : ℚ),(137833023628890197390617/635368377476445696000000 : ℚ),(136273602568607719723/430466380404096000000 : ℚ),(3924682432939206191/7874385007392000000 : ℚ)],![(7716761862578393/120445236864000000 : ℚ),(16044232267960376881/210056493090816000000 : ℚ),(1563291446798165969/15754236981811200000 : ℚ),(3417088981962449/23501509632000000 : ℚ),(44048616238961/195248822400000 : ℚ)],![(201708959642143/6510553344000000 : ℚ),(5452281072651611/177412578624000000 : ℚ),(4761669358798067633/116027826420096000000 : ℚ),(3664305507552079/58957228872000000 : ℚ),(1441459854126331/11503849536000000 : ℚ)]]
64 refine ⟨⟨4,4,c,?_,?_⟩,(5452281072651611/177412578624000000 : ℚ),?_,?_,?_⟩
65 · decide +kernel
66 · apply MvPolynomial.funext
67 intro x
68 norm_num [Rectangle.localPolynomial,cell_1,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_20 : Rectangle := ((square.quarter true false).quarter false false)
77 def leaf_20 : RecordedLeaf polynomial cell_20 := by
78 let c : Fin 5 → Fin 5 → ℚ := ![![(1441459854126331/11503849536000000 : ℚ),(8888526397794251/94331566195200000 : ℚ),(34070512758220799609/464111305680384000000 : ℚ),(4564708181222479189/77351884280064000000 : ℚ),(60801472026129273511/1237630148481024000000 : ℚ)],![(298848919951110841/1702569731328000000 : ℚ),(138087449564234754823/1116885743751168000000 : ℚ),(1226369744326132177009/13737694648139366400000 : ℚ),(24083330533589254880171/366338523950383104000000 : ℚ),(244187537946385384051/4950520593924096000000 : ℚ)],![(3378668799165198479/12599016011827200000 : ℚ),(1525755396659340291871/8264954503758643200000 : ℚ),(1316797753565046660636673/10165894039623131136000000 : ℚ),(1247288122726994610653437/13554525386164174848000000 : ℚ),(446151254532132486993667/6777262693082087424000000 : ℚ)],![(40769284550280212671/100792128094617600000 : ℚ),(91777648171235937948599/330598180150345728000000 : ℚ),(7897429654025538329026247/40663576158492524544000000 : ℚ),(14920439372212551882790453/108436203089313398784000000 : ℚ),(5324346847644058081069499/54218101544656699392000000 : ℚ)],![(590656833733077419359/1007921280946176000000 : ℚ),(66715785363370211014003/165299090075172864000000 : ℚ),(2887248203167480891708907/10165894039623131136000000 : ℚ),(11008272640608708775953113/54218101544656699392000000 : ℚ),(637194152188310422815727/4337448123572535951360000 : ℚ)]]
79 refine ⟨⟨4,4,c,?_,?_⟩,(60801472026129273511/1237630148481024000000 : ℚ),?_,?_,?_⟩
80 · decide +kernel
81 · apply MvPolynomial.funext
82 intro x
83 norm_num [Rectangle.localPolynomial,cell_20,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_21 : Rectangle := ((square.quarter true false).quarter false true)
92 def leaf_21 : RecordedLeaf polynomial cell_21 := by
93 let c : Fin 5 → Fin 5 → ℚ := ![![(60801472026129273511/1237630148481024000000 : ℚ),(24283806576349439999/618815074240512000000 : ℚ),(31439448896150418679/928222611360768000000 : ℚ),(44149705512374317/1419300628992000000 : ℚ),(201708959642143/6510553344000000 : ℚ)],![(244187537946385384051/4950520593924096000000 : ℚ),(12056425082475781959377/366338523950383104000000 : ℚ),(6487036709852434158989/274753892962787328000000 : ℚ),(14875072697938618201/840225972363264000000 : ℚ),(6956170795121087/481780947456000000 : ℚ)],![(446151254532132486993667/6777262693082087424000000 : ℚ),(59701877266837259702359/1506058376240463872000000 : ℚ),(62960228144214437659591/2541473509905782784000000 : ℚ),(465838939883577225877/31088360977440768000000 : ℚ),(34527749888140637/3961310012416000000 : ℚ)],![(5324346847644058081069499/54218101544656699392000000 : ℚ),(6376948018363680441487543/108436203089313398784000000 : ℚ),(2979622277277769496098129/81327152316985049088000000 : ℚ),(5504777431187000736023/248706887819526144000000 : ℚ),(1837512836531297641/142607160446976000000 : ℚ)],![(637194152188310422815727/4337448123572535951360000 : ℚ),(2460790582049525897220031/27109050772328349696000000 : ℚ),(4837911195810876189132103/81327152316985049088000000 : ℚ),(2441867469840018683747/62176721954881536000000 : ℚ),(15279306774547857007/570428641787904000000 : ℚ)]]
94 refine ⟨⟨4,4,c,?_,?_⟩,(34527749888140637/3961310012416000000 : ℚ),?_,?_,?_⟩
95 · decide +kernel
96 · apply MvPolynomial.funext
97 intro x
98 norm_num [Rectangle.localPolynomial,cell_21,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_22 : Rectangle := ((square.quarter true false).quarter true false)
107 def leaf_22 : RecordedLeaf polynomial cell_22 := by
108 let c : Fin 5 → Fin 5 → ℚ := ![![(590656833733077419359/1007921280946176000000 : ℚ),(66715785363370211014003/165299090075172864000000 : ℚ),(2887248203167480891708907/10165894039623131136000000 : ℚ),(11008272640608708775953113/54218101544656699392000000 : ℚ),(637194152188310422815727/4337448123572535951360000 : ℚ)],![(96702602745419089001/125990160118272000000 : ℚ),(175085493282244906107413/330598180150345728000000 : ℚ),(15200555971314308804645009/40663576158492524544000000 : ℚ),(29112651190222283221021999/108436203089313398784000000 : ℚ),(2651376739265925622330919/13554525386164174848000000 : ℚ)],![(250537364213579262229/251980320236544000000 : ℚ),(56911476522097886998117/82649545037586432000000 : ℚ),(2484180456104715949223027/5082947019811565568000000 : ℚ),(9590682154458854890422647/27109050772328349696000000 : ℚ),(1413153025509634871245769/5421810154465669939200000 : ℚ)],![(798614366762019679/629950800591360000 : ℚ),(72857049471580075865573/82649545037586432000000 : ℚ),(6398969573852174299425893/10165894039623131136000000 : ℚ),(12457063459035509922149683/27109050772328349696000000 : ℚ),(1160510709315993247394261/3388631346541043712000000 : ℚ)],![(100145552482963963039/62995080059136000000 : ℚ),(1433224904405942041769/1291399141212288000000 : ℚ),(63326966633452135915273/79421047184555712000000 : ℚ),(99468314063775703213117/169431567327052185600000 : ℚ),(2998703468128979109582871/6777262693082087424000000 : ℚ)]]
109 refine ⟨⟨4,4,c,?_,?_⟩,(637194152188310422815727/4337448123572535951360000 : ℚ),?_,?_,?_⟩
110 · decide +kernel
111 · apply MvPolynomial.funext
112 intro x
113 norm_num [Rectangle.localPolynomial,cell_22,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_23 : Rectangle := ((square.quarter true false).quarter true true)
122 def leaf_23 : RecordedLeaf polynomial cell_23 := by
123 let c : Fin 5 → Fin 5 → ℚ := ![![(637194152188310422815727/4337448123572535951360000 : ℚ),(2460790582049525897220031/27109050772328349696000000 : ℚ),(4837911195810876189132103/81327152316985049088000000 : ℚ),(2441867469840018683747/62176721954881536000000 : ℚ),(15279306774547857007/570428641787904000000 : ℚ)],![(2651376739265925622330919/13554525386164174848000000 : ℚ),(2661875327606505347254541/21687240617862679756800000 : ℚ),(6696200114343982882166077/81327152316985049088000000 : ℚ),(14030162327533148733953/248706887819526144000000 : ℚ),(464171244059410469/11408572835758080000 : ℚ)],![(1413153025509634871245769/5421810154465669939200000 : ℚ),(1513616033545831274011681/9036350257442783232000000 : ℚ),(1180985371843411097155351/10165894039623131136000000 : ℚ),(5194370327940228450719/62176721954881536000000 : ℚ),(1630623008781463/25352384079462400 : ℚ)],![(1160510709315993247394261/3388631346541043712000000 : ℚ),(6111107890020382036158493/27109050772328349696000000 : ℚ),(3279005794181656769865001/20331788079246262272000000 : ℚ),(7509919364114616225557/62176721954881536000000 : ℚ),(6953713465601339081/71303580223488000000 : ℚ)],![(2998703468128979109582871/6777262693082087424000000 : ℚ),(1009337186853465045320531/3388631346541043712000000 : ℚ),(6015343682566430495957/27475389296278732800000 : ℚ),(1314999555532803999751/7772090244360192000000 : ℚ),(1004740642084909007/7130358022348800000 : ℚ)]]
124 refine ⟨⟨4,4,c,?_,?_⟩,(15279306774547857007/570428641787904000000 : ℚ),?_,?_,?_⟩
125 · decide +kernel
126 · apply MvPolynomial.funext
127 intro x
128 norm_num [Rectangle.localPolynomial,cell_23,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_300 : Rectangle := (((square.quarter true true).quarter false false).quarter false false)
137 def leaf_300 : RecordedLeaf polynomial cell_300 := by
138 let c : Fin 5 → Fin 5 → ℚ := ![![(201708959642143/6510553344000000 : ℚ),(17553590818717441/567720251596800000 : ℚ),(23403690522498020987/742578089088614400000 : ℚ),(162267449802675624679/4950520593924096000000 : ℚ),(689657146145967254599/19802082375696384000000 : ℚ)],![(21882633808639669/963561894912000000 : ℚ),(73478241725538534343/3360903889453056000000 : ℚ),(47642792623466066476891/2198031143702298624000000 : ℚ),(129553736213492504966303/5861416383206129664000000 : ℚ),(136299375435218304938561/5861416383206129664000000 : ℚ)],![(271646809963506853/15845240049664000000 : ℚ),(3862003024706723334713/248706887819526144000000 : ℚ),(297415163936524800130559/20331788079246262272000000 : ℚ),(691499073989068062443619/48193868039694843904000000 : ℚ),(1283051402247245284895699/86748962471450719027200000 : ℚ)],![(3232364508503902393/228171456715161600000 : ℚ),(46928237801955363164777/3979310205112418304000000 : ℚ),(5332010602447509540281911/520493774828704314163200000 : ℚ),(13011125223125475415196861/1387983399543211504435200000 : ℚ),(64456626129220120985158909/6939916997716057522176000000 : ℚ)],![(125128845156101598751/9126858268606464000000 : ℚ),(21043288368739351594651/1989655102556209152000000 : ℚ),(43868914041066500412061231/5204937748287043141632000000 : ℚ),(24525910682620130384086139/3469958498858028761088000000 : ℚ),(183598489904131917720946807/27759667990864230088704000000 : ℚ)]]
139 refine ⟨⟨4,4,c,?_,?_⟩,(183598489904131917720946807/27759667990864230088704000000 : ℚ),?_,?_,?_⟩
140 · decide +kernel
141 · apply MvPolynomial.funext
142 intro x
143 norm_num [Rectangle.localPolynomial,cell_300,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_301 : Rectangle := (((square.quarter true true).quarter false false).quarter false true)
152 def leaf_301 : RecordedLeaf polynomial cell_301 := by
153 let c : Fin 5 → Fin 5 → ℚ := ![![(689657146145967254599/19802082375696384000000 : ℚ),(365122246540616005241/9901041187848192000000 : ℚ),(589835851255754687389/14851561781772288000000 : ℚ),(21518520362053176701/495052059392409600000 : ℚ),(11974922227636748267/247526029696204800000 : ℚ)],![(136299375435218304938561/5861416383206129664000000 : ℚ),(143045014656944104910819/5861416383206129664000000 : ℚ),(28880625728027383217639/1099015571851149312000000 : ℚ),(42472199331488559912229/1465354095801532416000000 : ℚ),(12009649030402292002871/366338523950383104000000 : ℚ)],![(1283051402247245284895699/86748962471450719027200000 : ℚ),(178568171799211899647687/11722832766412259328000000 : ℚ),(1333484664747059597386679/81327152316985049088000000 : ℚ),(53878133836872361978981/2930708191603064832000000 : ℚ),(582643035738937345352497/27109050772328349696000000 : ℚ)],![(64456626129220120985158909/6939916997716057522176000000 : ℚ),(63857626142812864894333513/6939916997716057522176000000 : ℚ),(25761553032626663565171461/2602468874143521570816000000 : ℚ),(19925874278855763208160351/1734979249429014380544000000 : ℚ),(1241751643939211850428051/86748962471450719027200000 : ℚ)],![(183598489904131917720946807/27759667990864230088704000000 : ℚ),(85494847173651396184602251/13879833995432115044352000000 : ℚ),(137649269493778625593018009/20819750993148172566528000000 : ℚ),(28063722961874925579086719/3469958498858028761088000000 : ℚ),(19123744599210407663943151/1734979249429014380544000000 : ℚ)]]
154 refine ⟨⟨4,4,c,?_,?_⟩,(85494847173651396184602251/13879833995432115044352000000 : ℚ),?_,?_,?_⟩
155 · decide +kernel
156 · apply MvPolynomial.funext
157 intro x
158 norm_num [Rectangle.localPolynomial,cell_301,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_302 : Rectangle := (((square.quarter true true).quarter false false).quarter true false)
167 def leaf_302 : RecordedLeaf polynomial cell_302 := by
168 let c : Fin 5 → Fin 5 → ℚ := ![![(125128845156101598751/9126858268606464000000 : ℚ),(21043288368739351594651/1989655102556209152000000 : ℚ),(43868914041066500412061231/5204937748287043141632000000 : ℚ),(24525910682620130384086139/3469958498858028761088000000 : ℚ),(183598489904131917720946807/27759667990864230088704000000 : ℚ)],![(60481554986023550891/4563429134303232000000 : ℚ),(37244915673002043213827/3979310205112418304000000 : ℚ),(4302215257207238177662919/650617218535880392704000000 : ℚ),(33048016614853144460360251/6939916997716057522176000000 : ℚ),(54685237645691675750628989/13879833995432115044352000000 : ℚ)],![(11650468483563496621/760571522383872000000 : ℚ),(10606351034350233363377/994827551278104576000000 : ℚ),(9583378508528992217597897/1301234437071760785408000000 : ℚ),(987795768135481548906473/192775472158779375616000000 : ℚ),(28416097567031056571967091/6939916997716057522176000000 : ℚ)],![(22629358120673047571/1140857283575808000000 : ℚ),(14326953111293270751857/994827551278104576000000 : ℚ),(3445099931810331627870079/325308609267940196352000000 : ℚ),(13952658446043310326187657/1734979249429014380544000000 : ℚ),(24101839410500823661333001/3469958498858028761088000000 : ℚ)],![(15279306774547857007/570428641787904000000 : ℚ),(1277232922718565278771/62176721954881536000000 : ℚ),(5279747221653943181903683/325308609267940196352000000 : ℚ),(291289107957393634792463/21687240617862679756800000 : ℚ),(21478233435176807474044591/1734979249429014380544000000 : ℚ)]]
169 refine ⟨⟨4,4,c,?_,?_⟩,(54685237645691675750628989/13879833995432115044352000000 : ℚ),?_,?_,?_⟩
170 · decide +kernel
171 · apply MvPolynomial.funext
172 intro x
173 norm_num [Rectangle.localPolynomial,cell_302,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_303 : Rectangle := (((square.quarter true true).quarter false false).quarter true true)
182 def leaf_303 : RecordedLeaf polynomial cell_303 := by
183 let c : Fin 5 → Fin 5 → ℚ := ![![(183598489904131917720946807/27759667990864230088704000000 : ℚ),(85494847173651396184602251/13879833995432115044352000000 : ℚ),(137649269493778625593018009/20819750993148172566528000000 : ℚ),(28063722961874925579086719/3469958498858028761088000000 : ℚ),(19123744599210407663943151/1734979249429014380544000000 : ℚ)],![(54685237645691675750628989/13879833995432115044352000000 : ℚ),(10818610515419265645134369/3469958498858028761088000000 : ℚ),(6920611472654394266466433/2081975099314817256652800000 : ℚ),(254307771344348824091449/54218101544656699392000000 : ℚ),(6706228159818289159662641/867489624714507190272000000 : ℚ)],![(28416097567031056571967091/6939916997716057522176000000 : ℚ),(10635773740592388691650577/3469958498858028761088000000 : ℚ),(456753075042625170389021/140673993196947111936000000 : ℚ),(4159902019877618308544393/867489624714507190272000000 : ℚ),(3611000292249168181022083/433744812357253595136000000 : ℚ)],![(24101839410500823661333001/3469958498858028761088000000 : ℚ),(79290476284824322930823/13554525386164174848000000 : ℚ),(16150367009725262049833693/2602468874143521570816000000 : ℚ),(355811197032967965792101/43374481235725359513600000 : ℚ),(545669754100977572464369/43374481235725359513600000 : ℚ)],![(21478233435176807474044591/1734979249429014380544000000 : ℚ),(9826669116881062082346071/867489624714507190272000000 : ℚ),(3128860656474344559911477/260246887414352157081600000 : ℚ),(637508186492597666842103/43374481235725359513600000 : ℚ),(438907059614079603733931/21687240617862679756800000 : ℚ)]]
184 refine ⟨⟨4,4,c,?_,?_⟩,(10635773740592388691650577/3469958498858028761088000000 : ℚ),?_,?_,?_⟩
185 · decide +kernel
186 · apply MvPolynomial.funext
187 intro x
188 norm_num [Rectangle.localPolynomial,cell_303,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 cell_31 : Rectangle := ((square.quarter true true).quarter false true)
197 def leaf_31 : RecordedLeaf polynomial cell_31 := by
198 let c : Fin 5 → Fin 5 → ℚ := ![![(11974922227636748267/247526029696204800000 : ℚ),(144062463208570681/2475260296962048000 : ℚ),(33722939925241225043/464111305680384000000 : ℚ),(88414298079596203/943315661952000000 : ℚ),(1441459854126331/11503849536000000 : ℚ)],![(3148206581951098285291/183169261975191552000000 : ℚ),(8264450296056731316997/366338523950383104000000 : ℚ),(176052718780887672871/5495077859255746560000 : ℚ),(1303227172772040319/27241115701248000000 : ℚ),(63976060407087761/851284865664000000 : ℚ)],![(21802378081861904690503/6777262693082087424000000 : ℚ),(101911892031015512278907/13554525386164174848000000 : ℚ),(171878692518756904567159/10165894039623131136000000 : ℚ),(34781493585544606157/1007921280946176000000 : ℚ),(4291823413561371073/62995080059136000000 : ℚ)],![(53381347243448984365219/10843620308931339878400000 : ℚ),(49234775177471128289843/4337448123572535951360000 : ℚ),(515546800092770075131033/20331788079246262272000000 : ℚ),(17083003255532702855047/330598180150345728000000 : ℚ),(25746928154654321353/251980320236544000000 : ℚ)],![(438907059614079603733931/21687240617862679756800000 : ℚ),(67921299234964114435969/2168724061786267975680000 : ℚ),(21901274432423349109811/406635761584925245440000 : ℚ),(15693732624442328958419/165299090075172864000000 : ℚ),(173432866903950144031/1007921280946176000000 : ℚ)]]
199 refine ⟨⟨4,4,c,?_,?_⟩,(21802378081861904690503/6777262693082087424000000 : ℚ),?_,?_,?_⟩
200 · decide +kernel
201 · apply MvPolynomial.funext
202 intro x
203 norm_num [Rectangle.localPolynomial,cell_31,Rectangle.quarter,Rectangle.half,
204 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
205 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
206 ring
207 · norm_num
208 · decide +kernel
209 · decide +kernel
210
211 def cell_32 : Rectangle := ((square.quarter true true).quarter true false)
212 def leaf_32 : RecordedLeaf polynomial cell_32 := by
213 let c : Fin 5 → Fin 5 → ℚ := ![![(15279306774547857007/570428641787904000000 : ℚ),(2669733954989231663/186716882747392000000 : ℚ),(155133179090249342515163/16265430463397009817600000 : ℚ),(149099945103992539871/16281712175572582400000 : ℚ),(438907059614079603733931/21687240617862679756800000 : ℚ)],![(464171244059410469/11408572835758080000 : ℚ),(2069234637819049238149/82902295939842048000000 : ℚ),(1580312311538278215409153/81327152316985049088000000 : ℚ),(143283580223531943401561/7229080205954226585600000 : ℚ),(48190714046328827421089/1355452538616417484800000 : ℚ)],![(1630623008781463/25352384079462400 : ℚ),(2803835530132847564281/62176721954881536000000 : ℚ),(3194243943683180378321/81327152316985049088000 : ℚ),(225368661910650609689753/5421810154465669939200000 : ℚ),(1747931337963355793779477/27109050772328349696000000 : ℚ)],![(6953713465601339081/71303580223488000000 : ℚ),(1539118973298039710569/20725573984960512000000 : ℚ),(1387269955661451670487101/20331788079246262272000000 : ℚ),(659670063232144831238569/9036350257442783232000000 : ℚ),(88904771208539052272867/847157836635260928000000 : ℚ)],![(1004740642084909007/7130358022348800000 : ℚ),(97259449356921959501/863565582706688000000 : ℚ),(537757400467567317323509/5082947019811565568000000 : ℚ),(42431445072613360764873/376514594060115968000000 : ℚ),(1046169649501273119041671/6777262693082087424000000 : ℚ)]]
214 refine ⟨⟨4,4,c,?_,?_⟩,(149099945103992539871/16281712175572582400000 : ℚ),?_,?_,?_⟩
215 · decide +kernel
216 · apply MvPolynomial.funext
217 intro x
218 norm_num [Rectangle.localPolynomial,cell_32,Rectangle.quarter,Rectangle.half,
219 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
220 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
221 ring
222 · norm_num
223 · decide +kernel
224 · decide +kernel
225
226 def cell_33 : Rectangle := ((square.quarter true true).quarter true true)
227 def leaf_33 : RecordedLeaf polynomial cell_33 := by
228 let c : Fin 5 → Fin 5 → ℚ := ![![(438907059614079603733931/21687240617862679756800000 : ℚ),(67921299234964114435969/2168724061786267975680000 : ℚ),(21901274432423349109811/406635761584925245440000 : ℚ),(15693732624442328958419/165299090075172864000000 : ℚ),(173432866903950144031/1007921280946176000000 : ℚ)],![(48190714046328827421089/1355452538616417484800000 : ℚ),(222450421762385329454033/4337448123572535951360000 : ℚ),(1674580643149564835850067/20331788079246262272000000 : ℚ),(45691927242236612978629/330598180150345728000000 : ℚ),(4877560423785660053/20158425618923520000 : ℚ)],![(1747931337963355793779477/27109050772328349696000000 : ℚ),(2369019366373458539110189/27109050772328349696000000 : ℚ),(1330912535575551665286193/10165894039623131136000000 : ℚ),(3431308893473322553333/16529909007517286400000 : ℚ),(87612447939578342911/251980320236544000000 : ℚ)],![(88904771208539052272867/847157836635260928000000 : ℚ),(3710895167650064851747781/27109050772328349696000000 : ℚ),(996274355647974301883803/5082947019811565568000000 : ℚ),(24684424333068783169933/82649545037586432000000 : ℚ),(60984721998511680161/125990160118272000000 : ℚ)],![(1046169649501273119041671/6777262693082087424000000 : ℚ),(332143321923876436078907/1694315673270521856000000 : ℚ),(1871578804121979990737/6868847324069683200000 : ℚ),(1045324735332741626351/2582798282424576000000 : ℚ),(40480809992388313003/62995080059136000000 : ℚ)]]
229 refine ⟨⟨4,4,c,?_,?_⟩,(438907059614079603733931/21687240617862679756800000 : ℚ),?_,?_,?_⟩
230 · decide +kernel
231 · apply MvPolynomial.funext
232 intro x
233 norm_num [Rectangle.localPolynomial,cell_33,Rectangle.quarter,Rectangle.half,
234 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
235 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
236 ring
237 · norm_num
238 · decide +kernel
239 · decide +kernel
240
241 def witness : SubdivisionWitness polynomial square :=
242 .of_quarters (fun
243 | false,false => .leaf leaf_0.certificate
244 | false,true => .leaf leaf_1.certificate
245 | true,false => .of_quarters (fun
246 | false,false => .leaf leaf_20.certificate
247 | false,true => .leaf leaf_21.certificate
248 | true,false => .leaf leaf_22.certificate
249 | true,true => .leaf leaf_23.certificate)
250 | true,true => .of_quarters (fun
251 | false,false => .of_quarters (fun
252 | false,false => .leaf leaf_300.certificate
253 | false,true => .leaf leaf_301.certificate
254 | true,false => .leaf leaf_302.certificate
255 | true,true => .leaf leaf_303.certificate)
256 | false,true => .leaf leaf_31.certificate
257 | true,false => .leaf leaf_32.certificate
258 | true,true => .leaf leaf_33.certificate))
259
260 def certifiedWitness : SubdivisionWitness (squareGapPolynomial (nominalProposed false) (1/16) true) square :=
261 polynomial_source ▸ witness
262
263 end
264 end Komorebi.LSM.Section88ProposedDirectNegGap
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: f9b2f44d214063f39ebfabc6b29ad328c7a88ea3a973fa92665bc4bf9973d50b