Large Signal Model · Lean source
Section88ProposedDirectPosOrientation.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/Section88ProposedDirectPosOrientation.lean344 lines
Original source path
Lean/KomorebiLSM/Section88ProposedDirectPosOrientation.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, orientation. -/
5 set_option autoImplicit false
6 set_option maxRecDepth 4000
7 set_option maxHeartbeats 800000
8 namespace Komorebi.LSM.Section88ProposedDirectPosOrientation
9 open TensorBernsteinCertificate RationalBernsteinMargin RationalLorentzMatrix
10 open PerturbedOperatorFixture RecordedBernsteinFixture
11 noncomputable section
12
13 def polynomial : Polynomial₂ := MvPolynomial.C (9/32 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^0 +
14 MvPolynomial.C (9/32 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^2 +
15 MvPolynomial.C (690753/656000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (-690753/656000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^2 +
17 MvPolynomial.C (1381219/872000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
18 MvPolynomial.C (63/32 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^0 +
19 MvPolynomial.C (63/32 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^2
20
21 theorem polynomial_source : polynomial=orientationPolynomial (nominalProposed false) (1/16) false := by
22 apply MvPolynomial.funext
23 intro x
24 norm_num [polynomial,orientationPolynomial,orientationPolynomial,squareGapPolynomial,outputPolynomial,
25 liftPolynomial,denominatorPolynomial,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
26 ring
27
28 def cell_00 : Rectangle := ((square.quarter false false).quarter false false)
29 def leaf_00 : RecordedLeaf polynomial cell_00 := by
30 let c : Fin 3 → Fin 3 → ℚ := ![![(5305219/872000 : ℚ),(28862493/7150400 : ℚ),(161012737/57203200 : ℚ)],![(12972657/3488000 : ℚ),(68488029/28601600 : ℚ),(362375211/228812800 : ℚ)],![(4078969/1744000 : ℚ),(42642111/28601600 : ℚ),(110736487/114406400 : ℚ)]]
31 refine ⟨⟨2,2,c,?_,?_⟩,(110736487/114406400 : ℚ),?_,?_,?_⟩
32 · decide +kernel
33 · apply MvPolynomial.funext
34 intro x
35 norm_num [Rectangle.localPolynomial,cell_00,Rectangle.quarter,Rectangle.half,
36 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
37 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
38 ring
39 · norm_num
40 · decide +kernel
41 · decide +kernel
42
43 def cell_01 : Rectangle := ((square.quarter false false).quarter false true)
44 def leaf_01 : RecordedLeaf polynomial cell_01 := by
45 let c : Fin 3 → Fin 3 → ℚ := ![![(161012737/57203200 : ℚ),(9112553/5720320 : ℚ),(785247/656000 : ℚ)],![(362375211/228812800 : ℚ),(17684619/22881280 : ℚ),(1248741/2624000 : ℚ)],![(110736487/114406400 : ℚ),(5090453/11440640 : ℚ),(323997/1312000 : ℚ)]]
46 refine ⟨⟨2,2,c,?_,?_⟩,(323997/1312000 : ℚ),?_,?_,?_⟩
47 · decide +kernel
48 · apply MvPolynomial.funext
49 intro x
50 norm_num [Rectangle.localPolynomial,cell_01,Rectangle.quarter,Rectangle.half,
51 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
52 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
53 ring
54 · norm_num
55 · decide +kernel
56 · decide +kernel
57
58 def cell_02 : Rectangle := ((square.quarter false false).quarter true false)
59 def leaf_02 : RecordedLeaf polynomial cell_02 := by
60 let c : Fin 3 → Fin 3 → ℚ := ![![(4078969/1744000 : ℚ),(42642111/28601600 : ℚ),(110736487/114406400 : ℚ)],![(3343219/3488000 : ℚ),(16796193/28601600 : ℚ),(80570737/228812800 : ℚ)],![(9/16 : ℚ),(27/64 : ℚ),(45/128 : ℚ)]]
61 refine ⟨⟨2,2,c,?_,?_⟩,(45/128 : ℚ),?_,?_,?_⟩
62 · decide +kernel
63 · apply MvPolynomial.funext
64 intro x
65 norm_num [Rectangle.localPolynomial,cell_02,Rectangle.quarter,Rectangle.half,
66 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
67 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
68 ring
69 · norm_num
70 · decide +kernel
71 · decide +kernel
72
73 def cell_03 : Rectangle := ((square.quarter false false).quarter true true)
74 def leaf_03 : RecordedLeaf polynomial cell_03 := by
75 let c : Fin 3 → Fin 3 → ℚ := ![![(110736487/114406400 : ℚ),(5090453/11440640 : ℚ),(323997/1312000 : ℚ)],![(80570737/228812800 : ℚ),(2677193/22881280 : ℚ),(47247/2624000 : ℚ)],![(45/128 : ℚ),(9/32 : ℚ),(9/32 : ℚ)]]
76 refine ⟨⟨2,2,c,?_,?_⟩,(47247/2624000 : ℚ),?_,?_,?_⟩
77 · decide +kernel
78 · apply MvPolynomial.funext
79 intro x
80 norm_num [Rectangle.localPolynomial,cell_03,Rectangle.quarter,Rectangle.half,
81 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
82 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
83 ring
84 · norm_num
85 · decide +kernel
86 · decide +kernel
87
88 def cell_10 : Rectangle := ((square.quarter false true).quarter false false)
89 def leaf_10 : RecordedLeaf polynomial cell_10 := by
90 let c : Fin 3 → Fin 3 → ℚ := ![![(785247/656000 : ℚ),(114553867/143008000 : ℚ),(352023853/286016000 : ℚ)],![(1248741/2624000 : ℚ),(102335601/572032000 : ℚ),(452756559/1144064000 : ℚ)],![(323997/1312000 : ℚ),(14001367/286016000 : ℚ),(100642603/572032000 : ℚ)]]
91 refine ⟨⟨2,2,c,?_,?_⟩,(14001367/286016000 : ℚ),?_,?_,?_⟩
92 · decide +kernel
93 · apply MvPolynomial.funext
94 intro x
95 norm_num [Rectangle.localPolynomial,cell_10,Rectangle.quarter,Rectangle.half,
96 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
97 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
98 ring
99 · norm_num
100 · decide +kernel
101 · decide +kernel
102
103 def cell_11 : Rectangle := ((square.quarter false true).quarter false true)
104 def leaf_11 : RecordedLeaf polynomial cell_11 := by
105 let c : Fin 3 → Fin 3 → ℚ := ![![(352023853/286016000 : ℚ),(118734993/71504000 : ℚ),(2542781/872000 : ℚ)],![(452756559/1144064000 : ℚ),(175210479/286016000 : ℚ),(4685343/3488000 : ℚ)],![(100642603/572032000 : ℚ),(21660309/71504000 : ℚ),(1316531/1744000 : ℚ)]]
106 refine ⟨⟨2,2,c,?_,?_⟩,(100642603/572032000 : ℚ),?_,?_,?_⟩
107 · decide +kernel
108 · apply MvPolynomial.funext
109 intro x
110 norm_num [Rectangle.localPolynomial,cell_11,Rectangle.quarter,Rectangle.half,
111 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
112 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
113 ring
114 · norm_num
115 · decide +kernel
116 · decide +kernel
117
118 def cell_120 : Rectangle := (((square.quarter false true).quarter true false).quarter false false)
119 def leaf_120 : RecordedLeaf polynomial cell_120 := by
120 let c : Fin 3 → Fin 3 → ℚ := ![![(323997/1312000 : ℚ),(84632713/572032000 : ℚ),(297910763/2288128000 : ℚ)],![(695241/5248000 : ℚ),(133235139/2288128000 : ℚ),(380914539/9152512000 : ℚ)],![(185061/1312000 : ℚ),(104743213/1144064000 : ℚ),(95845097/1144064000 : ℚ)]]
121 refine ⟨⟨2,2,c,?_,?_⟩,(380914539/9152512000 : ℚ),?_,?_,?_⟩
122 · decide +kernel
123 · apply MvPolynomial.funext
124 intro x
125 norm_num [Rectangle.localPolynomial,cell_120,Rectangle.quarter,Rectangle.half,
126 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
127 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
128 ring
129 · norm_num
130 · decide +kernel
131 · decide +kernel
132
133 def cell_121 : Rectangle := (((square.quarter false true).quarter true false).quarter false true)
134 def leaf_121 : RecordedLeaf polynomial cell_121 := by
135 let c : Fin 3 → Fin 3 → ℚ := ![![(297910763/2288128000 : ℚ),(128645337/1144064000 : ℚ),(100642603/572032000 : ℚ)],![(380914539/9152512000 : ℚ),(114444261/4576256000 : ℚ),(151099059/2288128000 : ℚ)],![(95845097/1144064000 : ℚ),(86946981/1144064000 : ℚ),(15722591/143008000 : ℚ)]]
136 refine ⟨⟨2,2,c,?_,?_⟩,(114444261/4576256000 : ℚ),?_,?_,?_⟩
137 · decide +kernel
138 · apply MvPolynomial.funext
139 intro x
140 norm_num [Rectangle.localPolynomial,cell_121,Rectangle.quarter,Rectangle.half,
141 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
142 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
143 ring
144 · norm_num
145 · decide +kernel
146 · decide +kernel
147
148 def cell_122 : Rectangle := (((square.quarter false true).quarter true false).quarter true false)
149 def leaf_122 : RecordedLeaf polynomial cell_122 := by
150 let c : Fin 3 → Fin 3 → ℚ := ![![(185061/1312000 : ℚ),(104743213/1144064000 : ℚ),(95845097/1144064000 : ℚ)],![(785247/5248000 : ℚ),(285737713/2288128000 : ℚ),(1152607013/9152512000 : ℚ)],![(9/32 : ℚ),(9/32 : ℚ),(153/512 : ℚ)]]
151 refine ⟨⟨2,2,c,?_,?_⟩,(95845097/1144064000 : ℚ),?_,?_,?_⟩
152 · decide +kernel
153 · apply MvPolynomial.funext
154 intro x
155 norm_num [Rectangle.localPolynomial,cell_122,Rectangle.quarter,Rectangle.half,
156 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
157 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
158 ring
159 · norm_num
160 · decide +kernel
161 · decide +kernel
162
163 def cell_123 : Rectangle := (((square.quarter false true).quarter true false).quarter true true)
164 def leaf_123 : RecordedLeaf polynomial cell_123 := by
165 let c : Fin 3 → Fin 3 → ℚ := ![![(95845097/1144064000 : ℚ),(86946981/1144064000 : ℚ),(15722591/143008000 : ℚ)],![(1152607013/9152512000 : ℚ),(581131587/4576256000 : ℚ),(352023853/2288128000 : ℚ)],![(153/512 : ℚ),(81/256 : ℚ),(45/128 : ℚ)]]
166 refine ⟨⟨2,2,c,?_,?_⟩,(86946981/1144064000 : ℚ),?_,?_,?_⟩
167 · decide +kernel
168 · apply MvPolynomial.funext
169 intro x
170 norm_num [Rectangle.localPolynomial,cell_123,Rectangle.quarter,Rectangle.half,
171 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
172 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
173 ring
174 · norm_num
175 · decide +kernel
176 · decide +kernel
177
178 def cell_130 : Rectangle := (((square.quarter false true).quarter true true).quarter false false)
179 def leaf_130 : RecordedLeaf polynomial cell_130 := by
180 let c : Fin 3 → Fin 3 → ℚ := ![![(100642603/572032000 : ℚ),(10957003/45762560 : ℚ),(175805943/457625600 : ℚ)],![(151099059/2288128000 : ℚ),(19598079/183050240 : ℚ),(376589079/1830502400 : ℚ)],![(15722591/143008000 : ℚ),(6584579/45762560 : ℚ),(50236017/228812800 : ℚ)]]
181 refine ⟨⟨2,2,c,?_,?_⟩,(151099059/2288128000 : ℚ),?_,?_,?_⟩
182 · decide +kernel
183 · apply MvPolynomial.funext
184 intro x
185 norm_num [Rectangle.localPolynomial,cell_130,Rectangle.quarter,Rectangle.half,
186 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
187 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
188 ring
189 · norm_num
190 · decide +kernel
191 · decide +kernel
192
193 def cell_131 : Rectangle := (((square.quarter false true).quarter true true).quarter false true)
194 def leaf_131 : RecordedLeaf polynomial cell_131 := by
195 let c : Fin 3 → Fin 3 → ℚ := ![![(175805943/457625600 : ℚ),(236369/446900 : ℚ),(1316531/1744000 : ℚ)],![(376589079/1830502400 : ℚ),(69649671/228812800 : ℚ),(3213843/6976000 : ℚ)],![(50236017/228812800 : ℚ),(67549139/228812800 : ℚ),(359789/872000 : ℚ)]]
196 refine ⟨⟨2,2,c,?_,?_⟩,(376589079/1830502400 : ℚ),?_,?_,?_⟩
197 · decide +kernel
198 · apply MvPolynomial.funext
199 intro x
200 norm_num [Rectangle.localPolynomial,cell_131,Rectangle.quarter,Rectangle.half,
201 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
202 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
203 ring
204 · norm_num
205 · decide +kernel
206 · decide +kernel
207
208 def cell_132 : Rectangle := (((square.quarter false true).quarter true true).quarter true false)
209 def leaf_132 : RecordedLeaf polynomial cell_132 := by
210 let c : Fin 3 → Fin 3 → ℚ := ![![(15722591/143008000 : ℚ),(6584579/45762560 : ℚ),(50236017/228812800 : ℚ)],![(352023853/2288128000 : ℚ),(33078553/183050240 : ℚ),(427187193/1830502400 : ℚ)],![(45/128 : ℚ),(99/256 : ℚ),(225/512 : ℚ)]]
211 refine ⟨⟨2,2,c,?_,?_⟩,(15722591/143008000 : ℚ),?_,?_,?_⟩
212 · decide +kernel
213 · apply MvPolynomial.funext
214 intro x
215 norm_num [Rectangle.localPolynomial,cell_132,Rectangle.quarter,Rectangle.half,
216 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
217 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
218 ring
219 · norm_num
220 · decide +kernel
221 · decide +kernel
222
223 def cell_133 : Rectangle := (((square.quarter false true).quarter true true).quarter true true)
224 def leaf_133 : RecordedLeaf polynomial cell_133 := by
225 let c : Fin 3 → Fin 3 → ℚ := ![![(50236017/228812800 : ℚ),(67549139/228812800 : ℚ),(359789/872000 : ℚ)],![(427187193/1830502400 : ℚ),(65448607/228812800 : ℚ),(2542781/6976000 : ℚ)],![(225/512 : ℚ),(63/128 : ℚ),(9/16 : ℚ)]]
226 refine ⟨⟨2,2,c,?_,?_⟩,(50236017/228812800 : ℚ),?_,?_,?_⟩
227 · decide +kernel
228 · apply MvPolynomial.funext
229 intro x
230 norm_num [Rectangle.localPolynomial,cell_133,Rectangle.quarter,Rectangle.half,
231 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
232 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
233 ring
234 · norm_num
235 · decide +kernel
236 · decide +kernel
237
238 def cell_20 : Rectangle := ((square.quarter true false).quarter false false)
239 def leaf_20 : RecordedLeaf polynomial cell_20 := by
240 let c : Fin 3 → Fin 3 → ℚ := ![![(9/16 : ℚ),(27/64 : ℚ),(45/128 : ℚ)],![(580781/3488000 : ℚ),(7336407/28601600 : ℚ),(80313263/228812800 : ℚ)],![(1316531/1744000 : ℚ),(23722539/28601600 : ℚ),(110479013/114406400 : ℚ)]]
241 refine ⟨⟨2,2,c,?_,?_⟩,(580781/3488000 : ℚ),?_,?_,?_⟩
242 · decide +kernel
243 · apply MvPolynomial.funext
244 intro x
245 norm_num [Rectangle.localPolynomial,cell_20,Rectangle.quarter,Rectangle.half,
246 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
247 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
248 ring
249 · norm_num
250 · decide +kernel
251 · decide +kernel
252
253 def cell_21 : Rectangle := ((square.quarter true false).quarter false true)
254 def leaf_21 : RecordedLeaf polynomial cell_21 := by
255 let c : Fin 3 → Fin 3 → ℚ := ![![(45/128 : ℚ),(9/32 : ℚ),(9/32 : ℚ)],![(80313263/228812800 : ℚ),(10193527/22881280 : ℚ),(1428753/2624000 : ℚ)],![(110479013/114406400 : ℚ),(12606787/11440640 : ℚ),(1705503/1312000 : ℚ)]]
256 refine ⟨⟨2,2,c,?_,?_⟩,(9/32 : ℚ),?_,?_,?_⟩
257 · decide +kernel
258 · apply MvPolynomial.funext
259 intro x
260 norm_num [Rectangle.localPolynomial,cell_21,Rectangle.quarter,Rectangle.half,
261 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
262 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
263 ring
264 · norm_num
265 · decide +kernel
266 · decide +kernel
267
268 def cell_22 : Rectangle := ((square.quarter true false).quarter true false)
269 def leaf_22 : RecordedLeaf polynomial cell_22 := by
270 let c : Fin 3 → Fin 3 → ℚ := ![![(1316531/1744000 : ℚ),(23722539/28601600 : ℚ),(110479013/114406400 : ℚ)],![(4685343/3488000 : ℚ),(40108671/28601600 : ℚ),(361602789/228812800 : ℚ)],![(2542781/872000 : ℚ),(19402707/7150400 : ℚ),(160755263/57203200 : ℚ)]]
271 refine ⟨⟨2,2,c,?_,?_⟩,(1316531/1744000 : ℚ),?_,?_,?_⟩
272 · decide +kernel
273 · apply MvPolynomial.funext
274 intro x
275 norm_num [Rectangle.localPolynomial,cell_22,Rectangle.quarter,Rectangle.half,
276 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
277 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
278 ring
279 · norm_num
280 · decide +kernel
281 · decide +kernel
282
283 def cell_23 : Rectangle := ((square.quarter true false).quarter true true)
284 def leaf_23 : RecordedLeaf polynomial cell_23 := by
285 let c : Fin 3 → Fin 3 → ℚ := ![![(110479013/114406400 : ℚ),(12606787/11440640 : ℚ),(1705503/1312000 : ℚ)],![(361602789/228812800 : ℚ),(40233621/22881280 : ℚ),(5393259/2624000 : ℚ)],![(160755263/57203200 : ℚ),(16628887/5720320 : ℚ),(2166753/656000 : ℚ)]]
286 refine ⟨⟨2,2,c,?_,?_⟩,(110479013/114406400 : ℚ),?_,?_,?_⟩
287 · decide +kernel
288 · apply MvPolynomial.funext
289 intro x
290 norm_num [Rectangle.localPolynomial,cell_23,Rectangle.quarter,Rectangle.half,
291 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
292 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
293 ring
294 · norm_num
295 · decide +kernel
296 · decide +kernel
297
298 def cell_3 : Rectangle := (square.quarter true true)
299 def leaf_3 : RecordedLeaf polynomial cell_3 := by
300 let c : Fin 3 → Fin 3 → ℚ := ![![(9/32 : ℚ),(9/32 : ℚ),(9/16 : ℚ)],![(1059753/1312000 : ℚ),(10758941/8938000 : ℚ),(2362219/1744000 : ℚ)],![(2166753/656000 : ℚ),(36600757/8938000 : ℚ),(5305219/872000 : ℚ)]]
301 refine ⟨⟨2,2,c,?_,?_⟩,(9/32 : ℚ),?_,?_,?_⟩
302 · decide +kernel
303 · apply MvPolynomial.funext
304 intro x
305 norm_num [Rectangle.localPolynomial,cell_3,Rectangle.quarter,Rectangle.half,
306 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
307 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
308 ring
309 · norm_num
310 · decide +kernel
311 · decide +kernel
312
313 def witness : SubdivisionWitness polynomial square :=
314 .of_quarters (fun
315 | false,false => .of_quarters (fun
316 | false,false => .leaf leaf_00.certificate
317 | false,true => .leaf leaf_01.certificate
318 | true,false => .leaf leaf_02.certificate
319 | true,true => .leaf leaf_03.certificate)
320 | false,true => .of_quarters (fun
321 | false,false => .leaf leaf_10.certificate
322 | false,true => .leaf leaf_11.certificate
323 | true,false => .of_quarters (fun
324 | false,false => .leaf leaf_120.certificate
325 | false,true => .leaf leaf_121.certificate
326 | true,false => .leaf leaf_122.certificate
327 | true,true => .leaf leaf_123.certificate)
328 | true,true => .of_quarters (fun
329 | false,false => .leaf leaf_130.certificate
330 | false,true => .leaf leaf_131.certificate
331 | true,false => .leaf leaf_132.certificate
332 | true,true => .leaf leaf_133.certificate))
333 | true,false => .of_quarters (fun
334 | false,false => .leaf leaf_20.certificate
335 | false,true => .leaf leaf_21.certificate
336 | true,false => .leaf leaf_22.certificate
337 | true,true => .leaf leaf_23.certificate)
338 | true,true => .leaf leaf_3.certificate)
339
340 def certifiedWitness : SubdivisionWitness (orientationPolynomial (nominalProposed false) (1/16) false) square :=
341 polynomial_source ▸ witness
342
343 end
344 end Komorebi.LSM.Section88ProposedDirectPosOrientation
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: f6047664c2c171710143b256768b8c22d2cce0ce09d5bc5d6b6d7c9e2a2a7092