Large Signal Model · Lean source
Section88ComparisonDirectNegOrientation.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/Section88ComparisonDirectNegOrientation.lean382 lines
Original source path
Lean/KomorebiLSM/Section88ComparisonDirectNegOrientation.leanSkip declarations and read code
1 import KomorebiLSM.PerturbedOperatorFixture
2 import KomorebiLSM.RecordedBernsteinFixture
3
4 /-! Exact rational replay of robust_comparison_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.Section88ComparisonDirectNegOrientation
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 (-168021/160000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (168021/160000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^2 +
17 MvPolynomial.C (-251979/160000 : ℚ)*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 (nominalComparison false) (1/16) true := 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 → ℚ := ![![(468021/160000 : ℚ),(348021/128000 : ℚ),(360021/128000 : ℚ)],![(864063/640000 : ℚ),(720063/512000 : ℚ),(810063/512000 : ℚ)],![(243021/320000 : ℚ),(213021/256000 : ℚ),(247521/256000 : ℚ)]]
31 refine ⟨⟨2,2,c,?_,?_⟩,(243021/320000 : ℚ),?_,?_,?_⟩
32 · intro i j
33 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
34 · apply MvPolynomial.funext
35 intro x
36 norm_num [Rectangle.localPolynomial,cell_00,Rectangle.quarter,Rectangle.half,
37 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
38 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
39 ring
40 · norm_num
41 · intro i j
42 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
43 · exact ⟨2,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
44
45 def cell_01 : Rectangle := ((square.quarter false false).quarter false true)
46 def leaf_01 : RecordedLeaf polynomial cell_01 := by
47 let c : Fin 3 → Fin 3 → ℚ := ![![(360021/128000 : ℚ),(372021/128000 : ℚ),(528021/160000 : ℚ)],![(810063/512000 : ℚ),(900063/512000 : ℚ),(1314063/640000 : ℚ)],![(247521/256000 : ℚ),(282021/256000 : ℚ),(415521/320000 : ℚ)]]
48 refine ⟨⟨2,2,c,?_,?_⟩,(247521/256000 : ℚ),?_,?_,?_⟩
49 · intro i j
50 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
51 · apply MvPolynomial.funext
52 intro x
53 norm_num [Rectangle.localPolynomial,cell_01,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 · intro i j
59 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
60 · exact ⟨2,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
61
62 def cell_02 : Rectangle := ((square.quarter false false).quarter true false)
63 def leaf_02 : RecordedLeaf polynomial cell_02 := by
64 let c : Fin 3 → Fin 3 → ℚ := ![![(243021/320000 : ℚ),(213021/256000 : ℚ),(247521/256000 : ℚ)],![(108021/640000 : ℚ),(132021/512000 : ℚ),(180021/512000 : ℚ)],![(9/16 : ℚ),(27/64 : ℚ),(45/128 : ℚ)]]
65 refine ⟨⟨2,2,c,?_,?_⟩,(108021/640000 : ℚ),?_,?_,?_⟩
66 · intro i j
67 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
68 · apply MvPolynomial.funext
69 intro x
70 norm_num [Rectangle.localPolynomial,cell_02,Rectangle.quarter,Rectangle.half,
71 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
72 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
73 ring
74 · norm_num
75 · intro i j
76 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
77 · exact ⟨1,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
78
79 def cell_03 : Rectangle := ((square.quarter false false).quarter true true)
80 def leaf_03 : RecordedLeaf polynomial cell_03 := by
81 let c : Fin 3 → Fin 3 → ℚ := ![![(247521/256000 : ℚ),(282021/256000 : ℚ),(415521/320000 : ℚ)],![(180021/512000 : ℚ),(228021/512000 : ℚ),(348021/640000 : ℚ)],![(45/128 : ℚ),(9/32 : ℚ),(9/32 : ℚ)]]
82 refine ⟨⟨2,2,c,?_,?_⟩,(9/32 : ℚ),?_,?_,?_⟩
83 · intro i j
84 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
85 · apply MvPolynomial.funext
86 intro x
87 norm_num [Rectangle.localPolynomial,cell_03,Rectangle.quarter,Rectangle.half,
88 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
89 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
90 ring
91 · norm_num
92 · intro i j
93 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
94 · exact ⟨2,1,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
95
96 def cell_1 : Rectangle := (square.quarter false true)
97 def leaf_1 : RecordedLeaf polynomial cell_1 := by
98 let c : Fin 3 → Fin 3 → ℚ := ![![(528021/160000 : ℚ),(1308021/320000 : ℚ),(971979/160000 : ℚ)],![(258021/320000 : ℚ),(768021/640000 : ℚ),(431979/320000 : ℚ)],![(9/32 : ℚ),(9/32 : ℚ),(9/16 : ℚ)]]
99 refine ⟨⟨2,2,c,?_,?_⟩,(9/32 : ℚ),?_,?_,?_⟩
100 · intro i j
101 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
102 · apply MvPolynomial.funext
103 intro x
104 norm_num [Rectangle.localPolynomial,cell_1,Rectangle.quarter,Rectangle.half,
105 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
106 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
107 ring
108 · norm_num
109 · intro i j
110 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
111 · exact ⟨2,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
112
113 def cell_20 : Rectangle := ((square.quarter true false).quarter false false)
114 def leaf_20 : RecordedLeaf polynomial cell_20 := by
115 let c : Fin 3 → Fin 3 → ℚ := ![![(9/16 : ℚ),(27/64 : ℚ),(45/128 : ℚ)],![(611979/640000 : ℚ),(299979/512000 : ℚ),(179979/512000 : ℚ)],![(746979/320000 : ℚ),(380979/256000 : ℚ),(247479/256000 : ℚ)]]
116 refine ⟨⟨2,2,c,?_,?_⟩,(179979/512000 : ℚ),?_,?_,?_⟩
117 · intro i j
118 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
119 · apply MvPolynomial.funext
120 intro x
121 norm_num [Rectangle.localPolynomial,cell_20,Rectangle.quarter,Rectangle.half,
122 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
123 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
124 ring
125 · norm_num
126 · intro i j
127 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
128 · exact ⟨1,2,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
129
130 def cell_21 : Rectangle := ((square.quarter true false).quarter false true)
131 def leaf_21 : RecordedLeaf polynomial cell_21 := by
132 let c : Fin 3 → Fin 3 → ℚ := ![![(45/128 : ℚ),(9/32 : ℚ),(9/32 : ℚ)],![(179979/512000 : ℚ),(59979/512000 : ℚ),(11979/640000 : ℚ)],![(247479/256000 : ℚ),(113979/256000 : ℚ),(79479/320000 : ℚ)]]
133 refine ⟨⟨2,2,c,?_,?_⟩,(11979/640000 : ℚ),?_,?_,?_⟩
134 · intro i j
135 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
136 · apply MvPolynomial.funext
137 intro x
138 norm_num [Rectangle.localPolynomial,cell_21,Rectangle.quarter,Rectangle.half,
139 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
140 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
141 ring
142 · norm_num
143 · intro i j
144 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
145 · exact ⟨1,2,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
146
147 def cell_22 : Rectangle := ((square.quarter true false).quarter true false)
148 def leaf_22 : RecordedLeaf polynomial cell_22 := by
149 let c : Fin 3 → Fin 3 → ℚ := ![![(746979/320000 : ℚ),(380979/256000 : ℚ),(247479/256000 : ℚ)],![(2375937/640000 : ℚ),(1223937/512000 : ℚ),(809937/512000 : ℚ)],![(971979/160000 : ℚ),(515979/128000 : ℚ),(359979/128000 : ℚ)]]
150 refine ⟨⟨2,2,c,?_,?_⟩,(247479/256000 : ℚ),?_,?_,?_⟩
151 · intro i j
152 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
153 · apply MvPolynomial.funext
154 intro x
155 norm_num [Rectangle.localPolynomial,cell_22,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 · intro i j
161 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
162 · exact ⟨0,2,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
163
164 def cell_23 : Rectangle := ((square.quarter true false).quarter true true)
165 def leaf_23 : RecordedLeaf polynomial cell_23 := by
166 let c : Fin 3 → Fin 3 → ℚ := ![![(247479/256000 : ℚ),(113979/256000 : ℚ),(79479/320000 : ℚ)],![(809937/512000 : ℚ),(395937/512000 : ℚ),(305937/640000 : ℚ)],![(359979/128000 : ℚ),(203979/128000 : ℚ),(191979/160000 : ℚ)]]
167 refine ⟨⟨2,2,c,?_,?_⟩,(79479/320000 : ℚ),?_,?_,?_⟩
168 · intro i j
169 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
170 · apply MvPolynomial.funext
171 intro x
172 norm_num [Rectangle.localPolynomial,cell_23,Rectangle.quarter,Rectangle.half,
173 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
174 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
175 ring
176 · norm_num
177 · intro i j
178 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
179 · exact ⟨0,2,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
180
181 def cell_300 : Rectangle := (((square.quarter true true).quarter false false).quarter false false)
182 def leaf_300 : RecordedLeaf polynomial cell_300 := by
183 let c : Fin 3 → Fin 3 → ℚ := ![![(9/32 : ℚ),(9/32 : ℚ),(153/512 : ℚ)],![(191979/1280000 : ℚ),(1283853/10240000 : ℚ),(2591769/20480000 : ℚ)],![(90729/640000 : ℚ),(473853/5120000 : ℚ),(870519/10240000 : ℚ)]]
184 refine ⟨⟨2,2,c,?_,?_⟩,(870519/10240000 : ℚ),?_,?_,?_⟩
185 · intro i j
186 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
187 · apply MvPolynomial.funext
188 intro x
189 norm_num [Rectangle.localPolynomial,cell_300,Rectangle.quarter,Rectangle.half,
190 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
191 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
192 ring
193 · norm_num
194 · intro i j
195 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
196 · exact ⟨2,2,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
197
198 def cell_301 : Rectangle := (((square.quarter true true).quarter false false).quarter false true)
199 def leaf_301 : RecordedLeaf polynomial cell_301 := by
200 let c : Fin 3 → Fin 3 → ℚ := ![![(153/512 : ℚ),(81/256 : ℚ),(45/128 : ℚ)],![(2591769/20480000 : ℚ),(326979/2560000 : ℚ),(791979/5120000 : ℚ)],![(870519/10240000 : ℚ),(198333/2560000 : ℚ),(285729/2560000 : ℚ)]]
201 refine ⟨⟨2,2,c,?_,?_⟩,(198333/2560000 : ℚ),?_,?_,?_⟩
202 · intro i j
203 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
204 · apply MvPolynomial.funext
205 intro x
206 norm_num [Rectangle.localPolynomial,cell_301,Rectangle.quarter,Rectangle.half,
207 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
208 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
209 ring
210 · norm_num
211 · intro i j
212 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
213 · exact ⟨2,1,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
214
215 def cell_302 : Rectangle := (((square.quarter true true).quarter false false).quarter true false)
216 def leaf_302 : RecordedLeaf polynomial cell_302 := by
217 let c : Fin 3 → Fin 3 → ℚ := ![![(90729/640000 : ℚ),(473853/5120000 : ℚ),(870519/10240000 : ℚ)],![(170937/1280000 : ℚ),(611559/10240000 : ℚ),(890307/20480000 : ℚ)],![(79479/320000 : ℚ),(383853/2560000 : ℚ),(679269/5120000 : ℚ)]]
218 refine ⟨⟨2,2,c,?_,?_⟩,(890307/20480000 : ℚ),?_,?_,?_⟩
219 · intro i j
220 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
221 · apply MvPolynomial.funext
222 intro x
223 norm_num [Rectangle.localPolynomial,cell_302,Rectangle.quarter,Rectangle.half,
224 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
225 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
226 ring
227 · norm_num
228 · intro i j
229 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
230 · exact ⟨1,2,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
231
232 def cell_303 : Rectangle := (((square.quarter true true).quarter false false).quarter true true)
233 def leaf_303 : RecordedLeaf polynomial cell_303 := by
234 let c : Fin 3 → Fin 3 → ℚ := ![![(870519/10240000 : ℚ),(198333/2560000 : ℚ),(285729/2560000 : ℚ)],![(890307/20480000 : ℚ),(69687/2560000 : ℚ),(350937/5120000 : ℚ)],![(679269/5120000 : ℚ),(36927/320000 : ℚ),(229479/1280000 : ℚ)]]
235 refine ⟨⟨2,2,c,?_,?_⟩,(69687/2560000 : ℚ),?_,?_,?_⟩
236 · intro i j
237 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
238 · apply MvPolynomial.funext
239 intro x
240 norm_num [Rectangle.localPolynomial,cell_303,Rectangle.quarter,Rectangle.half,
241 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
242 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
243 ring
244 · norm_num
245 · intro i j
246 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
247 · exact ⟨1,1,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
248
249 def cell_310 : Rectangle := (((square.quarter true true).quarter false true).quarter false false)
250 def leaf_310 : RecordedLeaf polynomial cell_310 := by
251 let c : Fin 3 → Fin 3 → ℚ := ![![(45/128 : ℚ),(99/256 : ℚ),(225/512 : ℚ)],![(791979/5120000 : ℚ),(93/512 : ℚ),(960021/4096000 : ℚ)],![(285729/2560000 : ℚ),(597/4096 : ℚ),(453771/2048000 : ℚ)]]
252 refine ⟨⟨2,2,c,?_,?_⟩,(285729/2560000 : ℚ),?_,?_,?_⟩
253 · intro i j
254 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
255 · apply MvPolynomial.funext
256 intro x
257 norm_num [Rectangle.localPolynomial,cell_310,Rectangle.quarter,Rectangle.half,
258 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
259 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
260 ring
261 · norm_num
262 · intro i j
263 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
264 · exact ⟨2,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
265
266 def cell_311 : Rectangle := (((square.quarter true true).quarter false true).quarter false true)
267 def leaf_311 : RecordedLeaf polynomial cell_311 := by
268 let c : Fin 3 → Fin 3 → ℚ := ![![(225/512 : ℚ),(63/128 : ℚ),(9/16 : ℚ)],![(960021/4096000 : ℚ),(588021/2048000 : ℚ),(468021/1280000 : ℚ)],![(453771/2048000 : ℚ),(304521/1024000 : ℚ),(265521/640000 : ℚ)]]
269 refine ⟨⟨2,2,c,?_,?_⟩,(453771/2048000 : ℚ),?_,?_,?_⟩
270 · intro i j
271 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
272 · apply MvPolynomial.funext
273 intro x
274 norm_num [Rectangle.localPolynomial,cell_311,Rectangle.quarter,Rectangle.half,
275 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
276 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
277 ring
278 · norm_num
279 · intro i j
280 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
281 · exact ⟨2,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
282
283 def cell_312 : Rectangle := (((square.quarter true true).quarter false true).quarter true false)
284 def leaf_312 : RecordedLeaf polynomial cell_312 := by
285 let c : Fin 3 → Fin 3 → ℚ := ![![(285729/2560000 : ℚ),(597/4096 : ℚ),(453771/2048000 : ℚ)],![(350937/5120000 : ℚ),(225/2048 : ℚ),(855063/4096000 : ℚ)],![(229479/1280000 : ℚ),(249/1024 : ℚ),(397521/1024000 : ℚ)]]
286 refine ⟨⟨2,2,c,?_,?_⟩,(350937/5120000 : ℚ),?_,?_,?_⟩
287 · intro i j
288 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
289 · apply MvPolynomial.funext
290 intro x
291 norm_num [Rectangle.localPolynomial,cell_312,Rectangle.quarter,Rectangle.half,
292 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
293 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
294 ring
295 · norm_num
296 · intro i j
297 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
298 · exact ⟨1,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
299
300 def cell_313 : Rectangle := (((square.quarter true true).quarter false true).quarter true true)
301 def leaf_313 : RecordedLeaf polynomial cell_313 := by
302 let c : Fin 3 → Fin 3 → ℚ := ![![(453771/2048000 : ℚ),(304521/1024000 : ℚ),(265521/640000 : ℚ)],![(855063/4096000 : ℚ),(630063/2048000 : ℚ),(594063/1280000 : ℚ)],![(397521/1024000 : ℚ),(273021/512000 : ℚ),(243021/320000 : ℚ)]]
303 refine ⟨⟨2,2,c,?_,?_⟩,(855063/4096000 : ℚ),?_,?_,?_⟩
304 · intro i j
305 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
306 · apply MvPolynomial.funext
307 intro x
308 norm_num [Rectangle.localPolynomial,cell_313,Rectangle.quarter,Rectangle.half,
309 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
310 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
311 ring
312 · norm_num
313 · intro i j
314 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
315 · exact ⟨1,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
316
317 def cell_32 : Rectangle := ((square.quarter true true).quarter true false)
318 def leaf_32 : RecordedLeaf polynomial cell_32 := by
319 let c : Fin 3 → Fin 3 → ℚ := ![![(79479/320000 : ℚ),(65937/1280000 : ℚ),(229479/1280000 : ℚ)],![(305937/640000 : ℚ),(467811/2560000 : ℚ),(1025937/2560000 : ℚ)],![(191979/160000 : ℚ),(515937/640000 : ℚ),(791979/640000 : ℚ)]]
320 refine ⟨⟨2,2,c,?_,?_⟩,(65937/1280000 : ℚ),?_,?_,?_⟩
321 · intro i j
322 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
323 · apply MvPolynomial.funext
324 intro x
325 norm_num [Rectangle.localPolynomial,cell_32,Rectangle.quarter,Rectangle.half,
326 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
327 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
328 ring
329 · norm_num
330 · intro i j
331 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
332 · exact ⟨0,1,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
333
334 def cell_33 : Rectangle := ((square.quarter true true).quarter true true)
335 def leaf_33 : RecordedLeaf polynomial cell_33 := by
336 let c : Fin 3 → Fin 3 → ℚ := ![![(229479/1280000 : ℚ),(393021/1280000 : ℚ),(243021/320000 : ℚ)],![(1025937/2560000 : ℚ),(1584063/2560000 : ℚ),(864063/640000 : ℚ)],![(791979/640000 : ℚ),(1068021/640000 : ℚ),(468021/160000 : ℚ)]]
337 refine ⟨⟨2,2,c,?_,?_⟩,(229479/1280000 : ℚ),?_,?_,?_⟩
338 · intro i j
339 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
340 · apply MvPolynomial.funext
341 intro x
342 norm_num [Rectangle.localPolynomial,cell_33,Rectangle.quarter,Rectangle.half,
343 Rectangle.lower,Rectangle.upper,Rectangle.width,square,polynomial,c,tensorPolynomial,
344 basisPolynomial,Nat.choose,Fin.sum_univ_succ,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
345 ring
346 · norm_num
347 · intro i j
348 fin_cases i <;> fin_cases j <;> norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]
349 · exact ⟨0,0,by norm_num [c,Matrix.cons_val_two,Matrix.cons_val_three,Matrix.cons_val_four]⟩
350
351 def witness : SubdivisionWitness polynomial square :=
352 .of_quarters (fun
353 | false,false => .of_quarters (fun
354 | false,false => .leaf leaf_00.certificate
355 | false,true => .leaf leaf_01.certificate
356 | true,false => .leaf leaf_02.certificate
357 | true,true => .leaf leaf_03.certificate)
358 | false,true => .leaf leaf_1.certificate
359 | true,false => .of_quarters (fun
360 | false,false => .leaf leaf_20.certificate
361 | false,true => .leaf leaf_21.certificate
362 | true,false => .leaf leaf_22.certificate
363 | true,true => .leaf leaf_23.certificate)
364 | true,true => .of_quarters (fun
365 | false,false => .of_quarters (fun
366 | false,false => .leaf leaf_300.certificate
367 | false,true => .leaf leaf_301.certificate
368 | true,false => .leaf leaf_302.certificate
369 | true,true => .leaf leaf_303.certificate)
370 | false,true => .of_quarters (fun
371 | false,false => .leaf leaf_310.certificate
372 | false,true => .leaf leaf_311.certificate
373 | true,false => .leaf leaf_312.certificate
374 | true,true => .leaf leaf_313.certificate)
375 | true,false => .leaf leaf_32.certificate
376 | true,true => .leaf leaf_33.certificate))
377
378 def certifiedWitness : SubdivisionWitness (orientationPolynomial (nominalComparison false) (1/16) true) square :=
379 polynomial_source ▸ witness
380
381 end
382 end Komorebi.LSM.Section88ComparisonDirectNegOrientation
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: 4ffbfc567e5ed8ff1a46db2418b52477ce92d5f24ef2b26053f715629f1f56b1