Large Signal Model · Lean source
Section88ComparisonRotatedPosGap.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/Section88ComparisonRotatedPosGap.lean215 lines
Original source path
Lean/KomorebiLSM/Section88ComparisonRotatedPosGap.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.Section88ComparisonRotatedPosGap
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 (359387/160000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^0 +
16 MvPolynomial.C (9985843/30000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^1 +
17 MvPolynomial.C (57325581089/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 (-142919/80000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^4 +
21 MvPolynomial.C (159408487/480000000 : ℚ)*MvPolynomial.X 0^1*MvPolynomial.X 1^3 +
22 MvPolynomial.C (57978084689/230400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^4 +
23 MvPolynomial.C (80127887/38400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^1 +
24 MvPolynomial.C (-5561353/960000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^0 +
25 MvPolynomial.C (131571713/38400000000 : ℚ)*MvPolynomial.X 0^2*MvPolynomial.X 1^3 +
26 MvPolynomial.C (1597547/960000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^4 +
27 MvPolynomial.C (17323607/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^1 +
28 MvPolynomial.C (41128493/1920000000 : ℚ)*MvPolynomial.X 0^3*MvPolynomial.X 1^3 +
29 MvPolynomial.C (38563/4000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^0 +
30 MvPolynomial.C (695359/1024000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^2 +
31 MvPolynomial.C (-97069/12800000 : ℚ)*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 (3283/6400000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^1 +
37 MvPolynomial.C (-66591/128000000 : ℚ)*MvPolynomial.X 0^4*MvPolynomial.X 1^3
38
39 theorem polynomial_source : polynomial=squareGapPolynomial (nominalComparison true) (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_0 : Rectangle := (square.quarter false false)
47 def leaf_0 : RecordedLeaf polynomial cell_0 := by
48 let c : Fin 5 → Fin 5 → ℚ := ![![(52455119593/28800000000 : ℚ),(211088168341/230400000000 : ℚ),(384402283967/691200000000 : ℚ),(174098915257/460800000000 : ℚ),(67572722669/230400000000 : ℚ)],![(521965112309/460800000000 : ℚ),(519821152127/921600000000 : ℚ),(920467762999/2764800000000 : ℚ),(200801724727/921600000000 : ℚ),(71634078209/460800000000 : ℚ)],![(864951494489/1382400000000 : ℚ),(860343479567/2764800000000 : ℚ),(1483284169279/8294400000000 : ℚ),(312054414517/2764800000000 : ℚ),(99025261289/1382400000000 : ℚ)],![(140125619/480000000 : ℚ),(1113095071/7680000000 : ℚ),(158012921/1920000000 : ℚ),(49193657/960000000 : ℚ),(39329589/1280000000 : ℚ)],![(40293167/320000000 : ℚ),(19963103/320000000 : ℚ),(26413549/640000000 : ℚ),(19840701/640000000 : ℚ),(40048363/1280000000 : ℚ)]]
49 refine ⟨⟨4,4,c,?_,?_⟩,(39329589/1280000000 : ℚ),?_,?_,?_⟩
50 · decide +kernel
51 · apply MvPolynomial.funext
52 intro x
53 norm_num [Rectangle.localPolynomial,cell_0,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_10 : Rectangle := ((square.quarter false true).quarter false false)
62 def leaf_10 : RecordedLeaf polynomial cell_10 := by
63 let c : Fin 5 → Fin 5 → ℚ := ![![(67572722669/230400000000 : ℚ),(231337420757/921600000000 : ℚ),(641975558717/2764800000000 : ℚ),(832493679307/3686400000000 : ℚ),(877873160369/3686400000000 : ℚ)],![(68926507849/307200000000 : ℚ),(230559195347/1228800000000 : ℚ),(1247393058689/7372800000000 : ℚ),(261462572349/1638400000000 : ℚ),(266895731883/1638400000000 : ℚ)],![(934266066557/5529600000000 : ℚ),(3044138144921/22118400000000 : ℚ),(15963037169377/132710400000000 : ℚ),(9635420776921/88473600000000 : ℚ),(9367686480557/88473600000000 : ℚ)],![(77205265549/614400000000 : ℚ),(61229426243/614400000000 : ℚ),(620536774957/7372800000000 : ℚ),(59436537681/819200000000 : ℚ),(216379959783/3276800000000 : ℚ)],![(86348037449/921600000000 : ℚ),(268964748347/3686400000000 : ℚ),(5319440533531/88473600000000 : ℚ),(1471626531119/29491200000000 : ℚ),(79085938303/1843200000000 : ℚ)]]
64 refine ⟨⟨4,4,c,?_,?_⟩,(79085938303/1843200000000 : ℚ),?_,?_,?_⟩
65 · decide +kernel
66 · apply MvPolynomial.funext
67 intro x
68 norm_num [Rectangle.localPolynomial,cell_10,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_11 : Rectangle := ((square.quarter false true).quarter false true)
77 def leaf_11 : RecordedLeaf polynomial cell_11 := by
78 let c : Fin 5 → Fin 5 → ℚ := ![![(877873160369/3686400000000 : ℚ),(307750880477/1228800000000 : ℚ),(778114001903/2764800000000 : ℚ),(51813163249/153600000000 : ℚ),(12716850043/28800000000 : ℚ)],![(266895731883/1638400000000 : ℚ),(272328891417/1638400000000 : ℚ),(1345189930301/7372800000000 : ℚ),(88348367833/409600000000 : ℚ),(87112937399/307200000000 : ℚ)],![(9367686480557/88473600000000 : ℚ),(3033317394731/29491200000000 : ℚ),(14356631391193/132710400000000 : ℚ),(916003218269/7372800000000 : ℚ),(905871872807/5529600000000 : ℚ)],![(216379959783/3276800000000 : ℚ),(97506884421/1638400000000 : ℚ),(53530132061/921600000000 : ℚ),(12893353927/204800000000 : ℚ),(12776595131/153600000000 : ℚ)],![(79085938303/1843200000000 : ℚ),(353041164859/9830400000000 : ℚ),(2844422314279/88473600000000 : ℚ),(158440801607/4915200000000 : ℚ),(157358597771/3686400000000 : ℚ)]]
79 refine ⟨⟨4,4,c,?_,?_⟩,(2844422314279/88473600000000 : ℚ),?_,?_,?_⟩
80 · decide +kernel
81 · apply MvPolynomial.funext
82 intro x
83 norm_num [Rectangle.localPolynomial,cell_11,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_12 : Rectangle := ((square.quarter false true).quarter true false)
92 def leaf_12 : RecordedLeaf polynomial cell_12 := by
93 let c : Fin 5 → Fin 5 → ℚ := ![![(86348037449/921600000000 : ℚ),(268964748347/3686400000000 : ℚ),(5319440533531/88473600000000 : ℚ),(1471626531119/29491200000000 : ℚ),(79085938303/1843200000000 : ℚ)],![(113776353149/1843200000000 : ℚ),(42638234809/921600000000 : ℚ),(1596219883789/44236800000000 : ℚ),(401768852861/14745600000000 : ℚ),(583330387649/29491200000000 : ℚ)],![(227229405569/5529600000000 : ℚ),(682254726257/22118400000000 : ℚ),(3201032573659/132710400000000 : ℚ),(1618354872157/88473600000000 : ℚ),(1183150978169/88473600000000 : ℚ)],![(2480561/80000000 : ℚ),(199291367/7680000000 : ℚ),(180699709/7680000000 : ℚ),(2753930093/122880000000 : ℚ),(1427529653/61440000000 : ℚ)],![(40048363/1280000000 : ℚ),(80463687/2560000000 : ℚ),(175173953/5120000000 : ℚ),(405499417/10240000000 : ℚ),(1013933003/20480000000 : ℚ)]]
94 refine ⟨⟨4,4,c,?_,?_⟩,(1183150978169/88473600000000 : ℚ),?_,?_,?_⟩
95 · decide +kernel
96 · apply MvPolynomial.funext
97 intro x
98 norm_num [Rectangle.localPolynomial,cell_12,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_13 : Rectangle := ((square.quarter false true).quarter true true)
107 def leaf_13 : RecordedLeaf polynomial cell_13 := by
108 let c : Fin 5 → Fin 5 → ℚ := ![![(79085938303/1843200000000 : ℚ),(353041164859/9830400000000 : ℚ),(2844422314279/88473600000000 : ℚ),(158440801607/4915200000000 : ℚ),(157358597771/3686400000000 : ℚ)],![(583330387649/29491200000000 : ℚ),(15130127899/1228800000000 : ℚ),(274975975351/44236800000000 : ℚ),(3720554483/2457600000000 : ℚ),(4039456199/1843200000000 : ℚ)],![(1183150978169/88473600000000 : ℚ),(249315694727/29491200000000 : ℚ),(589809209731/132710400000000 : ℚ),(10005062423/7372800000000 : ℚ),(10193760569/5529600000000 : ℚ)],![(1427529653/61440000000 : ℚ),(985396173/40960000000 : ℚ),(274642683/10240000000 : ℚ),(329318627/10240000000 : ℚ),(20487191/480000000 : ℚ)],![(1013933003/20480000000 : ℚ),(304216793/5120000000 : ℚ),(189054061/2560000000 : ℚ),(60623231/640000000 : ℚ),(40293167/320000000 : ℚ)]]
109 refine ⟨⟨4,4,c,?_,?_⟩,(10005062423/7372800000000 : ℚ),?_,?_,?_⟩
110 · decide +kernel
111 · apply MvPolynomial.funext
112 intro x
113 norm_num [Rectangle.localPolynomial,cell_13,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_20 : Rectangle := ((square.quarter true false).quarter false false)
122 def leaf_20 : RecordedLeaf polynomial cell_20 := by
123 let c : Fin 5 → Fin 5 → ℚ := ![![(40293167/320000000 : ℚ),(6025627/64000000 : ℚ),(37370459/512000000 : ℚ),(2994463/51200000 : ℚ),(7970551/163840000 : ℚ)],![(16477453/384000000 : ℚ),(65556431/2048000000 : ℚ),(54214363/2048000000 : ℚ),(7757513/327680000 : ℚ),(56368649/2457600000 : ℚ)],![(10179131129/5529600000000 : ℚ),(1916485183/1474560000000 : ℚ),(115974898403/26542080000000 : ℚ),(9965138633/1179648000000 : ℚ),(47826053609/3538944000000 : ℚ)],![(3715829819/1843200000000 : ℚ),(732515503/491520000000 : ℚ),(55398156443/8847360000000 : ℚ),(2448622909/196608000000 : ℚ),(23682792809/1179648000000 : ℚ)],![(158199143771/3686400000000 : ℚ),(31891953427/983040000000 : ℚ),(570173251067/17694720000000 : ℚ),(14112102931/393216000000 : ℚ),(3162072013/73728000000 : ℚ)]]
124 refine ⟨⟨4,4,c,?_,?_⟩,(1916485183/1474560000000 : ℚ),?_,?_,?_⟩
125 · decide +kernel
126 · apply MvPolynomial.funext
127 intro x
128 norm_num [Rectangle.localPolynomial,cell_20,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_21 : Rectangle := ((square.quarter true false).quarter false true)
137 def leaf_21 : RecordedLeaf polynomial cell_21 := by
138 let c : Fin 5 → Fin 5 → ℚ := ![![(7970551/163840000 : ℚ),(15897051/409600000 : ℚ),(34447653/1024000000 : ℚ),(15945953/512000000 : ℚ),(40048363/1280000000 : ℚ)],![(56368649/2457600000 : ℚ),(109111901/4915200000 : ℚ),(18064513/768000000 : ℚ),(40280449/1536000000 : ℚ),(161631/5120000 : ℚ)],![(47826053609/3538944000000 : ℚ),(65756691319/3538944000000 : ℚ),(653894029703/26542080000000 : ℚ),(140054740459/4423680000000 : ℚ),(233439612929/5529600000000 : ℚ)],![(23682792809/1179648000000 : ℚ),(8168462041/294912000000 : ℚ),(325129817093/8847360000000 : ℚ),(34826238107/737280000000 : ℚ),(116214094469/1843200000000 : ℚ)],![(3162072013/73728000000 : ℚ),(58849995623/1179648000000 : ℚ),(1065583855967/17694720000000 : ℚ),(54067792789/737280000000 : ℚ),(87083381849/921600000000 : ℚ)]]
139 refine ⟨⟨4,4,c,?_,?_⟩,(47826053609/3538944000000 : ℚ),?_,?_,?_⟩
140 · decide +kernel
141 · apply MvPolynomial.funext
142 intro x
143 norm_num [Rectangle.localPolynomial,cell_21,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_22 : Rectangle := ((square.quarter true false).quarter true false)
152 def leaf_22 : RecordedLeaf polynomial cell_22 := by
153 let c : Fin 5 → Fin 5 → ℚ := ![![(158199143771/3686400000000 : ℚ),(31891953427/983040000000 : ℚ),(570173251067/17694720000000 : ℚ),(14112102931/393216000000 : ℚ),(3162072013/73728000000 : ℚ)],![(1609201187/19200000000 : ℚ),(2596619827/40960000000 : ℚ),(1787413523/30720000000 : ℚ),(1943913337/32768000000 : ℚ),(25834503869/393216000000 : ℚ)],![(914784035927/5529600000000 : ℚ),(184478019709/1474560000000 : ℚ),(2872236527489/26542080000000 : ℚ),(120543423989/1179648000000 : ℚ),(370750366397/3538944000000 : ℚ)],![(88245517519/307200000000 : ℚ),(17812842433/81920000000 : ℚ),(89647715311/491520000000 : ℚ),(10791855883/65536000000 : ℚ),(31524476609/196608000000 : ℚ)],![(12929282683/28800000000 : ℚ),(10464717539/30720000000 : ℚ),(155534833489/552960000000 : ℚ),(12166030103/49152000000 : ℚ),(34397731169/147456000000 : ℚ)]]
154 refine ⟨⟨4,4,c,?_,?_⟩,(570173251067/17694720000000 : ℚ),?_,?_,?_⟩
155 · decide +kernel
156 · apply MvPolynomial.funext
157 intro x
158 norm_num [Rectangle.localPolynomial,cell_22,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_23 : Rectangle := ((square.quarter true false).quarter true true)
167 def leaf_23 : RecordedLeaf polynomial cell_23 := by
168 let c : Fin 5 → Fin 5 → ℚ := ![![(3162072013/73728000000 : ℚ),(58849995623/1179648000000 : ℚ),(1065583855967/17694720000000 : ℚ),(54067792789/737280000000 : ℚ),(87083381849/921600000000 : ℚ)],![(25834503869/393216000000 : ℚ),(14171023847/196608000000 : ℚ),(13712111831/163840000000 : ℚ),(24436449157/245760000000 : ℚ),(25791048103/204800000000 : ℚ)],![(370750366397/3538944000000 : ℚ),(379870460827/3538944000000 : ℚ),(3145839360389/26542080000000 : ℚ),(601852052827/4423680000000 : ℚ),(928871643677/5529600000000 : ℚ)],![(31524476609/196608000000 : ℚ),(30673385569/196608000000 : ℚ),(27045601637/163840000000 : ℚ),(45115869989/245760000000 : ℚ),(22636502323/102400000000 : ℚ)],![(34397731169/147456000000 : ℚ),(32297372029/147456000000 : ℚ),(124029446389/552960000000 : ℚ),(44787318799/184320000000 : ℚ),(65938307789/230400000000 : ℚ)]]
169 refine ⟨⟨4,4,c,?_,?_⟩,(3162072013/73728000000 : ℚ),?_,?_,?_⟩
170 · decide +kernel
171 · apply MvPolynomial.funext
172 intro x
173 norm_num [Rectangle.localPolynomial,cell_23,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_3 : Rectangle := (square.quarter true true)
182 def leaf_3 : RecordedLeaf polynomial cell_3 := by
183 let c : Fin 5 → Fin 5 → ℚ := ![![(40048363/1280000000 : ℚ),(10103831/320000000 : ℚ),(27147471/640000000 : ℚ),(1270629/20000000 : ℚ),(40293167/320000000 : ℚ)],![(40767137/1280000000 : ℚ),(101644519/1920000000 : ℚ),(162443627/1920000000 : ℚ),(1131398839/7680000000 : ℚ),(280689739/960000000 : ℚ)],![(102130364969/1382400000000 : ℚ),(320330660719/2764800000000 : ℚ),(1514938443931/8294400000000 : ℚ),(872583381731/2764800000000 : ℚ),(868754772569/1382400000000 : ℚ)],![(71851905329/460800000000 : ℚ),(202246570129/921600000000 : ℚ),(931002667771/2764800000000 : ℚ),(526718181371/921600000000 : ℚ),(527044720829/460800000000 : ℚ)],![(65938307789/230400000000 : ℚ),(171693252739/460800000000 : ℚ),(385052196293/691200000000 : ℚ),(213914836843/230400000000 : ℚ),(53301813133/28800000000 : ℚ)]]
184 refine ⟨⟨4,4,c,?_,?_⟩,(40048363/1280000000 : ℚ),?_,?_,?_⟩
185 · decide +kernel
186 · apply MvPolynomial.funext
187 intro x
188 norm_num [Rectangle.localPolynomial,cell_3,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 => .leaf leaf_0.certificate
199 | false,true => .of_quarters (fun
200 | false,false => .leaf leaf_10.certificate
201 | false,true => .leaf leaf_11.certificate
202 | true,false => .leaf leaf_12.certificate
203 | true,true => .leaf leaf_13.certificate)
204 | true,false => .of_quarters (fun
205 | false,false => .leaf leaf_20.certificate
206 | false,true => .leaf leaf_21.certificate
207 | true,false => .leaf leaf_22.certificate
208 | true,true => .leaf leaf_23.certificate)
209 | true,true => .leaf leaf_3.certificate)
210
211 def certifiedWitness : SubdivisionWitness (squareGapPolynomial (nominalComparison true) (1/16) false) square :=
212 polynomial_source ▸ witness
213
214 end
215 end Komorebi.LSM.Section88ComparisonRotatedPosGap
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: d576ac7bfe5c36e48241bd09e6dc5717f285ce26acdad68d8153a02918ab89c0