Large Signal Model · Lean source
Section88ProposedDirectPosGap.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/Section88ProposedDirectPosGap.lean264 lines
Original source path
Lean/KomorebiLSM/Section88ProposedDirectPosGap.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.Section88ProposedDirectPosGap
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 (1769118374654253/13382804096000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (856100969275951/4269440916480000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
17 MvPolynomial.C (388856298069010919/1485491254656000000 : ℚ)*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 (-531352814559833/4014841228800000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^4 +
21 MvPolynomial.C (21452330597546779/106736022912000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^3 +
22 MvPolynomial.C (15431789372628797/59419650186240000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^4 +
23 MvPolynomial.C (70516418707807037/3949232847744000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^1 +
24 MvPolynomial.C (892881998260693/26765608192000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^0 +
25 MvPolynomial.C (-104251184003445269/3949232847744000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^3 +
26 MvPolynomial.C (-398310922888487/13382804096000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^4 +
27 MvPolynomial.C (62326278926060499/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^1 +
28 MvPolynomial.C (77469101614088247/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^3 +
29 MvPolynomial.C (5834773688303/2893579264000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^0 +
30 MvPolynomial.C (-74499466744462809/1980655006208000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^2 +
31 MvPolynomial.C (1427106941687/115743170560000 : ℚ)*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 (2036718627769/326409856000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^1 +
37 MvPolynomial.C (6942302319869/326409856000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^3
38
39 theorem polynomial_source : polynomial=squareGapPolynomial (nominalProposed false) (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_00 : Rectangle := ((square.quarter false false).quarter false false)
47 def leaf_00 : RecordedLeaf polynomial cell_00 := by
48 let c : Fin 5 → Fin 5 → ℚ := ![![(99315266031470684539/62995080059136000000 : ℚ),(706561533040941374239/645699570606144000000 : ℚ),(123949724801143811254139/158842094369111424000000 : ℚ),(241148556062060937471301/423578918317630464000000 : ℚ),(2878943274024604614417811/6777262693082087424000000 : ℚ)],![(159801437575934998517/125990160118272000000 : ℚ),(72663766779466333477157/82649545037586432000000 : ℚ),(6352918289110676327252831/10165894039623131136000000 : ℚ),(12293505809451214755935179/27109050772328349696000000 : ℚ),(909872196237460721143399/2710905077232834969600000 : ℚ)],![(251685068583912962023/251980320236544000000 : ℚ),(57081597964542101273341/82649545037586432000000 : ℚ),(621211933869025030486283/1270736754952891392000000 : ℚ),(9556441424374690829634407/27109050772328349696000000 : ℚ),(189393551746195158792319/732677047900766208000000 : ℚ)],![(10518324448614674381/13620557850624000000 : ℚ),(951550876267547768173/1787017190001868800000 : ℚ),(15259575737237158102396523/40663576158492524544000000 : ℚ),(29155951636745061264651127/108436203089313398784000000 : ℚ),(2117754929687354288930611/10843620308931339878400000 : ℚ)],![(86834992742872043/147249274060800000 : ℚ),(9806336286014277743/24148880945971200000 : ℚ),(39223614047392511873479/137376946481393664000000 : ℚ),(298673390826451632438497/1465354095801532416000000 : ℚ),(15961179617631454236913807/108436203089313398784000000 : ℚ)]]
49 refine ⟨⟨4,4,c,?_,?_⟩,(15961179617631454236913807/108436203089313398784000000 : ℚ),?_,?_,?_⟩
50 · decide +kernel
51 · apply MvPolynomial.funext
52 intro x
53 norm_num [Rectangle.localPolynomial,cell_00,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_01 : Rectangle := ((square.quarter false false).quarter false true)
62 def leaf_01 : RecordedLeaf polynomial cell_01 := by
63 let c : Fin 5 → Fin 5 → ℚ := ![![(2878943274024604614417811/6777262693082087424000000 : ℚ),(949754825528117114647403/3388631346541043712000000 : ℚ),(1028090324731490804763433/5082947019811565568000000 : ℚ),(1199636613046137543463/7772090244360192000000 : ℚ),(4606749491508045319/35651790111744000000 : ℚ)],![(909872196237460721143399/2710905077232834969600000 : ℚ),(5903938115297999666932801/27109050772328349696000000 : ℚ),(624297007398306004200419/4066357615849252454400000 : ℚ),(7065786944238863476577/62176721954881536000000 : ℚ),(409097194584783947/4456473763968000000 : ℚ)],![(189393551746195158792319/732677047900766208000000 : ℚ),(495409044982638991221911/3012116752480927744000000 : ℚ),(573187728151997656206179/5082947019811565568000000 : ℚ),(4989811071657962686931/62176721954881536000000 : ℚ),(976430946160221637/15845240049664000000 : ℚ)],![(2117754929687354288930611/10843620308931339878400000 : ℚ),(13199146957002024513961093/108436203089313398784000000 : ℚ),(1316788890971952215751599/16265430463397009817600000 : ℚ),(13674493940200318817069/248706887819526144000000 : ℚ),(1407505640405630329/35651790111744000000 : ℚ)],![(15961179617631454236913807/108436203089313398784000000 : ℚ),(2455132078526371918344709/27109050772328349696000000 : ℚ),(959685121095693467698931/16265430463397009817600000 : ℚ),(2406487421902459224641/62176721954881536000000 : ℚ),(14992938625246704487/570428641787904000000 : ℚ)]]
64 refine ⟨⟨4,4,c,?_,?_⟩,(14992938625246704487/570428641787904000000 : ℚ),?_,?_,?_⟩
65 · decide +kernel
66 · apply MvPolynomial.funext
67 intro x
68 norm_num [Rectangle.localPolynomial,cell_01,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_02 : Rectangle := ((square.quarter false false).quarter true false)
77 def leaf_02 : RecordedLeaf polynomial cell_02 := by
78 let c : Fin 5 → Fin 5 → ℚ := ![![(86834992742872043/147249274060800000 : ℚ),(9806336286014277743/24148880945971200000 : ℚ),(39223614047392511873479/137376946481393664000000 : ℚ),(298673390826451632438497/1465354095801532416000000 : ℚ),(15961179617631454236913807/108436203089313398784000000 : ℚ)],![(2773074604408326787/6810278925312000000 : ℚ),(499786894062565337791/1787017190001868800000 : ℚ),(1592160755763841785340609/8132715231698504908800000 : ℚ),(15047710205569780336246429/108436203089313398784000000 : ℚ),(335775310574667674516297/3388631346541043712000000 : ℚ)],![(16928646177846548041/62995080059136000000 : ℚ),(7646714805290613231503/41324772518793216000000 : ℚ),(52812379669729026241741/406635761584925245440000 : ℚ),(1251160354393525182716029/13554525386164174848000000 : ℚ),(3582383470734264445847/54218101544656699392000 : ℚ)],![(149359998003609227/851284865664000000 : ℚ),(138007732302272803111/1116885743751168000000 : ℚ),(765968615665048866553/8586059155087104000000 : ℚ),(24066887417251189578587/366338523950383104000000 : ℚ),(15252440991633923557/309407537120256000000 : ℚ)],![(1441459854126331/11503849536000000 : ℚ),(8888526397794251/94331566195200000 : ℚ),(34070512758220799609/464111305680384000000 : ℚ),(4564708181222479189/77351884280064000000 : ℚ),(60801472026129273511/1237630148481024000000 : ℚ)]]
79 refine ⟨⟨4,4,c,?_,?_⟩,(60801472026129273511/1237630148481024000000 : ℚ),?_,?_,?_⟩
80 · decide +kernel
81 · apply MvPolynomial.funext
82 intro x
83 norm_num [Rectangle.localPolynomial,cell_02,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_03 : Rectangle := ((square.quarter false false).quarter true true)
92 def leaf_03 : RecordedLeaf polynomial cell_03 := by
93 let c : Fin 5 → Fin 5 → ℚ := ![![(15961179617631454236913807/108436203089313398784000000 : ℚ),(2455132078526371918344709/27109050772328349696000000 : ℚ),(959685121095693467698931/16265430463397009817600000 : ℚ),(2406487421902459224641/62176721954881536000000 : ℚ),(14992938625246704487/570428641787904000000 : ℚ)],![(335775310574667674516297/3388631346541043712000000 : ℚ),(6441909671208950832796579/108436203089313398784000000 : ℚ),(602581351219434719646263/16265430463397009817600000 : ℚ),(5577405435019354980059/248706887819526144000000 : ℚ),(746578700400332371/57042864178790400000 : ℚ)],![(3582383470734264445847/54218101544656699392000 : ℚ),(60003486774845226689719/1506058376240463872000000 : ℚ),(15851001975834277642543/635368377476445696000000 : ℚ),(470633409533740384213/31088360977440768000000 : ℚ),(105060574516551163/11883930037248000000 : ℚ)],![(15252440991633923557/309407537120256000000 : ℚ),(12050892850937941404389/366338523950383104000000 : ℚ),(6487003851811691468399/274753892962787328000000 : ℚ),(2977019027912513489/168045194472652800000 : ℚ),(13930860655148887/963561894912000000 : ℚ)],![(60801472026129273511/1237630148481024000000 : ℚ),(24283806576349439999/618815074240512000000 : ℚ),(31439448896150418679/928222611360768000000 : ℚ),(44149705512374317/1419300628992000000 : ℚ),(201708959642143/6510553344000000 : ℚ)]]
94 refine ⟨⟨4,4,c,?_,?_⟩,(105060574516551163/11883930037248000000 : ℚ),?_,?_,?_⟩
95 · decide +kernel
96 · apply MvPolynomial.funext
97 intro x
98 norm_num [Rectangle.localPolynomial,cell_03,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_10 : Rectangle := ((square.quarter false true).quarter false false)
107 def leaf_10 : RecordedLeaf polynomial cell_10 := by
108 let c : Fin 5 → Fin 5 → ℚ := ![![(4606749491508045319/35651790111744000000 : ℚ),(269635388417123405207/2590696748120064000000 : ℚ),(517014899015935139946097/5082947019811565568000000 : ℚ),(129668773097102669616803/1129543782180347904000000 : ℚ),(1118690827946428647067651/6777262693082087424000000 : ℚ)],![(409097194584783947/4456473763968000000 : ℚ),(483295685939438642279/6908524661653504000000 : ℚ),(1345138782898849155774931/20331788079246262272000000 : ℚ),(223142933959390402666063/3012116752480927744000000 : ℚ),(1494980906107480493779631/13554525386164174848000000 : ℚ)],![(976430946160221637/15845240049664000000 : ℚ),(534643798761491344049/12435344390976307200000 : ℚ),(97212461711719965326509/2541473509905782784000000 : ℚ),(1140958803277404745692481/27109050772328349696000000 : ℚ),(1816944175886400985897699/27109050772328349696000000 : ℚ)],![(1407505640405630329/35651790111744000000 : ℚ),(1987674918246345177713/82902295939842048000000 : ℚ),(61625744302723272442711/3253086092679401963520000 : ℚ),(725096330240743350653537/36145401029771132928000000 : ℚ),(1989860975321660567826011/54218101544656699392000000 : ℚ)],![(14992938625246704487/570428641787904000000 : ℚ),(11492975978684298047/829022959398420480000 : ℚ),(757976396799493283655199/81327152316985049088000000 : ℚ),(83724087615563722548131/9036350257442783232000000 : ℚ),(2246885013044423851519183/108436203089313398784000000 : ℚ)]]
109 refine ⟨⟨4,4,c,?_,?_⟩,(83724087615563722548131/9036350257442783232000000 : ℚ),?_,?_,?_⟩
110 · decide +kernel
111 · apply MvPolynomial.funext
112 intro x
113 norm_num [Rectangle.localPolynomial,cell_10,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_11 : Rectangle := ((square.quarter false true).quarter false true)
122 def leaf_11 : RecordedLeaf polynomial cell_11 := by
123 let c : Fin 5 → Fin 5 → ℚ := ![![(1118690827946428647067651/6777262693082087424000000 : ℚ),(364842254327560319108621/1694315673270521856000000 : ℚ),(384762366776843257011649/1270736754952891392000000 : ℚ),(1160109747183050021219/2582798282424576000000 : ℚ),(44429662622260048183/62995080059136000000 : ℚ)],![(1494980906107480493779631/13554525386164174848000000 : ℚ),(3971637218795408351123957/27109050772328349696000000 : ℚ),(536270625330023905808627/2541473509905782784000000 : ℚ),(26478401285579147641573/82649545037586432000000 : ℚ),(32383102005280770871/62995080059136000000 : ℚ)],![(1816944175886400985897699/27109050772328349696000000 : ℚ),(2492929548495397226102917/27109050772328349696000000 : ℚ),(1402827905760374221613863/10165894039623131136000000 : ℚ),(17988176329306029237017/82649545037586432000000 : ℚ),(91028108374635888481/251980320236544000000 : ℚ)],![(1989860975321660567826011/54218101544656699392000000 : ℚ),(5784154910564412219343433/108436203089313398784000000 : ℚ),(869242810916419382767751/10165894039623131136000000 : ℚ),(9426571819486733815721/66119636030069145600000 : ℚ),(62390429060844125917/251980320236544000000 : ℚ)],![(2246885013044423851519183/108436203089313398784000000 : ℚ),(1744540487351041516230397/54218101544656699392000000 : ℚ),(140142633805389713327501/2541473509905782784000000 : ℚ),(15974605798930266539507/165299090075172864000000 : ℚ),(175483369820119583791/1007921280946176000000 : ℚ)]]
124 refine ⟨⟨4,4,c,?_,?_⟩,(2246885013044423851519183/108436203089313398784000000 : ℚ),?_,?_,?_⟩
125 · decide +kernel
126 · apply MvPolynomial.funext
127 intro x
128 norm_num [Rectangle.localPolynomial,cell_11,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_120 : Rectangle := (((square.quarter false true).quarter true false).quarter false false)
137 def leaf_120 : RecordedLeaf polynomial cell_120 := by
138 let c : Fin 5 → Fin 5 → ℚ := ![![(14992938625246704487/570428641787904000000 : ℚ),(156012719284575821413/7772090244360192000000 : ℚ),(5150471529496025712597163/325308609267940196352000000 : ℚ),(35614175229766730921881/2710905077232834969600000 : ℚ),(4238535017187990215484443/346995849885802876108800000 : ℚ)],![(22458725629250028197/1140857283575808000000 : ℚ),(14172658000429845003053/994827551278104576000000 : ℚ),(34001092423490408258959/3253086092679401963520000 : ℚ),(13771129344886066663082893/1734979249429014380544000000 : ℚ),(23891504235981300182090219/3469958498858028761088000000 : ℚ)],![(11655806736682602577/760571522383872000000 : ℚ),(10595778900412031289881/994827551278104576000000 : ℚ),(1912525693622797692055729/260246887414352157081600000 : ℚ),(2955570952080741458570411/578326416476338126848000000 : ℚ),(28354995314499296197484767/6939916997716057522176000000 : ℚ)],![(60766091875488184193/4563429134303232000000 : ℚ),(37422692190350353900871/3979310205112418304000000 : ℚ),(8647758296122546602600277/1301234437071760785408000000 : ℚ),(33219748918555862832424471/6939916997716057522176000000 : ℚ),(54892192882951285899353411/13879833995432115044352000000 : ℚ)],![(5030989693657011991/365074330744258560000 : ℚ),(21156748513922760168313/1989655102556209152000000 : ℚ),(44109386713688675987685343/5204937748287043141632000000 : ℚ),(24650218117289531660560817/3469958498858028761088000000 : ℚ),(184237142019519683042389687/27759667990864230088704000000 : ℚ)]]
139 refine ⟨⟨4,4,c,?_,?_⟩,(54892192882951285899353411/13879833995432115044352000000 : ℚ),?_,?_,?_⟩
140 · decide +kernel
141 · apply MvPolynomial.funext
142 intro x
143 norm_num [Rectangle.localPolynomial,cell_120,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_121 : Rectangle := (((square.quarter false true).quarter true false).quarter false true)
152 def leaf_121 : RecordedLeaf polynomial cell_121 := by
153 let c : Fin 5 → Fin 5 → ℚ := ![![(4238535017187990215484443/346995849885802876108800000 : ℚ),(1959227802482919436484059/173497924942901438054400000 : ℚ),(15800694934651832712643777/1301234437071760785408000000 : ℚ),(650314812886237704419351/43374481235725359513600000 : ℚ),(2246885013044423851519183/108436203089313398784000000 : ℚ)],![(23891504235981300182090219/3469958498858028761088000000 : ℚ),(5060187445547616759503663/867489624714507190272000000 : ℚ),(16248610577419827174940499/2602468874143521570816000000 : ℚ),(28122744155687612333419/3388631346541043712000000 : ℚ),(2760933088489950418905527/216872406178626797568000000 : ℚ)],![(28354995314499296197484767/6939916997716057522176000000 : ℚ),(10621569602014847446062301/3469958498858028761088000000 : ℚ),(3382989108209429985006817/1040987549657408628326400000 : ℚ),(4165712848342612499555717/867489624714507190272000000 : ℚ),(3611410117085491793351311/433744812357253595136000000 : ℚ)],![(54892192882951285899353411/13879833995432115044352000000 : ℚ),(1083622198219771153346447/346995849885802876108800000 : ℚ),(34540151506499053524315623/10409875496574086283264000000 : ℚ),(4049359350635657961051229/867489624714507190272000000 : ℚ),(6663545767880364870493463/867489624714507190272000000 : ℚ)],![(184237142019519683042389687/27759667990864230088704000000 : ℚ),(85636269550361556400146419/13879833995432115044352000000 : ℚ),(5501749523934599728978033/832790039725926902661120000 : ℚ),(27974702058518713332863383/3469958498858028761088000000 : ℚ),(19028543639406993226776271/1734979249429014380544000000 : ℚ)]]
154 refine ⟨⟨4,4,c,?_,?_⟩,(10621569602014847446062301/3469958498858028761088000000 : ℚ),?_,?_,?_⟩
155 · decide +kernel
156 · apply MvPolynomial.funext
157 intro x
158 norm_num [Rectangle.localPolynomial,cell_121,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_122 : Rectangle := (((square.quarter false true).quarter true false).quarter true false)
167 def leaf_122 : RecordedLeaf polynomial cell_122 := by
168 let c : Fin 5 → Fin 5 → ℚ := ![![(5030989693657011991/365074330744258560000 : ℚ),(21156748513922760168313/1989655102556209152000000 : ℚ),(44109386713688675987685343/5204937748287043141632000000 : ℚ),(24650218117289531660560817/3469958498858028761088000000 : ℚ),(184237142019519683042389687/27759667990864230088704000000 : ℚ)],![(32504325232968557791/2281714567151616000000 : ℚ),(47204301865340686772381/3979310205112418304000000 : ℚ),(26813870121443582782484789/2602468874143521570816000000 : ℚ),(65381123550602263809818797/6939916997716057522176000000 : ℚ),(32336237284142099285759069/3469958498858028761088000000 : ℚ)],![(163374911668736413/9507144029798400000 : ℚ),(3871645934476799431409/248706887819526144000000 : ℚ),(7453508592700186733423/508294701981156556800000 : ℚ),(2078950014355452072034033/144581604119084531712000000 : ℚ),(6425484473007275465072977/433744812357253595136000000 : ℚ)],![(43783786682186051/1927123789824000000 : ℚ),(73516665157710546307/3360903889453056000000 : ℚ),(47670621137152973314621/2198031143702298624000000 : ℚ),(25926198314903930902807/1172283276641225932800000 : ℚ),(68187538072789200806329/2930708191603064832000000 : ℚ)],![(201708959642143/6510553344000000 : ℚ),(17553590818717441/567720251596800000 : ℚ),(23403690522498020987/742578089088614400000 : ℚ),(162267449802675624679/4950520593924096000000 : ℚ),(689657146145967254599/19802082375696384000000 : ℚ)]]
169 refine ⟨⟨4,4,c,?_,?_⟩,(184237142019519683042389687/27759667990864230088704000000 : ℚ),?_,?_,?_⟩
170 · decide +kernel
171 · apply MvPolynomial.funext
172 intro x
173 norm_num [Rectangle.localPolynomial,cell_122,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_123 : Rectangle := (((square.quarter false true).quarter true false).quarter true true)
182 def leaf_123 : RecordedLeaf polynomial cell_123 := by
183 let c : Fin 5 → Fin 5 → ℚ := ![![(184237142019519683042389687/27759667990864230088704000000 : ℚ),(85636269550361556400146419/13879833995432115044352000000 : ℚ),(5501749523934599728978033/832790039725926902661120000 : ℚ),(27974702058518713332863383/3469958498858028761088000000 : ℚ),(19028543639406993226776271/1734979249429014380544000000 : ℚ)],![(32336237284142099285759069/3469958498858028761088000000 : ℚ),(63963825585966133333217479/6939916997716057522176000000 : ℚ),(51501793295932969850067601/5204937748287043141632000000 : ℚ),(795039334289895896430437/69399169977160575221760000 : ℚ),(1545624733940828544535351/108436203089313398784000000 : ℚ)],![(6425484473007275465072977/433744812357253595136000000 : ℚ),(1322823780589638942808771/86748962471450719027200000 : ℚ),(2668074394575438628151677/162654304633970098176000000 : ℚ),(1992872188039836748526773/108436203089313398784000000 : ℚ),(582053888795734704946291/27109050772328349696000000 : ℚ)],![(68187538072789200806329/2930708191603064832000000 : ℚ),(143119160716637148711281/5861416383206129664000000 : ℚ),(115573495987482187925111/4396062287404597248000000 : ℚ),(42486396107447934751843/1465354095801532416000000 : ℚ),(1501521030095528626783/45792315493797888000000 : ℚ)],![(689657146145967254599/19802082375696384000000 : ℚ),(365122246540616005241/9901041187848192000000 : ℚ),(589835851255754687389/14851561781772288000000 : ℚ),(21518520362053176701/495052059392409600000 : ℚ),(11974922227636748267/247526029696204800000 : ℚ)]]
184 refine ⟨⟨4,4,c,?_,?_⟩,(85636269550361556400146419/13879833995432115044352000000 : ℚ),?_,?_,?_⟩
185 · decide +kernel
186 · apply MvPolynomial.funext
187 intro x
188 norm_num [Rectangle.localPolynomial,cell_123,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_13 : Rectangle := ((square.quarter false true).quarter true true)
197 def leaf_13 : RecordedLeaf polynomial cell_13 := by
198 let c : Fin 5 → Fin 5 → ℚ := ![![(2246885013044423851519183/108436203089313398784000000 : ℚ),(1744540487351041516230397/54218101544656699392000000 : ℚ),(140142633805389713327501/2541473509905782784000000 : ℚ),(15974605798930266539507/165299090075172864000000 : ℚ),(175483369820119583791/1007921280946176000000 : ℚ)],![(64256009430690820923293/13554525386164174848000000 : ℚ),(238801407767950769115631/21687240617862679756800000 : ℚ),(251898259526698323852257/10165894039623131136000000 : ℚ),(16765564098287397079423/330598180150345728000000 : ℚ),(50702511698431331957/503960640473088000000 : ℚ)],![(4205361914375185088243/1355452538616417484800000 : ℚ),(98927806316534019610139/13554525386164174848000000 : ℚ),(1345110423847456830263/81327152316985049088000 : ℚ),(1402264414866446618713/41324772518793216000000 : ℚ),(4237440487844742151/62995080059136000000 : ℚ)],![(787681448078258824171/45792315493797888000000 : ℚ),(8265368782268978545741/366338523950383104000000 : ℚ),(879825632479967404637/27475389296278732800000 : ℚ),(53385170184825495983/1116885743751168000000 : ℚ),(25564639374056627/340513946265600000 : ℚ)],![(11974922227636748267/247526029696204800000 : ℚ),(144062463208570681/2475260296962048000 : ℚ),(33722939925241225043/464111305680384000000 : ℚ),(88414298079596203/943315661952000000 : ℚ),(1441459854126331/11503849536000000 : ℚ)]]
199 refine ⟨⟨4,4,c,?_,?_⟩,(4205361914375185088243/1355452538616417484800000 : ℚ),?_,?_,?_⟩
200 · decide +kernel
201 · apply MvPolynomial.funext
202 intro x
203 norm_num [Rectangle.localPolynomial,cell_13,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_2 : Rectangle := (square.quarter true false)
212 def leaf_2 : RecordedLeaf polynomial cell_2 := by
213 let c : Fin 5 → Fin 5 → ℚ := ![![(1441459854126331/11503849536000000 : ℚ),(9928469986254313/157219276992000000 : ℚ),(975505393958251831/23205565284019200000 : ℚ),(738780963712691/23655010483200000 : ℚ),(201708959642143/6510553344000000 : ℚ)],![(5321022902206757/212821216416000000 : ℚ),(858087631657188631/18614762395852800000 : ℚ),(859295437668481328537/17172118310174208000000 : ℚ),(3623294993129478509/70018831030272000000 : ℚ),(30848528385406859/481780947456000000 : ℚ)],![(765476741867911949/7874385007392000000 : ℚ),(293473238425409586659/2582798282424576000000 : ℚ),(14513299804797274800017/127073675495289139200000 : ℚ),(223734490154859954593/1943022561090048000000 : ℚ),(27869161835088243/198065500620800000 : ℚ)],![(10251956003061683579/31497540029568000000 : ℚ),(14881674006157213299/55995626719232000000 : ℚ),(76007455132629010345237/317684188738222848000000 : ℚ),(394290933311894100479/1727131165413376000000 : ℚ),(9602862057808514359/35651790111744000000 : ℚ)],![(40480809992388313003/62995080059136000000 : ℚ),(17066346509866089077/35872198367008000000 : ℚ),(134221438361605587853477/317684188738222848000000 : ℚ),(789288028007643417/1980655006208000000 : ℚ),(3282249967006478291/7130358022348800000 : ℚ)]]
214 refine ⟨⟨4,4,c,?_,?_⟩,(5321022902206757/212821216416000000 : ℚ),?_,?_,?_⟩
215 · decide +kernel
216 · apply MvPolynomial.funext
217 intro x
218 norm_num [Rectangle.localPolynomial,cell_2,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_3 : Rectangle := (square.quarter true true)
227 def leaf_3 : RecordedLeaf polynomial cell_3 := by
228 let c : Fin 5 → Fin 5 → ℚ := ![![(201708959642143/6510553344000000 : ℚ),(5452281072651611/177412578624000000 : ℚ),(4761669358798067633/116027826420096000000 : ℚ),(3664305507552079/58957228872000000 : ℚ),(1441459854126331/11503849536000000 : ℚ)],![(30848528385406859/481780947456000000 : ℚ),(16030031772686345521/210056493090816000000 : ℚ),(425744859593172403139/4293029577543552000000 : ℚ),(40603291039927310729/279221435937792000000 : ℚ),(192180890745762347/851284865664000000 : ℚ)],![(27869161835088243/198065500620800000 : ℚ),(323058465049571373067/1943022561090048000000 : ℚ),(137524378605127641682081/635368377476445696000000 : ℚ),(67911796589089837547/215233190202048000000 : ℚ),(7809292497933838417/15748770014784000000 : ℚ)],![(9602862057808514359/35651790111744000000 : ℚ),(4825077314601977616737/15544180488720384000000 : ℚ),(512730853099487212862599/1270736754952891392000000 : ℚ),(12088869959762691602251/20662386259396608000000 : ℚ),(59577320869439972761/62995080059136000000 : ℚ)],![(3282249967006478291/7130358022348800000 : ℚ),(4653828791481800351/8912947527936000000 : ℚ),(53195234737672324716421/79421047184555712000000 : ℚ),(1239517842989638401061/1291399141212288000000 : ℚ),(100145552482963963039/62995080059136000000 : ℚ)]]
229 refine ⟨⟨4,4,c,?_,?_⟩,(5452281072651611/177412578624000000 : ℚ),?_,?_,?_⟩
230 · decide +kernel
231 · apply MvPolynomial.funext
232 intro x
233 norm_num [Rectangle.localPolynomial,cell_3,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 => .of_quarters (fun
244 | false,false => .leaf leaf_00.certificate
245 | false,true => .leaf leaf_01.certificate
246 | true,false => .leaf leaf_02.certificate
247 | true,true => .leaf leaf_03.certificate)
248 | false,true => .of_quarters (fun
249 | false,false => .leaf leaf_10.certificate
250 | false,true => .leaf leaf_11.certificate
251 | true,false => .of_quarters (fun
252 | false,false => .leaf leaf_120.certificate
253 | false,true => .leaf leaf_121.certificate
254 | true,false => .leaf leaf_122.certificate
255 | true,true => .leaf leaf_123.certificate)
256 | true,true => .leaf leaf_13.certificate)
257 | true,false => .leaf leaf_2.certificate
258 | true,true => .leaf leaf_3.certificate)
259
260 def certifiedWitness : SubdivisionWitness (squareGapPolynomial (nominalProposed false) (1/16) false) square :=
261 polynomial_source ▸ witness
262
263 end
264 end Komorebi.LSM.Section88ProposedDirectPosGap
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: 254898da2812a67e537da290b0908b2cff6220c7c49aa056473961a1e10b9ebc