Large Signal Model · Lean source
Section88ComparisonDirectPosGap.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/Section88ComparisonDirectPosGap.lean264 lines
Original source path
Lean/KomorebiLSM/Section88ComparisonDirectPosGap.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, cone_gap. -/
5 set_option autoImplicit false
6 set_option maxRecDepth 4000
7 set_option maxHeartbeats 800000
8 namespace Komorebi.LSM.Section88ComparisonDirectPosGap
9 open TensorBernsteinCertificate RationalBernsteinMargin RationalLorentzMatrix
10 open PerturbedOperatorFixture RecordedBernsteinFixture
11 noncomputable section
12
13 def polynomial : Polynomial₂ := MvPolynomial.C (39656363/1280000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^0 +
14 MvPolynomial.C (40537971/640000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^2 +
15 MvPolynomial.C (15437009/120000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (92782613/480000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
17 MvPolynomial.C (55526301089/230400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^0 +
18 MvPolynomial.C (108793982311/230400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^2 +
19 MvPolynomial.C (39656363/1280000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^4 +
20 MvPolynomial.C (-61821389/480000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^4 +
21 MvPolynomial.C (23251403/120000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^3 +
22 MvPolynomial.C (55049844689/230400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^4 +
23 MvPolynomial.C (-319712113/38400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^1 +
24 MvPolynomial.C (-864703/960000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^0 +
25 MvPolynomial.C (-9548287/38400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^3 +
26 MvPolynomial.C (4309697/960000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^4 +
27 MvPolynomial.C (-31230493/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^1 +
28 MvPolynomial.C (-20126407/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^3 +
29 MvPolynomial.C (-18767/4000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^0 +
30 MvPolynomial.C (2671039/1024000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^2 +
31 MvPolynomial.C (2891/512000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^4 +
32 MvPolynomial.C (-319039/320000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^1 +
33 MvPolynomial.C (36309/80000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^2 +
34 MvPolynomial.C (319039/320000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^3 +
35 MvPolynomial.C (-31211089/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^2 +
36 MvPolynomial.C (89719/6400000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^1 +
37 MvPolynomial.C (1732689/128000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^3
38
39 theorem polynomial_source : polynomial=squareGapPolynomial (nominalComparison 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 → ℚ := ![![(41319071593/28800000000 : ℚ),(31068856339/30720000000 : ℚ),(404873800849/552960000000 : ℚ),(26637373423/49152000000 : ℚ),(60503950049/147456000000 : ℚ)],![(357410696599/307200000000 : ℚ),(200707741139/245760000000 : ℚ),(866928569773/1474560000000 : ℚ),(84925432429/196608000000 : ℚ),(63648508129/196608000000 : ℚ)],![(5111969516807/5529600000000 : ℚ),(952110964669/1474560000000 : ℚ),(12257068188449/26542080000000 : ℚ),(396851348189/1179648000000 : ℚ),(881950278557/3538944000000 : ℚ)],![(110778033631/153600000000 : ℚ),(61596722801/122880000000 : ℚ),(131321990051/368640000000 : ℚ),(50597897957/196608000000 : ℚ),(74103625189/393216000000 : ℚ)],![(2048157664571/3686400000000 : ℚ),(126167891889/327680000000 : ℚ),(4822852560827/17694720000000 : ℚ),(25674313897/131072000000 : ℚ),(10497636823/73728000000 : ℚ)]]
49 refine ⟨⟨4,4,c,?_,?_⟩,(10497636823/73728000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(60503950049/147456000000 : ℚ),(41095779829/147456000000 : ℚ),(113751247549/552960000000 : ℚ),(29692160119/184320000000 : ℚ),(32151938669/230400000000 : ℚ)],![(63648508129/196608000000 : ℚ),(42371583829/196608000000 : ℚ),(228620840773/1474560000000 : ℚ),(9608141163/81920000000 : ℚ),(9972405283/102400000000 : ℚ)],![(881950278557/3538944000000 : ℚ),(573346512547/3538944000000 : ℚ),(2998955208149/26542080000000 : ℚ),(361927411507/4423680000000 : ℚ),(355036254557/5529600000000 : ℚ)],![(74103625189/393216000000 : ℚ),(91819247/768000000 : ℚ),(118905399329/1474560000000 : ℚ),(568507133/10240000000 : ℚ),(8307886183/204800000000 : ℚ)],![(10497636823/73728000000 : ℚ),(104855553263/1179648000000 : ℚ),(1036454406527/17694720000000 : ℚ),(28630141249/737280000000 : ℚ),(24634287449/921600000000 : ℚ)]]
64 refine ⟨⟨4,4,c,?_,?_⟩,(24634287449/921600000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(2048157664571/3686400000000 : ℚ),(126167891889/327680000000 : ℚ),(4822852560827/17694720000000 : ℚ),(25674313897/131072000000 : ℚ),(10497636823/73728000000 : ℚ)],![(718821260999/1843200000000 : ℚ),(132116784463/491520000000 : ℚ),(1671124799603/8847360000000 : ℚ),(13212521867/98304000000 : ℚ),(113613502769/1179648000000 : ℚ)],![(1448878661369/5529600000000 : ℚ),(266490324223/1474560000000 : ℚ),(3373450418723/26542080000000 : ℚ),(106777097513/1179648000000 : ℚ),(229766041769/3538944000000 : ℚ)],![(5209451/30000000 : ℚ),(752230691/6144000000 : ℚ),(90653017/1024000000 : ℚ),(80268169/1228800000 : ℚ),(60392203/1228800000 : ℚ)],![(40097167/320000000 : ℚ),(6030527/64000000 : ℚ),(37586059/512000000 : ℚ),(3021413/51200000 : ℚ),(8048951/163840000 : ℚ)]]
79 refine ⟨⟨4,4,c,?_,?_⟩,(8048951/163840000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(10497636823/73728000000 : ℚ),(104855553263/1179648000000 : ℚ),(1036454406527/17694720000000 : ℚ),(28630141249/737280000000 : ℚ),(24634287449/921600000000 : ℚ)],![(113613502769/1179648000000 : ℚ),(34338371567/589824000000 : ℚ),(323022010553/8847360000000 : ℚ),(8163884461/368640000000 : ℚ),(23766174149/1843200000000 : ℚ)],![(229766041769/3538944000000 : ℚ),(139200790999/3538944000000 : ℚ),(656492895623/26542080000000 : ℚ),(66670475659/4423680000000 : ℚ),(49007445569/5529600000000 : ℚ)],![(60392203/1228800000 : ℚ),(40516237/1228800000 : ℚ),(24399797/1024000000 : ℚ),(110875901/6144000000 : ℚ),(57221053/3840000000 : ℚ)],![(8048951/163840000 : ℚ),(16073451/409600000 : ℚ),(34682853/1024000000 : ℚ),(15926353/512000000 : ℚ),(39656363/1280000000 : ℚ)]]
94 refine ⟨⟨4,4,c,?_,?_⟩,(49007445569/5529600000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(32151938669/230400000000 : ℚ),(108754708757/921600000000 : ℚ),(330519686717/2764800000000 : ℚ),(511985127307/3686400000000 : ℚ),(721556216369/3686400000000 : ℚ)],![(9972405283/102400000000 : ℚ),(31738536449/409600000000 : ℚ),(556226106689/7372800000000 : ℚ),(424669211047/4915200000000 : ℚ),(617739423649/4915200000000 : ℚ)],![(355036254557/5529600000000 : ℚ),(1030652978921/22118400000000 : ℚ),(5646967097377/132710400000000 : ℚ),(4227503170921/88473600000000 : ℚ),(6551608908557/88473600000000 : ℚ)],![(8307886183/204800000000 : ℚ),(2622814853/102400000000 : ℚ),(153562063957/7372800000000 : ℚ),(27744466709/1228800000000 : ℚ),(391081092349/9830400000000 : ℚ)],![(24634287449/921600000000 : ℚ),(53923593347/3686400000000 : ℚ),(899370613531/88473600000000 : ℚ),(307065021119/29491200000000 : ℚ),(40768419553/1843200000000 : ℚ)]]
109 refine ⟨⟨4,4,c,?_,?_⟩,(899370613531/88473600000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(721556216369/3686400000000 : ℚ),(310375768477/1228800000000 : ℚ),(959232953903/2764800000000 : ℚ),(76573619249/153600000000 : ℚ),(21658482043/28800000000 : ℚ)],![(617739423649/4915200000000 : ℚ),(810809636251/4915200000000 : ℚ),(1714647382301/7372800000000 : ℚ),(422481711499/1228800000000 : ℚ),(164113105399/307200000000 : ℚ)],![(6551608908557/88473600000000 : ℚ),(2958571548731/29491200000000 : ℚ),(19591601523193/132710400000000 : ℚ),(1679007474269/7372800000000 : ℚ),(2037299960807/5529600000000 : ℚ)],![(391081092349/9830400000000 : ℚ),(280103225513/4915200000000 : ℚ),(165234534997/1843200000000 : ℚ),(90117888781/614400000000 : ℚ),(38330574631/153600000000 : ℚ)],![(40768419553/1843200000000 : ℚ),(110836044953/3276800000000 : ℚ),(5042126914279/88473600000000 : ℚ),(161162773869/1638400000000 : ℚ),(642848357771/3686400000000 : ℚ)]]
124 refine ⟨⟨4,4,c,?_,?_⟩,(40768419553/1843200000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(24634287449/921600000000 : ℚ),(152460743143/7372800000000 : ℚ),(5852594689291/353894400000000 : ℚ),(1644449536673/117964800000000 : ℚ),(3096574104929/235929600000000 : ℚ)],![(24344916349/1228800000000 : ℚ),(71139647809/4915200000000 : ℚ),(281252163087/26214400000000 : ℚ),(649272934699/78643200000000 : ℚ),(759936076943/104857600000000 : ℚ)],![(339410215157/22118400000000 : ℚ),(1900999830799/176947200000000 : ℚ),(31739840557019/4246732800000000 : ℚ),(14891055152789/2831155200000000 : ℚ),(24115160515997/5662310400000000 : ℚ)],![(32840108059/2457600000000 : ℚ),(373983280201/39321600000000 : ℚ),(711290081509/104857600000000 : ℚ),(3113639958811/629145600000000 : ℚ),(868630062813/209715200000000 : ℚ)],![(51164718389/3686400000000 : ℚ),(318019028923/29491200000000 : ℚ),(49015872616879/5662310400000000 : ℚ),(862765427957/117964800000000 : ℚ),(6488668836869/943718400000000 : ℚ)]]
139 refine ⟨⟨4,4,c,?_,?_⟩,(868630062813/209715200000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(3096574104929/235929600000000 : ℚ),(7563148793/614400000000 : ℚ),(4698644878789/353894400000000 : ℚ),(319786577989/19660800000000 : ℚ),(40768419553/1843200000000 : ℚ)],![(759936076943/104857600000000 : ℚ),(981262361431/157286400000000 : ℚ),(263236490647/39321600000000 : ℚ),(173161453973/19660800000000 : ℚ),(87071206833/6553600000000 : ℚ)],![(24115160515997/5662310400000000 : ℚ),(128112574489/39321600000000 : ℚ),(3684747797069/1061683200000000 : ℚ),(132512455239/26214400000000 : ℚ),(3045187168607/353894400000000 : ℚ)],![(868630062813/209715200000000 : ℚ),(2098140418067/629145600000000 : ℚ),(1118370703783/314572800000000 : ℚ),(388269056611/78643200000000 : ℚ),(52299415289/6553600000000 : ℚ)],![(6488668836869/943718400000000 : ℚ),(1012535708347/157286400000000 : ℚ),(39092962533991/5662310400000000 : ℚ),(2641044434141/314572800000000 : ℚ),(2674884700931/235929600000000 : ℚ)]]
154 refine ⟨⟨4,4,c,?_,?_⟩,(128112574489/39321600000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(51164718389/3686400000000 : ℚ),(318019028923/29491200000000 : ℚ),(49015872616879/5662310400000000 : ℚ),(862765427957/117964800000000 : ℚ),(6488668836869/943718400000000 : ℚ)],![(106138549379/7372800000000 : ℚ),(1422202390781/117964800000000 : ℚ),(3726380052017/353894400000000 : ℚ),(18267573818191/1887436800000000 : ℚ),(18137004782159/1887436800000000 : ℚ)],![(385119566369/22118400000000 : ℚ),(2801757481333/176947200000000 : ℚ),(31779232601599/2123366400000000 : ℚ),(41671016978063/2831155200000000 : ℚ),(86031165817049/5662310400000000 : ℚ)],![(88095071/3840000000 : ℚ),(2718602723/122880000000 : ℚ),(899734269/40960000000 : ℚ),(11022032927/491520000000 : ℚ),(46414714847/1966080000000 : ℚ)],![(39656363/1280000000 : ℚ),(158306413/5120000000 : ℚ),(645462153/20480000000 : ℚ),(2685164283/81920000000 : ℚ),(11412331003/327680000000 : ℚ)]]
169 refine ⟨⟨4,4,c,?_,?_⟩,(6488668836869/943718400000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(6488668836869/943718400000000 : ℚ),(1012535708347/157286400000000 : ℚ),(39092962533991/5662310400000000 : ℚ),(2641044434141/314572800000000 : ℚ),(2674884700931/235929600000000 : ℚ)],![(18137004782159/1887436800000000 : ℚ),(2000715082903/209715200000000 : ℚ),(3628453274993/353894400000000 : ℚ),(621502106973/52428800000000 : ℚ),(1733495225729/117964800000000 : ℚ)],![(86031165817049/5662310400000000 : ℚ),(821484237759/52428800000000 : ℚ),(71625860785967/4246732800000000 : ℚ),(742752786707/39321600000000 : ℚ),(7797821671769/353894400000000 : ℚ)],![(46414714847/1966080000000 : ℚ),(24370648993/983040000000 : ℚ),(4374464789/163840000000 : ℚ),(7235745523/245760000000 : ℚ),(4089539287/122880000000 : ℚ)],![(11412331003/327680000000 : ℚ),(6042002437/163840000000 : ℚ),(3253522483/81920000000 : ℚ),(1780439837/40960000000 : ℚ),(990805003/20480000000 : ℚ)]]
184 refine ⟨⟨4,4,c,?_,?_⟩,(1012535708347/157286400000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(40768419553/1843200000000 : ℚ),(110836044953/3276800000000 : ℚ),(5042126914279/88473600000000 : ℚ),(161162773869/1638400000000 : ℚ),(642848357771/3686400000000 : ℚ)],![(131346148649/29491200000000 : ℚ),(26202454673/2457600000000 : ℚ),(1076498074351/44236800000000 : ℚ),(123016766483/2457600000000 : ℚ),(182881462199/1843200000000 : ℚ)],![(300226138169/88473600000000 : ℚ),(226191754727/29491200000000 : ℚ),(2256816929731/132710400000000 : ℚ),(254278742423/7372800000000 : ℚ),(374787360569/5529600000000 : ℚ)],![(558562139/30720000000 : ℚ),(728473411/30720000000 : ℚ),(170865779/5120000000 : ℚ),(1516826881/30720000000 : ℚ),(147616639/1920000000 : ℚ)],![(990805003/20480000000 : ℚ),(297993793/5120000000 : ℚ),(186016061/2560000000 : ℚ),(59986231/640000000 : ℚ),(40097167/320000000 : ℚ)]]
199 refine ⟨⟨4,4,c,?_,?_⟩,(300226138169/88473600000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(40097167/320000000 : ℚ),(20208103/320000000 : ℚ),(26903549/640000000 : ℚ),(19987701/640000000 : ℚ),(39656363/1280000000 : ℚ)],![(27469639/960000000 : ℚ),(120356291/2560000000 : ℚ),(192207371/3840000000 : ℚ),(131353981/2560000000 : ℚ),(242465161/3840000000 : ℚ)],![(127238489369/1382400000000 : ℚ),(308124217007/2764800000000 : ℚ),(929372454559/8294400000000 : ℚ),(309389469157/2764800000000 : ℚ),(187272344969/1382400000000 : ℚ)],![(147044277629/460800000000 : ℚ),(237673101887/921600000000 : ℚ),(633554102119/2764800000000 : ℚ),(197038845187/921600000000 : ℚ),(114157413329/460800000000 : ℚ)],![(19852898683/28800000000 : ℚ),(108406813621/230400000000 : ℚ),(270414077327/691200000000 : ℚ),(161095042417/460800000000 : ℚ),(91014995789/230400000000 : ℚ)]]
214 refine ⟨⟨4,4,c,?_,?_⟩,(27469639/960000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(39656363/1280000000 : ℚ),(9834331/320000000 : ℚ),(26265471/640000000 : ℚ),(2486133/40000000 : ℚ),(40097167/320000000 : ℚ)],![(242465161/3840000000 : ℚ),(575798701/7680000000 : ℚ),(124648043/1280000000 : ℚ),(1096118839/7680000000 : ℚ),(26657233/120000000 : ℚ)],![(187272344969/1382400000000 : ℚ),(439699910719/2764800000000 : ℚ),(1711235103931/8294400000000 : ℚ),(834304581731/2764800000000 : ℚ),(658357452569/1382400000000 : ℚ)],![(114157413329/460800000000 : ℚ),(259590808129/921600000000 : ℚ),(1008865879771/2764800000000 : ℚ),(491487573371/921600000000 : ℚ),(404465368829/460800000000 : ℚ)],![(91014995789/230400000000 : ℚ),(202964940739/460800000000 : ℚ),(396023772293/691200000000 : ℚ),(193971052843/230400000000 : ℚ),(41700069133/28800000000 : ℚ)]]
229 refine ⟨⟨4,4,c,?_,?_⟩,(9834331/320000000 : ℚ),?_,?_,?_⟩
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 (nominalComparison false) (1/16) false) square :=
261 polynomial_source ▸ witness
262
263 end
264 end Komorebi.LSM.Section88ComparisonDirectPosGap
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: 9205dce806adf6115a3a2d50ce1984a6400e25b9e5c4ae1b69a3653d0dfa5553