OAI/Combinatorics/HoneycombChords/Continuation.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Fresh-row continuation of honeycomb bridges

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

  1. def OAI.CriticalHoneycomb.FiniteContinuation.row line 17

    Source documentation

    A fresh deterministic lattice row. Every two new centers advance one pure-cut spacing; this construction contributes no boundary-port weight.

    def row (i j : ℤ) : ℕ → List Center
  | 0 => []
  | n+1 => up i j::down i j::row (i+1) j n

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.up, OAI.CriticalHoneycomb.down

  2. lemma OAI.CriticalHoneycomb.FiniteContinuation.row_length line 21
  3. lemma OAI.CriticalHoneycomb.FiniteContinuation.mem_row line 26
  4. lemma OAI.CriticalHoneycomb.FiniteContinuation.row_nodup line 38
  5. lemma OAI.CriticalHoneycomb.FiniteContinuation.row_head line 45
  6. lemma OAI.CriticalHoneycomb.FiniteContinuation.row_last line 46
  7. lemma OAI.CriticalHoneycomb.FiniteContinuation.row_chain line 53
  8. def OAI.CriticalHoneycomb.FiniteContinuation.shift line 66
  9. lemma OAI.CriticalHoneycomb.FiniteContinuation.shift_injective line 67
  10. lemma OAI.CriticalHoneycomb.FiniteContinuation.shift_adj line 72
  11. lemma OAI.CriticalHoneycomb.FiniteContinuation.shift_up line 76
  12. lemma OAI.CriticalHoneycomb.FiniteContinuation.shift_down line 77
  13. lemma OAI.CriticalHoneycomb.FiniteContinuation.shift_shift line 78
  14. lemma OAI.CriticalHoneycomb.FiniteContinuation.shift_zero line 80
  15. def OAI.CriticalHoneycomb.FiniteContinuation.rect line 84

    Source documentation

    The same finite pure rectangle as the tensor grid, given by its literal integer-coordinate inequalities for the geometric continuation proof.

    def rect (W H : ℕ) : Set Center :=
…

    Mentions: OAI.CriticalHoneycomb.Center

  16. def OAI.CriticalHoneycomb.FiniteContinuation.extend line 88

    Source documentation

    The original bottom/top chord trace, with two fresh disjoint rows.

    def extend (W h : ℕ) (i x : Fin W) (p : List Center) : List Center :=
…

    Mentions: OAI.CriticalHoneycomb.Center

  17. lemma OAI.CriticalHoneycomb.FiniteContinuation.extend_length line 91
  18. lemma OAI.CriticalHoneycomb.FiniteContinuation.extend_length_le line 95
  19. lemma OAI.CriticalHoneycomb.FiniteContinuation.extend_mem line 102
  20. lemma OAI.CriticalHoneycomb.FiniteContinuation.extend_nodup line 120
  21. lemma OAI.CriticalHoneycomb.FiniteContinuation.adj_symm line 155

    Source documentation

    Symmetry is literal honeycomb adjacency, not a geometric relaxation.

    lemma adj_symm {v w : Center} (h : Adj v w) : Adj w v := by
…

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Adj

  22. lemma OAI.CriticalHoneycomb.FiniteContinuation.reverse_chain line 159
  23. def OAI.CriticalHoneycomb.FiniteContinuation.eastRun line 165

    Source documentation

    Enter from the EAST wall on the bottom fresh row, ending immediately below the original source. This direction matches the checked flux bound.

    def eastRun (W : ℕ) (i : Fin W) (j : ℤ) : List Center :=
…

    Mentions: OAI.CriticalHoneycomb.Center

  24. def OAI.CriticalHoneycomb.FiniteContinuation.westRun line 168

    Source documentation

    Leave from the original top endpoint through a new row to the WEST wall.

    def westRun (x : ℕ) (j : ℤ) : List Center :=
…

    Mentions: OAI.CriticalHoneycomb.Center

  25. lemma OAI.CriticalHoneycomb.FiniteContinuation.eastRun_length line 171
  26. lemma OAI.CriticalHoneycomb.FiniteContinuation.westRun_length line 173
  27. lemma OAI.CriticalHoneycomb.FiniteContinuation.eastRun_last line 175
  28. lemma OAI.CriticalHoneycomb.FiniteContinuation.westRun_head line 177
  29. lemma OAI.CriticalHoneycomb.FiniteContinuation.westRun_last line 179
  30. lemma OAI.CriticalHoneycomb.FiniteContinuation.eastRun_head line 184
  31. lemma OAI.CriticalHoneycomb.FiniteContinuation.eastRun_mem line 198
  32. lemma OAI.CriticalHoneycomb.FiniteContinuation.westRun_mem line 206
  33. lemma OAI.CriticalHoneycomb.FiniteContinuation.eastRun_nodup line 213
  34. lemma OAI.CriticalHoneycomb.FiniteContinuation.westRun_nodup line 218
  35. lemma OAI.CriticalHoneycomb.FiniteContinuation.eastRun_chain line 226
  36. lemma OAI.CriticalHoneycomb.FiniteContinuation.westRun_chain line 233
  37. def OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend line 245

    Source documentation

    Injective continuation along fresh rows.

    def turnedExtend (W h : ℕ) (i x : Fin W) (p : List Center) : List Center :=
…

    Mentions: OAI.CriticalHoneycomb.Center

  38. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_length line 247
  39. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_length_le line 250
  40. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_mem line 255
  41. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_nodup line 271
  42. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_chain line 301
  43. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_head line 319
  44. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_last line 322
  45. def OAI.CriticalHoneycomb.FiniteContinuation.middle line 326
  46. lemma OAI.CriticalHoneycomb.FiniteContinuation.filter_turnedExtend line 327
  47. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_injective line 350
  48. lemma OAI.CriticalHoneycomb.FiniteContinuation.turnedExtend_height line 356
  49. def OAI.CriticalHoneycomb.FiniteContinuation.RectBridge line 364

    Source documentation

    A literal bottom-to-top bridge in width W+1 and height h+1, with terminal position summed. No endpoint or length information is assumed.

    def RectBridge (W h : ℕ) (i : Fin (W+1)) :=
…
  50. def OAI.CriticalHoneycomb.FiniteContinuation.terminal line 368
  51. lemma OAI.CriticalHoneycomb.FiniteContinuation.terminal_last line 370
  52. def OAI.CriticalHoneycomb.FiniteContinuation.continuedTrace line 372
  53. lemma OAI.CriticalHoneycomb.FiniteContinuation.continuedTrace_trace line 375
  54. lemma OAI.CriticalHoneycomb.FiniteContinuation.continuedTrace_head line 389
  55. lemma OAI.CriticalHoneycomb.FiniteContinuation.continuedTrace_last line 392
  56. lemma OAI.CriticalHoneycomb.FiniteContinuation.continuedTrace_length line 395
  57. lemma OAI.CriticalHoneycomb.FiniteContinuation.continuedTrace_injective line 398
  58. lemma OAI.CriticalHoneycomb.FiniteContinuation.continuedTrace_height line 406
  59. def OAI.CriticalHoneycomb.FiniteContinuation.continuedChord line 418
  60. lemma OAI.CriticalHoneycomb.FiniteContinuation.continuedChord_injective line 433
  61. instance OAI.CriticalHoneycomb.FiniteContinuation.rectBridgeFintype line 438
  62. def OAI.CriticalHoneycomb.FiniteContinuation.continues line 443
  63. lemma OAI.CriticalHoneycomb.FiniteContinuation.continues_injective line 449
  64. lemma OAI.CriticalHoneycomb.FiniteContinuation.kappa_positive line 460
  65. lemma OAI.CriticalHoneycomb.FiniteContinuation.kappa_at_most_one line 462
  66. lemma OAI.CriticalHoneycomb.FiniteContinuation.continued_weight line 468
  67. def OAI.CriticalHoneycomb.FiniteContinuation.crossingMass line 479
  68. lemma OAI.CriticalHoneycomb.FiniteContinuation.crossingMass_nonnegative line 482
  69. theorem OAI.CriticalHoneycomb.FiniteContinuation.crossing_partial_sum line 490

    Source documentation

    Literal finite-height mass bound, using the injective fresh-row continuation and the already proved finite honeycomb Ward identity.

    theorem crossing_partial_sum (W N : ℕ) (i : Fin (W+1)) :
    kappa^(4*(W+1))*(∑ h : Fin (N+1),crossingMass W h.val i)≤1 := by
…

    Mentions: OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.FiniteContinuation.crossingMass

  70. theorem OAI.CriticalHoneycomb.FiniteContinuation.crossing_summable line 521

    Source documentation

    The actual fixed-width tall-crossing masses are summable. This is stronger than the qualitative decay needed for the physical transfer gap, and is a dependency only, not any of the manuscript's main theorems.

    theorem crossing_summable (W : ℕ) (i : Fin (W+1)) :
    Summable (fun h : ℕ => crossingMass W h i) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteContinuation.crossingMass

  71. theorem OAI.CriticalHoneycomb.FiniteContinuation.crossing_tendsto_zero line 535

    Source documentation

    Uniform over the finitely many terminal sites, with the original literal center weights and no assumed path estimates.

    theorem crossing_tendsto_zero (W : ℕ) (i : Fin (W+1)) :
    Filter.Tendsto (fun h : ℕ => crossingMass W h i) Filter.atTop (nhds 0) :=
…

    Mentions: OAI.CriticalHoneycomb.FiniteContinuation.crossingMass