Large Signal Model · Lean source
Section88ProposedRotatedNegGap.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/Section88ProposedRotatedNegGap.lean215 lines
Original source path
Lean/KomorebiLSM/Section88ProposedRotatedNegGap.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.Section88ProposedRotatedNegGap
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 (-422260412679/334570102400000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (-449987494681791241/1316410949248000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
17 MvPolynomial.C (47411116765089329/178258950558720000 : ℚ)*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 (23049642380303/13382804096000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^4 +
21 MvPolynomial.C (-18039959352220757/52656437969920000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^3 +
22 MvPolynomial.C (1172698248997177007/4456473763968000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^4 +
23 MvPolynomial.C (42370130525931607/11847698543232000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^1 +
24 MvPolynomial.C (-19955088271531/6691402048000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^0 +
25 MvPolynomial.C (-107281396030628911/11847698543232000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^3 +
26 MvPolynomial.C (-31103089579457/26765608192000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^4 +
27 MvPolynomial.C (-263362952468240247/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^1 +
28 MvPolynomial.C (-230597885513430099/2632821898496000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^3 +
29 MvPolynomial.C (-1553525873977/115743170560000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^0 +
30 MvPolynomial.C (840595139279394971871/23532162128757248000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^2 +
31 MvPolynomial.C (10941963700703/2893579264000000 : ℚ)*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 (-608104817709221/35578674304000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^1 +
37 MvPolynomial.C (606975135235679/35578674304000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^3
38
39 theorem polynomial_source : polynomial=squareGapPolynomial (nominalProposed true) (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_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 → ℚ := ![![(24451959701373395983/62995080059136000000 : ℚ),(36512908665504679231/125990160118272000000 : ℚ),(90347388892118493023/377970480354816000000 : ℚ),(213991680405587898643/1007921280946176000000 : ℚ),(825345677548410535591/4031685123784704000000 : ℚ)],![(2676813495242860091/10499180009856000000 : ℚ),(1049361238183433262637/5509969669172428800000 : ℚ),(13237761622152076995769/82649545037586432000000 : ℚ),(32292285369451327385447/220398786766897152000000 : ℚ),(805874285268277492223/5509969669172428800000 : ℚ)],![(113649882887552730143/755940960709632000000 : ℚ),(5571322299562738019141/49589727022551859200000 : ℚ),(186247403127956755385647/1906105132429337088000000 : ℚ),(7621797910839518807587931/81327152316985049088000000 : ℚ),(8012451756860881479621359/81327152316985049088000000 : ℚ)],![(39526132950713551/512155122432000000 : ℚ),(6357392288745018206017/110199393383448576000000 : ℚ),(724897222324065328584697/13554525386164174848000000 : ℚ),(2009170130100442638131291/36145401029771132928000000 : ℚ),(57057940461666955390931/903635025744278323200000 : ℚ)],![(23950398268889311/599596240896000000 : ℚ),(120446771306518022519/4031685123784704000000 : ℚ),(306216362405899102390121/10165894039623131136000000 : ℚ),(1857461222192507959459469/54218101544656699392000000 : ℚ),(4542748049702444175129607/108436203089313398784000000 : ℚ)]]
49 refine ⟨⟨4,4,c,?_,?_⟩,(120446771306518022519/4031685123784704000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(825345677548410535591/4031685123784704000000 : ℚ),(79472463347446947661/403168512378470400000 : ℚ),(630915978915124767241/3023763842838528000000 : ℚ),(1083697904493691477/4623492114432000000 : ℚ),(6108219572007571/21208679424000000 : ℚ)],![(805874285268277492223/5509969669172428800000 : ℚ),(32177657452010871992393/220398786766897152000000 : ℚ),(26303581368143470901957/165299090075172864000000 : ℚ),(498414124467254777/2732442186547200000 : ℚ),(131563071396629917/579703904256000000 : ℚ)],![(8012451756860881479621359/81327152316985049088000000 : ℚ),(8403105602882244151654787/81327152316985049088000000 : ℚ),(1782969609539676047110247/15248841059434696704000000 : ℚ),(25643132463960699938647/186530165864644608000000 : ℚ),(74437106494868747657/427821481340928000000 : ℚ)],![(57057940461666955390931/903635025744278323200000 : ℚ),(2555465106832913793143189/36145401029771132928000000 : ℚ),(2269236909746837389687241/27109050772328349696000000 : ℚ),(8398234571111911360789/82902295939842048000000 : ℚ),(12427467014141212921/95071440297984000000 : ℚ)],![(4542748049702444175129607/108436203089313398784000000 : ℚ),(1342643413754968107835069/27109050772328349696000000 : ℚ),(197328308607979103510119/3253086092679401963520000 : ℚ),(931333245173944517581/12435344390976307200000 : ℚ),(55829406981527087119/570428641787904000000 : ℚ)]]
64 refine ⟨⟨4,4,c,?_,?_⟩,(4542748049702444175129607/108436203089313398784000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(23950398268889311/599596240896000000 : ℚ),(120446771306518022519/4031685123784704000000 : ℚ),(306216362405899102390121/10165894039623131136000000 : ℚ),(1857461222192507959459469/54218101544656699392000000 : ℚ),(4542748049702444175129607/108436203089313398784000000 : ℚ)],![(33339138207336527/12291722938368000000 : ℚ),(136218725606780215013/66119636030069145600000 : ℚ),(275039232274996833366877/40663576158492524544000000 : ℚ),(1402334498468703923444003/108436203089313398784000000 : ℚ),(1119271622002426851673747/54218101544656699392000000 : ℚ)],![(267363104137180103/188985240177408000000 : ℚ),(134993320255979890613/123974317556379648000000 : ℚ),(130479798001509357589531/30497682118869393408000000 : ℚ),(342017036545291410581563/40663576158492524544000000 : ℚ),(54991866988405503213751/4066357615849252454400000 : ℚ)],![(56751066268165981/1399890667980800000 : ℚ),(139419128802204060601/4591641390977024000000 : ℚ),(2382667767597366330739/94128648515028992000000 : ℚ),(34386579950142913412341/1506058376240463872000000 : ℚ),(16795543427961725195267/753029188120231936000000 : ℚ)],![(220845497244887971/1749863334976000000 : ℚ),(1356100268007998831/14348879346803200000 : ℚ),(1725976848472355708523/23532162128757248000000 : ℚ),(691797471568653123199/11766081064378624000000 : ℚ),(9204138042865706316751/188257297030057984000000 : ℚ)]]
79 refine ⟨⟨4,4,c,?_,?_⟩,(134993320255979890613/123974317556379648000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(4542748049702444175129607/108436203089313398784000000 : ℚ),(1342643413754968107835069/27109050772328349696000000 : ℚ),(197328308607979103510119/3253086092679401963520000 : ℚ),(931333245173944517581/12435344390976307200000 : ℚ),(55829406981527087119/570428641787904000000 : ℚ)],![(1119271622002426851673747/54218101544656699392000000 : ℚ),(614950397908200696650197/21687240617862679756800000 : ℚ),(3058704701158443006444227/81327152316985049088000000 : ℚ),(12058626093622046620873/248706887819526144000000 : ℚ),(4636751484775862089/71303580223488000000 : ℚ)],![(54991866988405503213751/4066357615849252454400000 : ℚ),(757820303222818653693457/40663576158492524544000000 : ℚ),(188546174504450055564343/7624420529717348352000000 : ℚ),(2969508017195084373203/93265082932322304000000 : ℚ),(4557730296227044109/106955370335232000000 : ℚ)],![(16795543427961725195267/753029188120231936000000 : ℚ),(32795593761703987368727/1506058376240463872000000 : ℚ),(8735177976170002301149/376514594060115968000000 : ℚ),(89670566256644215711/3454262330826752000000 : ℚ),(839734447199489/26765608192000000 : ℚ)],![(9204138042865706316751/188257297030057984000000 : ℚ),(3669758270316481331159/94128648515028992000000 : ℚ),(1587332194711967762613/47064324257514496000000 : ℚ),(181714697872315281/5834902585856000000 : ℚ),(22581401164127/723394816000000 : ℚ)]]
94 refine ⟨⟨4,4,c,?_,?_⟩,(54991866988405503213751/4066357615849252454400000 : ℚ),?_,?_,?_⟩
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_1 : Rectangle := (square.quarter false true)
107 def leaf_1 : RecordedLeaf polynomial cell_1 := by
108 let c : Fin 5 → Fin 5 → ℚ := ![![(6108219572007571/21208679424000000 : ℚ),(11421123694409803/28896825715200000 : ℚ),(3626079079250740373/5905788755544000000 : ℚ),(33187514866099778123/31497540029568000000 : ℚ),(133626515252720363539/62995080059136000000 : ℚ)],![(7212610586878967/43477792819200000 : ℚ),(89788510210392777713/379126353383424000000 : ℚ),(11354846928229884623701/30993579389094912000000 : ℚ),(12870981082549003371107/20662386259396608000000 : ℚ),(1217302680351111677/984298125924000000 : ℚ)],![(1018413888223756183/13369421291904000000 : ℚ),(694818035314941881423/5829067683270144000000 : ℚ),(360240338932748486055451/1906105132429337088000000 : ℚ),(635093598437232654241/1937098711818432000000 : ℚ),(15409568781091311823/23623155022176000000 : ℚ)],![(843957051326279/26765608192000000 : ℚ),(45805275225534304433/863565582706688000000 : ℚ),(200406931598211554801/2353216212875724800000 : ℚ),(171222636244905747417/1147910347744256000000 : ℚ),(103971709484028333/349972666995200000 : ℚ)],![(22581401164127/723394816000000 : ℚ),(22874418703114323/729362823232000000 : ℚ),(247898216355372976851/5883040532189312000000 : ℚ),(142135252937525791/2242012397938000000 : ℚ),(220845497244887971/1749863334976000000 : ℚ)]]
109 refine ⟨⟨4,4,c,?_,?_⟩,(22581401164127/723394816000000 : ℚ),?_,?_,?_⟩
110 · decide +kernel
111 · apply MvPolynomial.funext
112 intro x
113 norm_num [Rectangle.localPolynomial,cell_1,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_2 : Rectangle := (square.quarter true false)
122 def leaf_2 : RecordedLeaf polynomial cell_2 := by
123 let c : Fin 5 → Fin 5 → ℚ := ![![(220845497244887971/1749863334976000000 : ℚ),(4506337293039581499/71744396734016000000 : ℚ),(48890994135310196837/1176608106437862400000 : ℚ),(9064390697739109/291745129292800000 : ℚ),(22581401164127/723394816000000 : ℚ)],![(1041317652128497921/3499726669952000000 : ℚ),(169956809943488060191/1147910347744256000000 : ℚ),(1976337545878505352163/23532162128757248000000 : ℚ),(45007607548167698401/863565582706688000000 : ℚ),(827066634819119/26765608192000000 : ℚ)],![(283932450422364539/433452385728000000 : ℚ),(429279657649725727/1316410949248000000 : ℚ),(3263553129320914035247/17487203049810432000000 : ℚ),(760020193837101973/6476741870300160000 : ℚ),(1001540362133103343/13369421291904000000 : ℚ)],![(1917028899354466771/1536465367296000000 : ℚ),(1427920202105533791373/2295820695488512000000 : ℚ),(229843538355590612451259/635368377476445696000000 : ℚ),(401141921826503411033/1727131165413376000000 : ℚ),(1448421555430695749/8912947527936000000 : ℚ)],![(80590727441636119/37474765056000000 : ℚ),(7515176808155130333/6999453339904000000 : ℚ),(197823671622466406997649/317684188738222848000000 : ℚ),(10611455253828491619/26986424459584000000 : ℚ),(1993056708154628807/7130358022348800000 : ℚ)]]
124 refine ⟨⟨4,4,c,?_,?_⟩,(827066634819119/26765608192000000 : ℚ),?_,?_,?_⟩
125 · decide +kernel
126 · apply MvPolynomial.funext
127 intro x
128 norm_num [Rectangle.localPolynomial,cell_2,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_30 : Rectangle := ((square.quarter true true).quarter false false)
137 def leaf_30 : RecordedLeaf polynomial cell_30 := by
138 let c : Fin 5 → Fin 5 → ℚ := ![![(22581401164127/723394816000000 : ℚ),(182568465707381483/5834902585856000000 : ℚ),(1601105177427255733277/47064324257514496000000 : ℚ),(741526794556704650097/18825729703005798400000 : ℚ),(1857355187831486828147/37651459406011596800000 : ℚ)],![(831289238945909/26765608192000000 : ℚ),(163460719300237407/6338096019865600000 : ℚ),(1745668909202417088371/75302918812023193600000 : ℚ),(32947794481052156441231/1506058376240463872000000 : ℚ),(16930148845896579434913/753029188120231936000000 : ℚ)],![(4490236191864432749/106955370335232000000 : ℚ),(39036988452929491091/1243534439097630720000 : ℚ),(186606253723138936570417/7624420529717348352000000 : ℚ),(50217493880255015579581/2710905077232834969600000 : ℚ),(274415006288685731233259/20331788079246262272000000 : ℚ)],![(4555967291624411083/71303580223488000000 : ℚ),(789402442249110562679/16580459187968409600000 : ℚ),(3012317531072288993604377/81327152316985049088000000 : ℚ),(202621242594143486902367/7229080205954226585600000 : ℚ),(221954750464001126947709/10843620308931339878400000 : ℚ)],![(54684187027083030607/570428641787904000000 : ℚ),(1512742497848641151693/20725573984960512000000 : ℚ),(959734344422344142804363/16265430463397009817600000 : ℚ),(87038616205134175572301/1807270051488556646400000 : ℚ),(885437242868016269460011/21687240617862679756800000 : ℚ)]]
139 refine ⟨⟨4,4,c,?_,?_⟩,(274415006288685731233259/20331788079246262272000000 : ℚ),?_,?_,?_⟩
140 · decide +kernel
141 · apply MvPolynomial.funext
142 intro x
143 norm_num [Rectangle.localPolynomial,cell_30,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_31 : Rectangle := ((square.quarter true true).quarter false true)
152 def leaf_31 : RecordedLeaf polynomial cell_31 := by
153 let c : Fin 5 → Fin 5 → ℚ := ![![(1857355187831486828147/37651459406011596800000 : ℚ),(22316567865495643561/376514594060115968000 : ℚ),(1736306585508821686521/23532162128757248000000 : ℚ),(13602993481041232123/143488793468032000000 : ℚ),(220845497244887971/1749863334976000000 : ℚ)],![(16930148845896579434913/753029188120231936000000 : ℚ),(939805429798220575633/40704280438931456000000 : ℚ),(192816955135061757409/7530291881202319360000 : ℚ),(140693843737460462247/4591641390977024000000 : ℚ),(17834743039315281/437465833744000000 : ℚ)],![(274415006288685731233259/20331788079246262272000000 : ℚ),(344397616950917691239321/40663576158492524544000000 : ℚ),(133127828013194432600077/30497682118869393408000000 : ℚ),(141407923483903984711/123974317556379648000000 : ℚ),(6524602698230509/4609396101888000000 : ℚ)],![(221954750464001126947709/10843620308931339878400000 : ℚ),(55991054814714809416747/4337448123572535951360000 : ℚ),(138251032063966472857283/20331788079246262272000000 : ℚ),(671965385498144458247/330598180150345728000000 : ℚ),(20024913021464779/7874385007392000000 : ℚ)],![(885437242868016269460011/21687240617862679756800000 : ℚ),(72641109127442243205241/2168724061786267975680000 : ℚ),(12066397241039065764539/406635761584925245440000 : ℚ),(4915230297520913983019/165299090075172864000000 : ℚ),(40491398816798028031/1007921280946176000000 : ℚ)]]
154 refine ⟨⟨4,4,c,?_,?_⟩,(141407923483903984711/123974317556379648000000 : ℚ),?_,?_,?_⟩
155 · decide +kernel
156 · apply MvPolynomial.funext
157 intro x
158 norm_num [Rectangle.localPolynomial,cell_31,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_32 : Rectangle := ((square.quarter true true).quarter true false)
167 def leaf_32 : RecordedLeaf polynomial cell_32 := by
168 let c : Fin 5 → Fin 5 → ℚ := ![![(54684187027083030607/570428641787904000000 : ℚ),(1512742497848641151693/20725573984960512000000 : ℚ),(959734344422344142804363/16265430463397009817600000 : ℚ),(87038616205134175572301/1807270051488556646400000 : ℚ),(885437242868016269460011/21687240617862679756800000 : ℚ)],![(486137571474471817/3802857611919360000 : ℚ),(2718309257181192133383/27634098646614016000000 : ℚ),(2195008637717050811479751/27109050772328349696000000 : ℚ),(164562562348976639225347/2409693401984742195200000 : ℚ),(110580415400669190418717/1807270051488556646400000 : ℚ)],![(2906811633988838273/17112859253637120000 : ℚ),(8263722763093509934681/62176721954881536000000 : ℚ),(137038252058068133076313/1219907284754775736320000 : ℚ),(537034654439689677319673/5421810154465669939200000 : ℚ),(7720576154254953158401931/81327152316985049088000000 : ℚ)],![(5252989920831975677/23767860074496000000 : ℚ),(1210028547411214520523/6908524661653504000000 : ℚ),(1024920101697381606165667/6777262693082087424000000 : ℚ),(416296373337334030766923/3012116752480927744000000 : ℚ),(315130383884778156364837/2259087564360695808000000 : ℚ)],![(1993056708154628807/7130358022348800000 : ℚ),(576866053760505102103/2590696748120064000000 : ℚ),(989994867730204103413309/5082947019811565568000000 : ℚ),(206259728670263817365419/1129543782180347904000000 : ℚ),(1298764472274658567964671/6777262693082087424000000 : ℚ)]]
169 refine ⟨⟨4,4,c,?_,?_⟩,(885437242868016269460011/21687240617862679756800000 : ℚ),?_,?_,?_⟩
170 · decide +kernel
171 · apply MvPolynomial.funext
172 intro x
173 norm_num [Rectangle.localPolynomial,cell_32,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_33 : Rectangle := ((square.quarter true true).quarter true true)
182 def leaf_33 : RecordedLeaf polynomial cell_33 := by
183 let c : Fin 5 → Fin 5 → ℚ := ![![(885437242868016269460011/21687240617862679756800000 : ℚ),(72641109127442243205241/2168724061786267975680000 : ℚ),(12066397241039065764539/406635761584925245440000 : ℚ),(4915230297520913983019/165299090075172864000000 : ℚ),(40491398816798028031/1007921280946176000000 : ℚ)],![(110580415400669190418717/1807270051488556646400000 : ℚ),(78191127231684721134739/1445816041190845317120000 : ℚ),(356129564013313367865539/6777262693082087424000000 : ℚ),(6329651934861837157943/110199393383448576000000 : ℚ),(522797391778990429/6719475206307840000 : ℚ)],![(7720576154254953158401931/81327152316985049088000000 : ℚ),(199611688970663815054291/2198031143702298624000000 : ℚ),(2923540807941115324818079/30497682118869393408000000 : ℚ),(5551660295119771698559/49589727022551859200000 : ℚ),(114854664692661412433/755940960709632000000 : ℚ)],![(315130383884778156364837/2259087564360695808000000 : ℚ),(1272153951066223158617927/9036350257442783232000000 : ℚ),(264954337069678301410351/1694315673270521856000000 : ℚ),(141244752614869821403/744590495834112000000 : ℚ),(293515714989763901/1135046487552000000 : ℚ)],![(1298764472274658567964671/6777262693082087424000000 : ℚ),(9188990354917123187411/45792315493797888000000 : ℚ),(1585963741201933911797/6868847324069683200000 : ℚ),(542915833153991579/1886631323904000000 : ℚ),(18195693709165387/46015398144000000 : ℚ)]]
184 refine ⟨⟨4,4,c,?_,?_⟩,(12066397241039065764539/406635761584925245440000 : ℚ),?_,?_,?_⟩
185 · decide +kernel
186 · apply MvPolynomial.funext
187 intro x
188 norm_num [Rectangle.localPolynomial,cell_33,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 => .of_quarters (fun
199 | false,false => .leaf leaf_00.certificate
200 | false,true => .leaf leaf_01.certificate
201 | true,false => .leaf leaf_02.certificate
202 | true,true => .leaf leaf_03.certificate)
203 | false,true => .leaf leaf_1.certificate
204 | true,false => .leaf leaf_2.certificate
205 | true,true => .of_quarters (fun
206 | false,false => .leaf leaf_30.certificate
207 | false,true => .leaf leaf_31.certificate
208 | true,false => .leaf leaf_32.certificate
209 | true,true => .leaf leaf_33.certificate))
210
211 def certifiedWitness : SubdivisionWitness (squareGapPolynomial (nominalProposed true) (1/16) true) square :=
212 polynomial_source ▸ witness
213
214 end
215 end Komorebi.LSM.Section88ProposedRotatedNegGap
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: 3d07c6b614fbd6383d5931187875683f7a4442ff1e0790b9fe1fae2241581d3b