Large Signal Model · Lean source
Section88ProposedRotatedNegOrientation.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/Section88ProposedRotatedNegOrientation.lean295 lines
Original source path
Lean/KomorebiLSM/Section88ProposedRotatedNegOrientation.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, orientation. -/
5 set_option autoImplicit false
6 set_option maxRecDepth 4000
7 set_option maxHeartbeats 800000
8 namespace Komorebi.LSM.Section88ProposedRotatedNegOrientation
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 (259/1968000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (-259/1968000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^2 +
17 MvPolynomial.C (-6888343/2616000 : ℚ)*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 true) (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 → ℚ := ![![(4883657/2616000 : ℚ),(30033079/21451200 : ℚ),(256697411/171609600 : ℚ)],![(1940657/3488000 : ℚ),(11933629/28601600 : ℚ),(136034411/228812800 : ℚ)],![(1204907/5232000 : ℚ),(14817533/85804800 : ℚ),(105868661/343219200 : ℚ)]]
31 refine ⟨⟨2,2,c,?_,?_⟩,(14817533/85804800 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(256697411/171609600 : ℚ),(27313019/17160960 : ℚ),(4427741/1968000 : ℚ)],![(136034411/228812800 : ℚ),(17659979/22881280 : ℚ),(3320741/2624000 : ℚ)],![(105868661/343219200 : ℚ),(15246719/34321920 : ℚ),(3043991/3936000 : ℚ)]]
46 refine ⟨⟨2,2,c,?_,?_⟩,(105868661/343219200 : ℚ),?_,?_,?_⟩
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_020 : Rectangle := (((square.quarter false false).quarter true false).quarter false false)
59 def leaf_020 : RecordedLeaf polynomial cell_020 := by
60 let c : Fin 3 → Fin 3 → ℚ := ![![(1204907/5232000 : ℚ),(57630013/286016000 : ℚ),(1517254121/6864384000 : ℚ)],![(469157/6976000 : ℚ),(33654957/572032000 : ℚ),(763110371/9152512000 : ℚ)],![(786391/5232000 : ℚ),(150453401/1144064000 : ℚ),(473581499/3432192000 : ℚ)]]
61 refine ⟨⟨2,2,c,?_,?_⟩,(33654957/572032000 : ℚ),?_,?_,?_⟩
62 · decide +kernel
63 · apply MvPolynomial.funext
64 intro x
65 norm_num [Rectangle.localPolynomial,cell_020,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_021 : Rectangle := (((square.quarter false false).quarter true false).quarter false true)
74 def leaf_021 : RecordedLeaf polynomial cell_021 := by
75 let c : Fin 3 → Fin 3 → ℚ := ![![(1517254121/6864384000 : ℚ),(165138793/686438400 : ℚ),(105868661/343219200 : ℚ)],![(763110371/9152512000 : ℚ),(98774143/915251200 : ℚ),(75702911/457625600 : ℚ)],![(473581499/3432192000 : ℚ),(99160559/686438400 : ℚ),(7559471/42902400 : ℚ)]]
76 refine ⟨⟨2,2,c,?_,?_⟩,(763110371/9152512000 : ℚ),?_,?_,?_⟩
77 · decide +kernel
78 · apply MvPolynomial.funext
79 intro x
80 norm_num [Rectangle.localPolynomial,cell_021,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_022 : Rectangle := (((square.quarter false false).quarter true false).quarter true false)
89 def leaf_022 : RecordedLeaf polynomial cell_022 := by
90 let c : Fin 3 → Fin 3 → ℚ := ![![(786391/5232000 : ℚ),(150453401/1144064000 : ℚ),(473581499/3432192000 : ℚ)],![(4883657/20928000 : ℚ),(29199611/143008000 : ℚ),(5287972871/27457536000 : ℚ)],![(9/16 : ℚ),(63/128 : ℚ),(225/512 : ℚ)]]
91 refine ⟨⟨2,2,c,?_,?_⟩,(150453401/1144064000 : ℚ),?_,?_,?_⟩
92 · decide +kernel
93 · apply MvPolynomial.funext
94 intro x
95 norm_num [Rectangle.localPolynomial,cell_022,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_023 : Rectangle := (((square.quarter false false).quarter true false).quarter true true)
104 def leaf_023 : RecordedLeaf polynomial cell_023 := by
105 let c : Fin 3 → Fin 3 → ℚ := ![![(473581499/3432192000 : ℚ),(99160559/686438400 : ℚ),(7559471/42902400 : ℚ)],![(5287972871/27457536000 : ℚ),(496962043/2745753600 : ℚ),(256697411/1372876800 : ℚ)],![(225/512 : ℚ),(99/256 : ℚ),(45/128 : ℚ)]]
106 refine ⟨⟨2,2,c,?_,?_⟩,(473581499/3432192000 : ℚ),?_,?_,?_⟩
107 · decide +kernel
108 · apply MvPolynomial.funext
109 intro x
110 norm_num [Rectangle.localPolynomial,cell_023,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_03 : Rectangle := ((square.quarter false false).quarter true true)
119 def leaf_03 : RecordedLeaf polynomial cell_03 := by
120 let c : Fin 3 → Fin 3 → ℚ := ![![(105868661/343219200 : ℚ),(15246719/34321920 : ℚ),(3043991/3936000 : ℚ)],![(15371411/686438400 : ℚ),(8006939/68643840 : ℚ),(2213741/7872000 : ℚ)],![(45/128 : ℚ),(9/32 : ℚ),(9/32 : ℚ)]]
121 refine ⟨⟨2,2,c,?_,?_⟩,(15371411/686438400 : ℚ),?_,?_,?_⟩
122 · decide +kernel
123 · apply MvPolynomial.funext
124 intro x
125 norm_num [Rectangle.localPolynomial,cell_03,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_1 : Rectangle := (square.quarter false true)
134 def leaf_1 : RecordedLeaf polynomial cell_1 := by
135 let c : Fin 3 → Fin 3 → ℚ := ![![(4427741/1968000 : ℚ),(95630729/26814000 : ℚ),(18660343/2616000 : ℚ)],![(1106741/3936000 : ℚ),(6297763/6703500 : ℚ),(9831343/5232000 : ℚ)],![(9/32 : ℚ),(9/32 : ℚ),(9/16 : ℚ)]]
136 refine ⟨⟨2,2,c,?_,?_⟩,(1106741/3936000 : ℚ),?_,?_,?_⟩
137 · decide +kernel
138 · apply MvPolynomial.funext
139 intro x
140 norm_num [Rectangle.localPolynomial,cell_1,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_2 : Rectangle := (square.quarter true false)
149 def leaf_2 : RecordedLeaf polynomial cell_2 := by
150 let c : Fin 3 → Fin 3 → ℚ := ![![(9/16 : ℚ),(9/32 : ℚ),(9/32 : ℚ)],![(9831343/5232000 : ℚ),(67185549/71504000 : ℚ),(1107259/3936000 : ℚ)],![(18660343/2616000 : ℚ),(127517049/35752000 : ℚ),(4428259/1968000 : ℚ)]]
151 refine ⟨⟨2,2,c,?_,?_⟩,(9/32 : ℚ),?_,?_,?_⟩
152 · decide +kernel
153 · apply MvPolynomial.funext
154 intro x
155 norm_num [Rectangle.localPolynomial,cell_2,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_30 : Rectangle := ((square.quarter true true).quarter false false)
164 def leaf_30 : RecordedLeaf polynomial cell_30 := by
165 let c : Fin 3 → Fin 3 → ℚ := ![![(9/32 : ℚ),(9/32 : ℚ),(45/128 : ℚ)],![(2214259/7872000 : ℚ),(66762133/572032000 : ℚ),(77026441/3432192000 : ℚ)],![(3044509/3936000 : ℚ),(127093633/286016000 : ℚ),(529512691/1716096000 : ℚ)]]
166 refine ⟨⟨2,2,c,?_,?_⟩,(77026441/3432192000 : ℚ),?_,?_,?_⟩
167 · decide +kernel
168 · apply MvPolynomial.funext
169 intro x
170 norm_num [Rectangle.localPolynomial,cell_30,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_310 : Rectangle := (((square.quarter true true).quarter false true).quarter false false)
179 def leaf_310 : RecordedLeaf polynomial cell_310 := by
180 let c : Fin 3 → Fin 3 → ℚ := ![![(45/128 : ℚ),(99/256 : ℚ),(225/512 : ℚ)],![(1283656441/6864384000 : ℚ),(33134567/183050240 : ℚ),(1057673621/5491507200 : ℚ)],![(302463533/1716096000 : ℚ),(3306293/22881280 : ℚ),(189472123/1372876800 : ℚ)]]
181 refine ⟨⟨2,2,c,?_,?_⟩,(189472123/1372876800 : ℚ),?_,?_,?_⟩
182 · decide +kernel
183 · apply MvPolynomial.funext
184 intro x
185 norm_num [Rectangle.localPolynomial,cell_310,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_311 : Rectangle := (((square.quarter true true).quarter false true).quarter false true)
194 def leaf_311 : RecordedLeaf polynomial cell_311 := by
195 let c : Fin 3 → Fin 3 → ℚ := ![![(225/512 : ℚ),(63/128 : ℚ),(9/16 : ℚ)],![(1057673621/5491507200 : ℚ),(140163779/686438400 : ℚ),(4883657/20928000 : ℚ)],![(189472123/1372876800 : ℚ),(90283333/686438400 : ℚ),(786391/5232000 : ℚ)]]
196 refine ⟨⟨2,2,c,?_,?_⟩,(90283333/686438400 : ℚ),?_,?_,?_⟩
197 · decide +kernel
198 · apply MvPolynomial.funext
199 intro x
200 norm_num [Rectangle.localPolynomial,cell_311,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_312 : Rectangle := (((square.quarter true true).quarter false true).quarter true false)
209 def leaf_312 : RecordedLeaf polynomial cell_312 := by
210 let c : Fin 3 → Fin 3 → ℚ := ![![(302463533/1716096000 : ℚ),(3306293/22881280 : ℚ),(189472123/1372876800 : ℚ)],![(378683941/2288128000 : ℚ),(19766121/183050240 : ℚ),(152701121/1830502400 : ℚ)],![(529512691/1716096000 : ℚ),(11013017/45762560 : ℚ),(303529871/1372876800 : ℚ)]]
211 refine ⟨⟨2,2,c,?_,?_⟩,(152701121/1830502400 : ℚ),?_,?_,?_⟩
212 · decide +kernel
213 · apply MvPolynomial.funext
214 intro x
215 norm_num [Rectangle.localPolynomial,cell_312,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_313 : Rectangle := (((square.quarter true true).quarter false true).quarter true true)
224 def leaf_313 : RecordedLeaf polynomial cell_313 := by
225 let c : Fin 3 → Fin 3 → ℚ := ![![(189472123/1372876800 : ℚ),(90283333/686438400 : ℚ),(786391/5232000 : ℚ)],![(152701121/1830502400 : ℚ),(13467629/228812800 : ℚ),(469157/6976000 : ℚ)],![(303529871/1372876800 : ℚ),(17291827/85804800 : ℚ),(1204907/5232000 : ℚ)]]
226 refine ⟨⟨2,2,c,?_,?_⟩,(13467629/228812800 : ℚ),?_,?_,?_⟩
227 · decide +kernel
228 · apply MvPolynomial.funext
229 intro x
230 norm_num [Rectangle.localPolynomial,cell_313,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_32 : Rectangle := ((square.quarter true true).quarter true false)
239 def leaf_32 : RecordedLeaf polynomial cell_32 := by
240 let c : Fin 3 → Fin 3 → ℚ := ![![(3044509/3936000 : ℚ),(127093633/286016000 : ℚ),(529512691/1716096000 : ℚ)],![(3321259/2624000 : ℚ),(441612399/572032000 : ℚ),(680341441/1144064000 : ℚ)],![(4428259/1968000 : ℚ),(227646133/143008000 : ℚ),(1283656441/858048000 : ℚ)]]
241 refine ⟨⟨2,2,c,?_,?_⟩,(529512691/1716096000 : ℚ),?_,?_,?_⟩
242 · decide +kernel
243 · apply MvPolynomial.funext
244 intro x
245 norm_num [Rectangle.localPolynomial,cell_32,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_33 : Rectangle := ((square.quarter true true).quarter true true)
254 def leaf_33 : RecordedLeaf polynomial cell_33 := by
255 let c : Fin 3 → Fin 3 → ℚ := ![![(529512691/1716096000 : ℚ),(9264487/53628000 : ℚ),(1204907/5232000 : ℚ)],![(680341441/1144064000 : ℚ),(119364521/286016000 : ℚ),(1940657/3488000 : ℚ)],![(1283656441/858048000 : ℚ),(300359021/214512000 : ℚ),(4883657/2616000 : ℚ)]]
256 refine ⟨⟨2,2,c,?_,?_⟩,(9264487/53628000 : ℚ),?_,?_,?_⟩
257 · decide +kernel
258 · apply MvPolynomial.funext
259 intro x
260 norm_num [Rectangle.localPolynomial,cell_33,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 witness : SubdivisionWitness polynomial square :=
269 .of_quarters (fun
270 | false,false => .of_quarters (fun
271 | false,false => .leaf leaf_00.certificate
272 | false,true => .leaf leaf_01.certificate
273 | true,false => .of_quarters (fun
274 | false,false => .leaf leaf_020.certificate
275 | false,true => .leaf leaf_021.certificate
276 | true,false => .leaf leaf_022.certificate
277 | true,true => .leaf leaf_023.certificate)
278 | true,true => .leaf leaf_03.certificate)
279 | false,true => .leaf leaf_1.certificate
280 | true,false => .leaf leaf_2.certificate
281 | true,true => .of_quarters (fun
282 | false,false => .leaf leaf_30.certificate
283 | false,true => .of_quarters (fun
284 | false,false => .leaf leaf_310.certificate
285 | false,true => .leaf leaf_311.certificate
286 | true,false => .leaf leaf_312.certificate
287 | true,true => .leaf leaf_313.certificate)
288 | true,false => .leaf leaf_32.certificate
289 | true,true => .leaf leaf_33.certificate))
290
291 def certifiedWitness : SubdivisionWitness (orientationPolynomial (nominalProposed true) (1/16) true) square :=
292 polynomial_source ▸ witness
293
294 end
295 end Komorebi.LSM.Section88ProposedRotatedNegOrientation
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: ba9a6c8a4a1347b94d2593ad9a6ee13e93ba69b0d6c90d7b3fdc0076e8fcff9c