Large Signal Model · Lean source
Section88ComparisonRotatedNegGap.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/Section88ComparisonRotatedNegGap.lean215 lines
Original source path
Lean/KomorebiLSM/Section88ComparisonRotatedNegGap.leanSkip declarations and read code
1 import KomorebiLSM.PerturbedOperatorFixture
2 import KomorebiLSM.RecordedBernsteinFixture
3
4 /-! Exact rational replay of robust_comparison_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.Section88ComparisonRotatedNegGap
9 open TensorBernsteinCertificate RationalBernsteinMargin RationalLorentzMatrix
10 open PerturbedOperatorFixture RecordedBernsteinFixture
11 noncomputable section
12
13 def polynomial : Polynomial₂ := MvPolynomial.C (40048363/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 (-142919/80000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (-159408487/480000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
17 MvPolynomial.C (57978084689/230400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^0 +
18 MvPolynomial.C (117860942311/230400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^2 +
19 MvPolynomial.C (40048363/1280000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^4 +
20 MvPolynomial.C (359387/160000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^4 +
21 MvPolynomial.C (-9985843/30000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^3 +
22 MvPolynomial.C (57325581089/230400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^4 +
23 MvPolynomial.C (-131571713/38400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^1 +
24 MvPolynomial.C (1597547/960000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^0 +
25 MvPolynomial.C (-80127887/38400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^3 +
26 MvPolynomial.C (-5561353/960000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^4 +
27 MvPolynomial.C (-41128493/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^1 +
28 MvPolynomial.C (-17323607/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^3 +
29 MvPolynomial.C (-97069/12800000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^0 +
30 MvPolynomial.C (695359/1024000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^2 +
31 MvPolynomial.C (38563/4000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^4 +
32 MvPolynomial.C (366961/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 (-366961/320000000 : ℚ)*MvPolynomial.X 0^0*MvPolynomial.X 1^3 +
35 MvPolynomial.C (23825711/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^2 +
36 MvPolynomial.C (66591/128000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^1 +
37 MvPolynomial.C (-3283/6400000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^3
38
39 theorem polynomial_source : polynomial=squareGapPolynomial (nominalComparison 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 → ℚ := ![![(12716850043/28800000000 : ℚ),(9984327419/30720000000 : ℚ),(145408559149/552960000000 : ℚ),(11271708563/49152000000 : ℚ),(31898531249/147456000000 : ℚ)],![(87112937399/307200000000 : ℚ),(17175501393/81920000000 : ℚ),(255695337373/1474560000000 : ℚ),(10219519223/65536000000 : ℚ),(9989184843/65536000000 : ℚ)],![(905871872807/5529600000000 : ℚ),(179148105469/1474560000000 : ℚ),(2761907747249/26542080000000 : ℚ),(115876832549/1179648000000 : ℚ),(358430249357/3538944000000 : ℚ)],![(12776595131/153600000000 : ℚ),(2531967267/40960000000 : ℚ),(10390777663/184320000000 : ℚ),(3778019389/65536000000 : ℚ),(8426060463/131072000000 : ℚ)],![(157358597771/3686400000000 : ℚ),(31255278787/983040000000 : ℚ),(557196661427/17694720000000 : ℚ),(13857862021/393216000000 : ℚ),(390578981/9216000000 : ℚ)]]
49 refine ⟨⟨4,4,c,?_,?_⟩,(557196661427/17694720000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(31898531249/147456000000 : ℚ),(29981936809/147456000000 : ℚ),(116659642549/552960000000 : ℚ),(42669580939/184320000000 : ℚ),(63467743469/230400000000 : ℚ)],![(9989184843/65536000000 : ℚ),(9758850463/65536000000 : ℚ),(234965243173/1474560000000 : ℚ),(43966013449/245760000000 : ℚ),(66585562249/307200000000 : ℚ)],![(358430249357/3538944000000 : ℚ),(369230001067/3538944000000 : ℚ),(3085900298549/26542080000000 : ℚ),(594308459707/4423680000000 : ℚ),(920198796557/5529600000000 : ℚ)],![(8426060463/131072000000 : ℚ),(2324020537/32768000000 : ℚ),(122277197129/1474560000000 : ℚ),(12157226071/122880000000 : ℚ),(77081239549/614400000000 : ℚ)],![(390578981/9216000000 : ℚ),(58414633073/1179648000000 : ℚ),(1062428071727/17694720000000 : ℚ),(27013179317/368640000000 : ℚ),(87007603349/921600000000 : ℚ)]]
64 refine ⟨⟨4,4,c,?_,?_⟩,(390578981/9216000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(157358597771/3686400000000 : ℚ),(31255278787/983040000000 : ℚ),(557196661427/17694720000000 : ℚ),(13857862021/393216000000 : ℚ),(390578981/9216000000 : ℚ)],![(4039456199/1843200000000 : ℚ),(871671583/491520000000 : ℚ),(58439333603/8847360000000 : ℚ),(1261901927/98304000000 : ℚ),(24153674969/1179648000000 : ℚ)],![(10193760569/5529600000000 : ℚ),(2076491743/1474560000000 : ℚ),(119999781923/26542080000000 : ℚ),(10153780793/1179648000000 : ℚ),(48345034169/3538944000000 : ℚ)],![(20487191/480000000 : ℚ),(65254297/2048000000 : ℚ),(27007197/1024000000 : ℚ),(4834401/204800000 : ℚ),(3514781/153600000 : ℚ)],![(40293167/320000000 : ℚ),(6025627/64000000 : ℚ),(37370459/512000000 : ℚ),(2994463/51200000 : ℚ),(7970551/163840000 : ℚ)]]
79 refine ⟨⟨4,4,c,?_,?_⟩,(2076491743/1474560000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(390578981/9216000000 : ℚ),(58414633073/1179648000000 : ℚ),(1062428071727/17694720000000 : ℚ),(27013179317/368640000000 : ℚ),(87007603349/921600000000 : ℚ)],![(24153674969/1179648000000 : ℚ),(16582263407/589824000000 : ℚ),(328764888953/8847360000000 : ℚ),(17554680421/368640000000 : ℚ),(116786694749/1843200000000 : ℚ)],![(48345034169/3538944000000 : ℚ),(66228725959/3538944000000 : ℚ),(656510535623/26542080000000 : ℚ),(140300512699/4423680000000 : ℚ),(233456653169/5529600000000 : ℚ)],![(3514781/153600000 : ℚ),(2723009/122880000 : ℚ),(72140011/3072000000 : ℚ),(160841761/6144000000 : ℚ),(40334201/1280000000 : ℚ)],![(7970551/163840000 : ℚ),(15897051/409600000 : ℚ),(34447653/1024000000 : ℚ),(15945953/512000000 : ℚ),(40048363/1280000000 : ℚ)]]
94 refine ⟨⟨4,4,c,?_,?_⟩,(48345034169/3538944000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(63467743469/230400000000 : ℚ),(167458556119/460800000000 : ℚ),(376796144153/691200000000 : ℚ),(208552788403/230400000000 : ℚ),(52455119593/28800000000 : ℚ)],![(72821199809/460800000000 : ℚ),(204132806509/921600000000 : ℚ),(933331524091/2764800000000 : ℚ),(524109072491/921600000000 : ℚ),(521965112309/460800000000 : ℚ)],![(102465136889/1382400000000 : ℚ),(320102305039/2764800000000 : ℚ),(1510932258811/8294400000000 : ℚ),(869559509411/2764800000000 : ℚ),(864951494489/1382400000000 : ℚ)],![(40620039/1280000000 : ℚ),(405330487/7680000000 : ℚ),(323935723/3840000000 : ℚ),(1128914833/7680000000 : ℚ),(140125619/480000000 : ℚ)],![(40048363/1280000000 : ℚ),(10103831/320000000 : ℚ),(27147471/640000000 : ℚ),(1270629/20000000 : ℚ),(40293167/320000000 : ℚ)]]
109 refine ⟨⟨4,4,c,?_,?_⟩,(40048363/1280000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(40293167/320000000 : ℚ),(19963103/320000000 : ℚ),(26413549/640000000 : ℚ),(19840701/640000000 : ℚ),(40048363/1280000000 : ℚ)],![(280689739/960000000 : ℚ),(1114119073/7680000000 : ℚ),(316247371/3840000000 : ℚ),(394066843/7680000000 : ℚ),(39476687/1280000000 : ℚ)],![(868754772569/1382400000000 : ℚ),(864926163407/2764800000000 : ℚ),(1491966788959/8294400000000 : ℚ),(314367183157/2764800000000 : ℚ),(99995496569/1382400000000 : ℚ)],![(527044720829/460800000000 : ℚ),(527371260287/921600000000 : ℚ),(932961904519/2764800000000 : ℚ),(202690995187/921600000000 : ℚ),(71969790929/460800000000 : ℚ)],![(53301813133/28800000000 : ℚ),(212499668221/230400000000 : ℚ),(380806690427/691200000000 : ℚ),(167751128917/460800000000 : ℚ),(63411352589/230400000000 : ℚ)]]
124 refine ⟨⟨4,4,c,?_,?_⟩,(39476687/1280000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(40048363/1280000000 : ℚ),(80463687/2560000000 : ℚ),(175173953/5120000000 : ℚ),(405499417/10240000000 : ℚ),(1013933003/20480000000 : ℚ)],![(1590501/51200000 : ℚ),(159859129/6144000000 : ℚ),(2901757/122880000 : ℚ),(17292179/768000000 : ℚ),(143521349/6144000000 : ℚ)],![(228517372529/5529600000000 : ℚ),(687297096737/22118400000000 : ℚ),(3231884651419/132710400000000 : ℚ),(1638997353037/88473600000000 : ℚ),(1202366006729/88473600000000 : ℚ)],![(114508760069/1843200000000 : ℚ),(171653067391/3686400000000 : ℚ),(1607102155609/44236800000000 : ℚ),(202519214533/7372800000000 : ℚ),(588870899969/29491200000000 : ℚ)],![(85744587749/921600000000 : ℚ),(132688557061/1843200000000 : ℚ),(5218274721931/88473600000000 : ℚ),(1437061664069/29491200000000 : ℚ),(77131551253/1843200000000 : ℚ)]]
139 refine ⟨⟨4,4,c,?_,?_⟩,(1202366006729/88473600000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(1013933003/20480000000 : ℚ),(304216793/5120000000 : ℚ),(189054061/2560000000 : ℚ),(60623231/640000000 : ℚ),(40293167/320000000 : ℚ)],![(143521349/6144000000 : ℚ),(24784211/1024000000 : ℚ),(27637253/1024000000 : ℚ),(66263193/2048000000 : ℚ),(16477453/384000000 : ℚ)],![(1202366006729/88473600000000 : ℚ),(255244886807/29491200000000 : ℚ),(612096573571/132710400000000 : ℚ),(10775836343/7372800000000 : ℚ),(10179131129/5529600000000 : ℚ)],![(588870899969/29491200000000 : ℚ),(61277490301/4915200000000 : ℚ),(279866406631/44236800000000 : ℚ),(3769082123/2457600000000 : ℚ),(3715829819/1843200000000 : ℚ)],![(77131551253/1843200000000 : ℚ),(343715992009/9830400000000 : ℚ),(2782792593679/88473600000000 : ℚ),(156938520407/4915200000000 : ℚ),(158199143771/3686400000000 : ℚ)]]
154 refine ⟨⟨4,4,c,?_,?_⟩,(10775836343/7372800000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(85744587749/921600000000 : ℚ),(132688557061/1843200000000 : ℚ),(5218274721931/88473600000000 : ℚ),(1437061664069/29491200000000 : ℚ),(77131551253/1843200000000 : ℚ)],![(25385510103/204800000000 : ℚ),(119700386951/1228800000000 : ℚ),(66873566043/819200000000 : ℚ),(344007745001/4915200000000 : ℚ),(626446246709/9830400000000 : ℚ)],![(912282357677/5529600000000 : ℚ),(2936674218281/22118400000000 : ℚ),(15256307115697/132710400000000 : ℚ),(9162815024281/88473600000000 : ℚ),(8945173047677/88473600000000 : ℚ)],![(22088055123/102400000000 : ℚ),(218187241207/1228800000000 : ℚ),(129759440801/819200000000 : ℚ),(731591007907/4915200000000 : ℚ),(753702883169/4915200000000 : ℚ)],![(63411352589/230400000000 : ℚ),(212716986617/921600000000 : ℚ),(583153050077/2764800000000 : ℚ),(754773365167/3686400000000 : ℚ),(808697512289/3686400000000 : ℚ)]]
169 refine ⟨⟨4,4,c,?_,?_⟩,(77131551253/1843200000000 : ℚ),?_,?_,?_⟩
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 → ℚ := ![![(77131551253/1843200000000 : ℚ),(343715992009/9830400000000 : ℚ),(2782792593679/88473600000000 : ℚ),(156938520407/4915200000000 : ℚ),(158199143771/3686400000000 : ℚ)],![(626446246709/9830400000000 : ℚ),(23536541809/409600000000 : ℚ),(34762863709/614400000000 : ℚ),(12764119857/204800000000 : ℚ),(1609201187/19200000000 : ℚ)],![(8945173047677/88473600000000 : ℚ),(2909177023691/29491200000000 : ℚ),(13950455256073/132710400000000 : ℚ),(907177973309/7372800000000 : ℚ),(914784035927/5529600000000 : ℚ)],![(753702883169/4915200000000 : ℚ),(258604919477/1638400000000 : ℚ),(433502072927/2457600000000 : ℚ),(87426822873/409600000000 : ℚ),(88245517519/307200000000 : ℚ)],![(808697512289/3686400000000 : ℚ),(287540553137/1228800000000 : ℚ),(744925491443/2764800000000 : ℚ),(51110673769/153600000000 : ℚ),(12929282683/28800000000 : ℚ)]]
184 refine ⟨⟨4,4,c,?_,?_⟩,(2782792593679/88473600000000 : ℚ),?_,?_,?_⟩
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 (nominalComparison true) (1/16) true) square :=
212 polynomial_source ▸ witness
213
214 end
215 end Komorebi.LSM.Section88ComparisonRotatedNegGap
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: c7d6dacb4f83bf74b98461d0f4d2ef0c04dbbbf3a2c1dc8cf16e41c6b651f1b1