OAI/Combinatorics/HoneycombChords/RasterGrid.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Finite honeycomb raster contractions

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

  1. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell line 16
  2. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire line 19

    Source documentation

    Horizontal wires run west/east; vertical wires run south/north. The extra endpoint in each coordinate is literal, not periodic boundary data.

    abbrev GridWire (W H : ℕ) := (Fin (W+1) × Fin H) ⊕ (Fin W × Fin (H+1))
  3. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.FullWire line 20
  4. def OAI.CriticalHoneycomb.Transfer.RasterGrid.network line 22
  5. def OAI.CriticalHoneycomb.Transfer.RasterGrid.wireEmbedding line 28
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.wireEmbedding_injective line 33
  7. def OAI.CriticalHoneycomb.Transfer.RasterGrid.spins line 52
  8. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.spins_wire line 56
  9. def OAI.CriticalHoneycomb.Transfer.RasterGrid.cellCenter line 60
  10. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.cellCenter_injective line 63
  11. def OAI.CriticalHoneycomb.Transfer.RasterGrid.domain line 70
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.up_wires line 73
  13. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.down_wires line 79
  14. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.up_centerTensor line 85
  15. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.down_centerTensor line 92
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.center_product_eq line 100

    Source documentation

    Product of actual visited-center tensors on the literal rectangle.

    lemma center_product_eq {W H : ℕ} (σ : GridWire W H → Fin 3) (μ : Cell W H → Fin 3) :
    centerProduct (domain W H) (spins σ μ) =
      ∏ t : Cell W H, upTensor (σ ((network W H).west t)) (σ ((network W H).south t)) (μ t) *
        downTensor (σ ((network W H).east t)) (σ ((network W H).north t)) (μ t) := by
…

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

  17. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.grid_physical_eq_centers line 113

    Source documentation

    The source finite physical network contracts precisely to the actual center tensors on the rectangle, with every internal middle wire summed.

    theorem grid_physical_eq_centers (W H : ℕ) (σ : GridWire W H → Fin 3) :
    (network W H).physical σ = ∑ μ : Cell W H → Fin 3,
      centerProduct (domain W H) (spins σ μ) := by
…

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

  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sum_vectors_cons line 127
  19. def OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath line 135

    Source documentation

    A finite matrix path expansion, used only for the actual physical column kernels below. All intermediate states are summed once.

    noncomputable def matrixPath {α : Type*} [Fintype α] [DecidableEq α] {n : ℕ}
    (K : Fin n → Matrix α α ℂ) (a b : α) : ℂ :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.a

  20. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath_zero line 140
  21. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath_succ line 145
  22. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath_eq_prod line 163
  23. abbrev OAI.CriticalHoneycomb.Transfer.RasterGrid.Column line 174
  24. def OAI.CriticalHoneycomb.Transfer.RasterGrid.columnProduct line 176
  25. def OAI.CriticalHoneycomb.Transfer.RasterGrid.columnKernel line 180
  26. def OAI.CriticalHoneycomb.Transfer.RasterGrid.spinsFromColumns line 188

    Source documentation

    Literal grid spins after fixing the west and north outer boundaries. The remaining horizontal and vertical wires are genuine independent coordinates, not redundant copies at the centers.

    def spinsFromColumns {W H : ℕ} (west : Column H) (north : Fin W → Fin 3)
    (horizontal : Fin W → Column H) (vertical : Fin W → Column H) : GridWire W H → Fin 3
  | .inl (i,j) => (Fin.cons (α:=fun _=>Column H) west horizontal) i j
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire

  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_columns line 193
  28. def OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition line 209

    Source documentation

    Actual finite grid tensor with all four boundary spin lists prescribed. West and north are built into the parametrization; east and south are imposed by their exact indicator, before performing any orientation sum.

    noncomputable def prescribedPartition (W H : ℕ) (west east : Column H)
    (south north : Fin W → Fin 3) : ℂ :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Column

  29. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition_eq_matrixPath line 216
  30. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition_eq_transfer line 238

    Source documentation

    The exact full finite rectangle contraction is the product of its physical column matrices. Together with grid_physical_eq_centers this connects the transfer ordering to the literal center tensors.

    theorem prescribedPartition_eq_transfer (W H : ℕ) (west east : Column H)
    (south north : Fin W → Fin 3) :
    prescribedPartition W H west east south north =
      (List.ofFn (fun i => columnKernel H (south i) (north i))).prod west east := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.columnKernel

  31. def OAI.CriticalHoneycomb.Transfer.RasterGrid.HasWestNorth line 246

    Source documentation

    The parametrization has exactly the actual spin assignments with the west/north walls fixed; no geometric configurations are dropped.

    def HasWestNorth {W H : ℕ} (west : Column H) (north : Fin W → Fin 3)
    (σ : GridWire W H → Fin 3) : Prop :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire

  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.spinsFromColumns_boundary line 250
  33. def OAI.CriticalHoneycomb.Transfer.RasterGrid.gridSpinsEquiv line 255
  34. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.fixedGridSpinsFintype line 280
  35. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition_eq_grid_sum line 285

    Source documentation

    Exact literal finite-network expression for the prescribed partition.

    theorem prescribedPartition_eq_grid_sum (W H : ℕ) (west east : Column H)
    (south north : Fin W → Fin 3) :
    prescribedPartition W H west east south north =
      ∑ σ : {σ : GridWire W H → Fin 3 // HasWestNorth west north σ},
        if (∀ j, σ.val (.inl (Fin.last W,j))=east j) ∧
            (∀ i, σ.val (.inr (i,0))=south i) then
          (network W H).physical σ.val else 0 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition, OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire, OAI.CriticalHoneycomb.Transfer.RasterGrid.HasWestNorth, OAI.CriticalHoneycomb.Transfer.RasterGrid.network