OAI/Combinatorics/HoneycombChords/PhysicalWeights.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb tile weights

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

  1. def OAI.CriticalHoneycombTransfer.L line 13
  2. def OAI.CriticalHoneycombTransfer.S line 14
  3. def OAI.CriticalHoneycombTransfer.b line 15
  4. def OAI.CriticalHoneycombTransfer.Q line 16
  5. def OAI.CriticalHoneycombTransfer.a line 17
  6. def OAI.CriticalHoneycombTransfer.h line 18
  7. def OAI.CriticalHoneycombTransfer.v line 19
  8. def OAI.CriticalHoneycombTransfer.c line 20
  9. def OAI.CriticalHoneycombTransfer.d line 21
  10. def OAI.CriticalHoneycombTransfer.κ line 22
  11. theorem OAI.CriticalHoneycombTransfer.κ_eq_inv_sqrt line 24
  12. theorem OAI.CriticalHoneycombTransfer.L_pos line 27
  13. theorem OAI.CriticalHoneycombTransfer.L_lt_pi_div_two line 28
  14. theorem OAI.CriticalHoneycombTransfer.cos_L_pos line 29
  15. theorem OAI.CriticalHoneycombTransfer.sin_two_L line 31
  16. theorem OAI.CriticalHoneycombTransfer.cos_two_L line 36
  17. theorem OAI.CriticalHoneycombTransfer.sin_three_L line 41
  18. theorem OAI.CriticalHoneycombTransfer.sin_four_L line 44
  19. theorem OAI.CriticalHoneycombTransfer.four_cos_sq line 47
  20. theorem OAI.CriticalHoneycombTransfer.κ_cos line 51
  21. theorem OAI.CriticalHoneycombTransfer.physical_weights line 57
  22. def OAI.CriticalHoneycomb.Transfer.Planar.angle line 102
  23. def OAI.CriticalHoneycomb.Transfer.Planar.bigAngle line 103
  24. def OAI.CriticalHoneycomb.Transfer.Planar.sine2 line 104
  25. def OAI.CriticalHoneycomb.Transfer.Planar.denominator line 105
  26. def OAI.CriticalHoneycomb.Transfer.Planar.a line 108
  27. def OAI.CriticalHoneycomb.Transfer.Planar.h line 110
  28. def OAI.CriticalHoneycomb.Transfer.Planar.v line 112
  29. def OAI.CriticalHoneycomb.Transfer.Planar.c line 114
  30. def OAI.CriticalHoneycomb.Transfer.Planar.d line 116
  31. def OAI.CriticalHoneycomb.Transfer.Planar.phase line 119
  32. lemma OAI.CriticalHoneycomb.Transfer.Planar.phase_sq line 121
  33. lemma OAI.CriticalHoneycomb.Transfer.Planar.phase_ne_zero line 130
  34. lemma OAI.CriticalHoneycomb.Transfer.Planar.phase_inv line 132
  35. def OAI.CriticalHoneycomb.Transfer.Planar.sourceR line 144
  36. def OAI.CriticalHoneycomb.Transfer.Planar.cup line 161
  37. def OAI.CriticalHoneycomb.Transfer.Planar.occupied line 164
  38. def OAI.CriticalHoneycomb.Transfer.Planar.vacant line 165
  39. def OAI.CriticalHoneycomb.Transfer.Planar.empty line 166
  40. theorem OAI.CriticalHoneycomb.Transfer.Planar.loop_erasure line 170

    Source documentation

    Ordinary transpose, not Hermitian adjoint: a closed unoriented loop has exactly weight zero at the source's phase.

    theorem loop_erasure : (∑ i : Fin 3, ∑ j : Fin 3, cup i j * cup i j) = 0 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.Planar.cup

  41. theorem OAI.CriticalHoneycomb.Transfer.Planar.snake_left line 176

    Source documentation

    Straightening a cup-cap pair leaves the occupied strand unchanged.

    theorem snake_left (i j : Fin 3) :
    (∑ k : Fin 3, cup i k * cup k j) = occupied i j := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.Planar.cup, OAI.CriticalHoneycomb.Transfer.Planar.occupied

  42. theorem OAI.CriticalHoneycomb.Transfer.Planar.snake_right line 181
  43. theorem OAI.CriticalHoneycomb.Transfer.Planar.tile_decomposition line 192

    Source documentation

    Exact dilute Temperley--Lieb decomposition of the source local tile. The eight connectivities carry precisely the coefficients listed in the physical crossing observable paragraph.

    theorem tile_decomposition (a h v c d : ℂ) (i j k l : Fin 3) :
    sourceR a h v c d (j,i) (k,l) =
      vacant i k * vacant j l +
      a * (occupied i k * vacant j l + vacant i k * occupied j l) +
      c * occupied i k * occupied j l +
      v * (empty i * empty l * occupied j k + empty j * empty k * occupied i l) +
      h * (cup i j * empty k * empty l + empty i * empty j * cup k l) +
      d * cup i j * cup k l := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.Planar.a, OAI.CriticalHoneycomb.Transfer.Planar.h, OAI.CriticalHoneycomb.Transfer.Planar.v, OAI.CriticalHoneycomb.Transfer.Planar.c, OAI.CriticalHoneycomb.Transfer.Planar.d, OAI.CriticalHoneycomb.Transfer.Planar.sourceR, OAI.CriticalHoneycomb.Transfer.Planar.vacant, OAI.CriticalHoneycomb.Transfer.Planar.occupied, OAI.CriticalHoneycomb.Transfer.Planar.empty, OAI.CriticalHoneycomb.Transfer.Planar.cup

  44. inductive OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape line 213

    Source documentation

    The eight choices of non-intersecting arcs in one actual triangular pair. W,S meet the up triangle; E,N meet the down triangle. The forbidden second two-arc choice would use both centers twice and is absent.

    inductive Shape
  | empty | westSouth | northEast | both | westNorth | southEast | westEast | northSouth
  deriving DecidableEq
  45. instance OAI.CriticalHoneycomb.Transfer.PhysicalTiles.(instance at line 216) line 216
  46. structure OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Selection line 219
  47. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape.selection line 227
  48. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Selection.upDegree line 237
  49. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Selection.downDegree line 238
  50. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Admissible line 240
  51. instance OAI.CriticalHoneycomb.Transfer.PhysicalTiles.(instance at line 242) line 242
  52. theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.selection_classification line 245

    Source documentation

    Local self-avoiding connectivity classification by both center degrees.

    theorem selection_classification (s : Selection) :
    Admissible s ↔ ∃ q : Shape, q.selection=s := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Selection, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Admissible, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape

  53. theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.selection_injective line 250
  54. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape.visits line 252
  55. theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.visits_eq line 258

    Source documentation

    The actual number of used centers, not the number of ports or arcs.

    theorem visits_eq (q : Shape) :
    q.visits = (if q.selection.upDegree=0 then 0 else 1) +
      (if q.selection.downDegree=0 then 0 else 1) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape

  56. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.shapeTensor line 265

    Source documentation

    Pure orientation kernel for a local connectivity. Indices are W,N,S,E, respectively: output order W,N, input order S,E in the braided drawing.

    noncomputable def shapeTensor (q : Shape) (w n s e : Fin 3) : ℂ :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape

  57. theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.physical_tile_expansion line 278

    Source documentation

    Critical weights count precisely the visited centers of the lozenge. This is a local equality of the exact R entries and actual path choices.

    theorem physical_tile_expansion (w n s e : Fin 3) :
    sourceR (kappa:ℂ) (kappa^2:ℂ) (kappa^2:ℂ) (kappa^2:ℂ) 0 (n,w) (s,e) =
      ∑ q : Shape, (kappa:ℂ)^q.visits * shapeTensor q w n s e := by
…

    Mentions: OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.shapeTensor

  58. inductive OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Node line 287
  59. instance OAI.CriticalHoneycomb.Transfer.PhysicalTiles.(instance at line 289) line 289
  60. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Node.position line 292
  61. def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Selection.adj line 300
  62. instance OAI.CriticalHoneycomb.Transfer.PhysicalTiles.(instance at line 307) line 307
  63. theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.selected_adjacent line 311

    Source documentation

    Every selected local edge is the exact source honeycomb adjacency.

    theorem selected_adjacent (s : Selection) (i j : ℤ) (a b : Node)
    (h : s.adj a b) : Adj (a.position i j) (b.position i j) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Selection, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Node, OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Adj

  64. theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.node_position_injective line 318

    Source documentation

    The local graph contains genuinely distinct centers, including its four exterior neighbor centers; no loop or collision is hidden by the drawing.

    theorem node_position_injective (i j : ℤ) : Function.Injective (Node.position i j) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Node.position

  65. theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.spectral_physical_tile_expansion line 331

    Source documentation

    The actual spectral weights, at the physical honeycomb specialization, are the exact local path expansion above. No R entries are altered.

    theorem spectral_physical_tile_expansion (w n s e : Fin 3) :
    sourceR (CriticalHoneycombTransfer.a CriticalHoneycombTransfer.L : ℂ)
      (CriticalHoneycombTransfer.h CriticalHoneycombTransfer.L : ℂ)
      (CriticalHoneycombTransfer.v CriticalHoneycombTransfer.L : ℂ)
      (CriticalHoneycombTransfer.c CriticalHoneycombTransfer.L : ℂ)
      (CriticalHoneycombTransfer.d CriticalHoneycombTransfer.L : ℂ) (n,w) (s,e) =
      ∑ q : Shape, (kappa:ℂ)^q.visits * shapeTensor q w n s e := by
…

    Mentions: OAI.CriticalHoneycombTransfer.a, OAI.CriticalHoneycombTransfer.L, OAI.CriticalHoneycombTransfer.h, OAI.CriticalHoneycombTransfer.v, OAI.CriticalHoneycombTransfer.c, OAI.CriticalHoneycombTransfer.d, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.shapeTensor