OAI/Combinatorics/HoneycombChords/RasterChords.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

Literal chord expansions in finite rectangles

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

  1. def OAI.CriticalHoneycomb.Transfer.RasterGrid.Matches line 16
  2. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.(instance at line 24) line 24
  3. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.maskedCell_sum line 29
  4. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.masked_orientation line 49

    Source documentation

    A resolved occupancy history is the literal finite-domain center sum with exactly its five occupied-edge masks, including each middle edge.

    theorem masked_orientation {W H : ℕ} (cfg : Cell W H → Shape)
    (σ : GridWire W H → Fin 3) :
    (kappa:ℂ)^(∑ t, (cfg t).visits) * (network W H).orientation cfg σ =
      ∑ μ : Cell W H → Fin 3, if Matches cfg σ μ then
        centerProduct (domain W H) (spins σ μ) else 0 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire, OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.RasterGrid.network, OAI.CriticalHoneycomb.Transfer.RasterGrid.Matches, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Transfer.RasterGrid.spins

  5. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.masked_chosenPartition line 73

    Source documentation

    Its prescribed-boundary contraction, with no auxiliary local model.

    theorem masked_chosenPartition {W H : ℕ} (cfg : Cell W H → Shape)
    (west east : Column H) (south north : Fin W → Fin 3) :
    (kappa:ℂ)^(∑ t, (cfg t).visits) * chosenPartition cfg west east south north =
      ∑ σ : {σ : GridWire W H → Fin 3 // HasWestNorth west north σ},
        ∑ μ : Cell W H → Fin 3,
          if (∀ j, σ.val (.inl (Fin.last W,j))=east j) ∧
              (∀ i, σ.val (.inr (i,0))=south i) ∧ Matches cfg σ.val μ then
            centerProduct (domain W H) (spins σ.val μ) else 0 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire, OAI.CriticalHoneycomb.Transfer.RasterGrid.HasWestNorth, OAI.CriticalHoneycomb.Transfer.RasterGrid.Matches, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Transfer.RasterGrid.spins

  6. def OAI.CriticalHoneycomb.Transfer.RasterGrid.selectionAt line 106
  7. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.selectionAt_admissible line 112
  8. def OAI.CriticalHoneycomb.Transfer.RasterGrid.occupancyShape line 120
  9. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.occupancyShape_selection line 124
  10. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.occupancyShape_matches line 129
  11. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matches_grid_occupied line 136
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matches_occupied line 158
  13. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.spins_injective line 171
  14. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.path_mask_unique line 184

    Source documentation

    If a fixed occupancy really is a simple actual path, every nonzero center term is its unique rooted orientation. This excludes the zero-branch without assuming any phase or noncancellation conclusion.

    theorem path_mask_unique {W H n : ℕ} (hW : 0<W) (hH : 0<H)
    (p : CenterPath n) {cfg : Cell W H → Shape}
    {σ τ : GridWire W H → Fin 3} {μ ν : Cell W H → Fin 3}
    (ha : Matches cfg σ μ) (hb : Matches cfg τ ν) (hp : spins τ ν=p.spins)
    (hc : ∀ i, p.center i∈domain W H)
    (hr : spins σ μ (p.edge 0)=outSpin (p.point 0) (p.side 0))
    (hn : centerProduct (domain W H) (spins σ μ)≠0) : σ=τ ∧ μ=ν := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire, OAI.CriticalHoneycomb.Transfer.RasterGrid.Matches, OAI.CriticalHoneycomb.Transfer.RasterGrid.spins, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain

  15. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.path_mask_contraction line 210

    Source documentation

    Reindexing a literal loop-free occupancy does not lose its nonzero rooted orientation inside the source rectangular transfer contraction.

    theorem path_mask_contraction {W H n : ℕ} (hW : 0<W) (hH : 0<H)
    (p : CenterPath n) (cfg : Cell W H → Shape)
    (west east : Column H) (south north : Fin W → Fin 3)
    (τ : GridWire W H → Fin 3) (ν : Cell W H → Fin 3)
    (hτ : HasWestNorth west north τ)
    (hE : ∀ j, τ (.inl (Fin.last W,j))=east j)
    (hS : ∀ i, τ (.inr (i,0))=south i)
    (hb : Matches cfg τ ν) (hp : spins τ ν=p.spins)
    (hc : ∀ i, p.center i∈domain W H)
    (j : Fin H) (hroot : p.edge 0=wireEmbedding (W:=W) (H:=H) (.inl (.inl (0,j))))
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire, OAI.CriticalHoneycomb.Transfer.RasterGrid.HasWestNorth, OAI.CriticalHoneycomb.Transfer.RasterGrid.Matches, OAI.CriticalHoneycomb.Transfer.RasterGrid.spins, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Transfer.RasterGrid.wireEmbedding

  16. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.path_chosen_nonzero line 251
  17. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.path_chosen_eq_one line 272

    Source documentation

    Exact one, not merely nonzero: a literal center chord has the normalized coefficient prescribed by the source single-strand transfer sector.

    theorem path_chosen_eq_one {W H n : ℕ} (hW : 0<W) (hH : 0<H)
    (p : CenterPath n) (cfg : Cell W H → Shape)
    (west east : Column H)
    (hi : (PlanarNormalization.occupancy (List.ofFn (fun j=>spinEquiv.symm (east j)))).count true=1)
    (ho : (PlanarNormalization.occupancy (List.ofFn (fun j=>spinEquiv.symm (west j)))).count true=1)
    (τ : GridWire W H → Fin 3) (ν : Cell W H → Fin 3)
    (hτ : HasWestNorth west (fun _=>1) τ)
    (hE : ∀ j, τ (.inl (Fin.last W,j))=east j)
    (hS : ∀ i, τ (.inr (i,0))=1)
    (hb : Matches cfg τ ν) (hp : spins τ ν=p.spins)
    (hc : ∀ i, p.center i∈domain W H)
    (h0 : p.point 0∉domain W H) (hl : p.point (Fin.last (n+1))∉domain W H)
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.occupancy, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire, OAI.CriticalHoneycomb.Transfer.RasterGrid.HasWestNorth, OAI.CriticalHoneycomb.Transfer.RasterGrid.Matches, OAI.CriticalHoneycomb.Transfer.RasterGrid.spins, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain

  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.cellCenter_mem line 297
  19. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.domain_coord_bounds line 302
  20. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.domain_wire_covered line 309
  21. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.path_wire_covered line 322
  22. def OAI.CriticalHoneycomb.Transfer.RasterGrid.restrictGrid line 336
  23. def OAI.CriticalHoneycomb.Transfer.RasterGrid.restrictMiddle line 338
  24. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.path_spins_restrict line 341
  25. def OAI.CriticalHoneycomb.Transfer.RasterGrid.pathShape line 358

    Source documentation

    Every actual loop-free path through the rectangle supplies an exact occupancy shape; no hypothetical shape data is needed.

    noncomputable def pathShape {W H n : ℕ} (p : CenterPath n) (hn : 0<n)
    (hc : ∀ i, p.center i∈domain W H)
    (h0 : p.point 0∉domain W H) (hl : p.point (Fin.last (n+1))∉domain W H) :
    Cell W H → Shape :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell

  26. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.pathShape_matches line 366
  27. def OAI.CriticalHoneycomb.Transfer.RasterGrid.westPort line 377
  28. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eastPort line 387
  29. def OAI.CriticalHoneycomb.Transfer.RasterGrid.southPort line 397
  30. def OAI.CriticalHoneycomb.Transfer.RasterGrid.northPort line 407
  31. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.westPort_side line 417
  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eastPort_side line 422
  33. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.southPort_side line 427
  34. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.northPort_side line 432
  35. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.westPort_wire line 437
  36. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eastPort_wire line 442
  37. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.southPort_wire line 447
  38. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.northPort_wire line 452
  39. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.westPort_injective line 457
  40. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eastPort_injective line 462
  41. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.west_ne_east line 467
  42. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.south_ne_west line 472
  43. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.south_ne_east line 479
  44. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.north_ne_west line 485
  45. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.north_ne_east line 491
  46. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.west_outside_ne_east line 499
  47. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.chord_length_pos line 509
  48. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_first line 513
  49. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_last line 518
  50. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_second line 525
  51. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_penultimate line 531
  52. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_center_mem line 543
  53. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_first_side line 548
  54. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_last_side line 555
  55. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_first_edge line 563
  56. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_last_edge line 570
  57. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.outside_incident_index line 578

    Source documentation

    A path never uses another exterior edge: its only outside incidences are the first and last edges, with their literal chronological indices.

    lemma CenterPath.outside_incident_index {n : ℕ} (p : CenterPath n)
    (hc : ∀ i, p.center i∈D) {v : Center} (hv : v∉D)
    (k : Fin 3) (j : Fin (n+1)) (he : incidentWire v k=p.edge j) :
    j=0 ∨ j=Fin.last n := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.incidentWire

  58. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_boundary_wire line 606
  59. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_boundary_vacant line 625
  60. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.RectChord line 636
  61. def OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath line 639
  62. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath_first_spins line 642
  63. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath_last_spins line 651
  64. def OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn line 661
  65. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn_occupancy line 663
  66. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath_west line 682
  67. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath_east line 696
  68. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath_north line 710
  69. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.rectanglePath_south line 718
  70. def OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangleShape line 726
  71. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_chord_chosen_one line 735

    Source documentation

    The normalized finite transfer coefficient of each literal source chord is exactly one. No path noncancellation or single-strand phase has been postulated; both are proved from the exact center tensors.

    theorem actual_chord_chosen_one {W H : ℕ} {j k : Fin (H+1)} (γ : RectChord W H j k) :
    chosenPartition (rectangleShape γ) (singleColumn j) (singleColumn k) (fun _=>1) (fun _=>1)=1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.RectChord, OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangleShape, OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn

  72. def OAI.CriticalHoneycomb.Transfer.ChordOrientations.usedCenter line 760
  73. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.usedCenter_degree line 763
  74. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.used_iff line 777
  75. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.center_injective line 793
  76. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.sum_used line 799
  77. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.shape_visits_used line 821
  78. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sum_visits_used line 842
  79. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_chord_visits line 855

    Source documentation

    Port half-edges are unweighted: the exact raster exponent is the number of centers in the source trace, with no additive endpoint correction.

    theorem actual_chord_visits {W H : ℕ} {j k : Fin (H+1)} (γ : RectChord W H j k) :
    (∑ t, (rectangleShape γ t).visits)=γ.val.length := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.RectChord, OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangleShape

  80. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.paths_eq_of_edges_subset line 871
  81. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.walk_in_closed_set line 897
  82. theorem OAI.CriticalHoneycomb.Transfer.PathComponents.two_port_path_unique line 910

    Source documentation

    The boundary path of a finite 0/2-degree configuration is unique. This prevents multiplicity in the physical path expansion.

    theorem two_port_path_unique [Fintype V] [DecidableRel G.Adj]
    {a b : V} (hab : a ≠ b) (ha : G.degree a = 1) (hb : G.degree b = 1)
    (upper : ∀ v, G.degree v ≤ 2) (p q : G.Walk a b)
    (hp : p.IsPath) (hq : q.IsPath) : p = q := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.v

  83. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.selected_edge line 930
  84. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.chord_boundary_selection line 934
  85. theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.chord_selected_path line 958

    Source documentation

    The converse path is bound to the actual selected midpoint edges, not just to the underlying hard-wall graph.

    theorem chord_selected_path {D : Finset Center} {a b : Port (D : Set Center)}
    (γ : Chord (D : Set Center) a b) (hab : a.outside≠b.outside) (s : Wire → Bool)
    (he : ∀ i, s ((ofChord γ hab).edge i)=true) :
    ∃ (xs : List (Interior D))
      (p : (selectedGraph a b s).Walk (.inr false) (.inr true)),
      xs.map Subtype.val=γ.val ∧ p.IsPath ∧
      p.support=Sum.inr false :: (xs.map Sum.inl ++ [Sum.inr true]) := by
…

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord

  86. theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.chord_eq_of_selected_eq line 1030

    Source documentation

    An unoriented occupied configuration has at most one literal source chord. This prevents hidden multiplicity in the finite transfer expansion.

    theorem chord_eq_of_selected_eq {D : Finset Center} {a b : Port (D : Set Center)}
    (γ δ : Chord (D : Set Center) a b) (hab : a.outside≠b.outside)
    (hs : selected (ofChord γ hab).spins=selected (ofChord δ hab).spins) : γ=δ := by
…

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord

  87. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangleShape_injective line 1067

    Source documentation

    No two different actual source chords are counted by the same literal raster shape configuration.

    theorem rectangleShape_injective {W H : ℕ} {j k : Fin (H+1)} :
    Function.Injective (rectangleShape (W:=W) (H:=H) (j:=j) (k:=k)) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.rectangleShape

  88. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.rectChordFintype line 1088
  89. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chord_term_real line 1091
  90. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.shape_term_nonnegative line 1100
  91. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_chord_sum_le_transfer line 1111

    Source documentation

    Every literal source chord appears with its exact critical weight and multiplicity one in the finite physical transfer expansion. Detached loops are not ignored here: all other fixed configurations are nonnegative.

    theorem actual_chord_sum_le_transfer {W H : ℕ} (j k : Fin (H+1)) :
    (∑ γ : RectChord W H j k, kappa^γ.val.length) ≤
      (prescribedPartition (W+1) (H+1) (singleColumn j) (singleColumn k) (fun _=>1) (fun _=>1)).re := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.RectChord, OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn

  92. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_chordMass_le_transfer line 1132

    Source documentation

    A finite-domain mass bound: the actual ENNReal chord mass is dominated by the literal source physical transfer coefficient.

    theorem actual_chordMass_le_transfer {W H : ℕ} (j k : Fin (H+1)) :
    chordMass (domain (W+1) (H+1) : Set Center) (westPort W H j) (eastPort W H k) ≤
      ENNReal.ofReal (prescribedPartition (W+1) (H+1) (singleColumn j) (singleColumn k)
        (fun _=>1) (fun _=>1)).re := by
…

    Mentions: OAI.CriticalHoneycomb.chordMass, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.RasterGrid.westPort, OAI.CriticalHoneycomb.Transfer.RasterGrid.eastPort, OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn