OAI/Combinatorics/HoneycombChords/Occupancy.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Resolved occupancy contractions

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

  1. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask line 17

    Source documentation

    Local occupancy projection. Unlike an entire frontier mask this fixes only the two wires touched by one actual lozenge.

    noncomputable def pairMask : ℕ → Bool → Bool → DiluteState → DiluteState
  | 0,a,b,f,x::y::xs => if x.isSome=a ∧ y.isSome=b then f (x::y::xs) else 0
  | 0,_,_,_,_ => 0
  | i+1,a,b,f,x::xs => pairMask i a b (fun ys => f (x::ys)) xs
  | _+1,_,_,_,[] => 0

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.a

  2. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_zero line 23
  3. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_add line 34
  4. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_smul line 45
  5. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_embed line 56
  6. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_resolved line 83
  7. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_two_choices line 96
  8. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_two_resolved line 113
  9. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pair_resolved_step line 127

    Source documentation

    A specified local output pair selects at most one of the source's two allowed physical connectivities; no superposition of planar words remains.

    lemma pair_resolved_step {b n i : ℕ} (hb : b≤1) (hi : i+1<n) (x y : Bool)
    {root : State} {f : DiluteState} (hf : Resolved b n root f) :
    Resolved b n root (pairMask i x y (act resolvedWeights i f)) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Resolved, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolvedWeights

  10. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeAction line 168

    Source documentation

    Exact chosen physical lozenge connectivity, before restoring κ^visits.

    noncomputable def shapeAction (q : PhysicalTiles.Shape) (i : ℕ) (f : DiluteState) : DiluteState :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState

  11. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeAction_resolved line 172
  12. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.chosen_tile_eq_shape line 182
  13. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeAction_zero line 194

    Source documentation

    A chosen shape operation is the literal source orientation tensor, not merely an abstraction with the same support.

    lemma shapeAction_zero (q : PhysicalTiles.Shape) (f : DiluteState) (w n : Spin) (xs : List Spin) :
    shapeAction q 0 f (w::n::xs) =
      ∑ s : Spin, ∑ e : Spin,
        PhysicalTiles.shapeTensor q (spinIndex w) (spinIndex n) (spinIndex s) (spinIndex e) *
          f (s::e::xs) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeAction, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.shapeTensor, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.spinIndex

  14. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addOne line 230
  15. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.removeOne line 234
  16. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addOne_embed line 236
  17. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.removeOne_embed line 243
  18. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addOne_resolved line 257
  19. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.removeOne_resolved line 270
  20. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRow line 285
  21. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRow_resolved line 289
  22. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeColumn line 297
  23. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeColumn_resolved line 300
  24. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRectangle line 307

    Source documentation

    A specified lozenge-shape configuration in a literal finite rectangle, scanned east-to-west with unmarked north/south boundaries.

    noncomputable def shapeRectangle (cfg : List (List PhysicalTiles.Shape))
    (f : DiluteState) : DiluteState := cfg.foldl (fun f qs=>shapeColumn qs f) f

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeColumn

  25. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRectangle_resolved line 310
  26. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRectangle_one_strand line 321

    Source documentation

    Endpointwise normalized orientation coefficient for a fixed finite physical configuration. This is 0 or the identity, without assuming nonnegativity of the complex local tensor entries.

    theorem shapeRectangle_one_strand {n : ℕ} (cfg : List (List PhysicalTiles.Shape))
    (hn : ∀ qs∈cfg, qs.length=n) (input out : List Bool) (hi : input.length=n)
    (hc : input.count true=1) (hout : out.count true=1) (root : State) :
    (∀ a : Bool, shapeRectangle cfg (embed input root) (arrowState out a)=0) ∨
    (∀ a : Bool, shapeRectangle cfg (embed input root) (arrowState out a)=root [a]) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRectangle, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.arrowState

  27. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.pairMask_prefix line 334
  28. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeAction_prefix line 342
  29. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRow_prefix line 355
  30. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeContraction line 368
  31. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeContraction_zero line 376
  32. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeContraction_succ line 380
  33. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRow_eq_contraction line 410

    Source documentation

    Every internal vertical variable of the normalized physical shape column is summed exactly once by the literal planar raster scan.

    theorem shapeRow_eq_contraction {n : ℕ} (q : Fin n → PhysicalTiles.Shape) (f : DiluteState)
    (west : Fin n → Spin) (north : Spin) :
    shapeRow 0 (List.ofFn q) f (List.ofFn west++[north]) = shapeContraction q f west north := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeRow, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeContraction

  34. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeKernel line 423
  35. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeColumn_eq_kernel line 431
  36. def OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenColumnProduct line 455
  37. def OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenColumnKernel line 460
  38. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.orientation_columns line 465
  39. def OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition line 481

    Source documentation

    The finite prescribed-boundary orientation coefficient of one exact unoriented honeycomb configuration.

    noncomputable def chosenPartition {W H : ℕ} (cfg : Cell W H → Shape)
    (west east : Column H) (south north : Fin W → Fin 3) : ℂ :=
…

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

  40. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition_eq_matrixPath line 488
  41. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition_eq_transfer line 507
  42. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition_eq_grid_sum line 513
  43. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenColumnKernel_eq_spin line 536
  44. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.occupancy_orientations_injective line 564
  45. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.orientations_length line 589
  46. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_delta line 595
  47. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.eq_arrowState line 609
  48. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeFold line 616
  49. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.shapeFold_resolved line 619
  50. def OAI.CriticalHoneycomb.Transfer.RasterGrid.columnVector line 632
  51. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenColumn_mulVec line 635
  52. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenProduct_mulVec line 653
  53. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vector_delta line 662
  54. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition_zero_or_one line 681

    Source documentation

    Fixed-shape normalized crossing coefficients on the exact source grid are 0 or 1, endpointwise. No positivity of local complex phases is assumed.

    theorem chosenPartition_zero_or_one {W H : ℕ} (cfg : Cell W H → Shape)
    (west east : Column H)
    (hi : (occupancy (List.ofFn (fun j=>spinEquiv.symm (east j)))).count true=1)
    (ho : (occupancy (List.ofFn (fun j=>spinEquiv.symm (west j)))).count true=1) :
    chosenPartition cfg west east (fun _=>1) (fun _=>1)=0 ∨
    chosenPartition cfg west east (fun _=>1) (fun _=>1)=1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column, OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition

  55. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolved_vacuum line 723
  56. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuum_delta_resolved line 742
  57. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenPartition_eq_shapeFold line 772
  58. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.chosen_vacuum_zero_or_one line 795

    Source documentation

    Actual finite-grid orientation coefficient with fixed unoriented configuration and vacant boundary. It is real and nonnegative, despite its complex local factors.

    theorem chosen_vacuum_zero_or_one {W H : ℕ} (cfg : Cell W H → Shape) :
    chosenPartition cfg (fun _=>1) (fun _=>1) (fun _=>1) (fun _=>1)=0 ∨
    chosenPartition cfg (fun _=>1) (fun _=>1) (fun _=>1) (fun _=>1)=1 := by
…

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

  59. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribed_shape_expansion line 804
  60. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addOne_span line 824
  61. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.removeOne_span line 850
  62. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_span line 866
  63. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_vacuum line 874
  64. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumColumn line 884

    Source documentation

    A literal column with unmarked top and bottom ports.

    noncomputable def vacuumColumn (t : TileWeights) (n : ℕ) (f : DiluteState) : DiluteState :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState

  65. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumColumn_span line 887
  66. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumColumn_vacuum line 893
  67. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumRectangle line 903

    Source documentation

    Finite physical columns cannot create an unmarked closed contribution: all such closed loops cancel exactly at the manuscript parameter.

    theorem vacuumRectangle (t : TileWeights) (n m : ℕ) :
    ((vacuumColumn t n)^[m]) (embed (List.replicate n false) (fun _ => 1))
      (List.replicate n none) = 1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumColumn, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed

  68. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addOne_cons line 925
  69. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumColumn_eq_kernel line 930

    Source documentation

    The finite orientation sum and the column operator agree also for a general boundary state, so that consecutive columns compose exactly.

    lemma vacuumColumn_eq_kernel (t : TileWeights) (n : ℕ) (f : DiluteState)
    (west : Fin n → Spin) :
    vacuumColumn t n f (List.ofFn west) =
      ∑ east : Fin n → Spin, columnKernelSpin t n none none west east * f (List.ofFn east) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.vacuumColumn, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.columnKernelSpin

  70. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.column_mulVec line 952
  71. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.column_pow_mulVec line 970
  72. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vector_vacuum line 978
  73. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_vacuum_entry line 997

    Source documentation

    The actual finite strip transfer has unmarked empty-empty entry one. This is a literal honeycomb-grid identity, not an assumed loop pairing.

    theorem physical_vacuum_entry (H W : ℕ) :
    ((columnKernel H 1 1)^W) (fun _=>1) (fun _=>1) = 1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.columnKernel

  74. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribed_vacuum_partition line 1009

    Source documentation

    Equivalent four-wall statement for the finite physical tensor partition.

    theorem prescribed_vacuum_partition (W H : ℕ) :
    prescribedPartition W H (fun _=>1) (fun _=>1) (fun _=>1) (fun _=>1) = 1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribedPartition

  75. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.shapeTensor_empty_ne_zero line 1021
  76. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenColumnProduct_empty line 1026
  77. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenColumnKernel_empty line 1046
  78. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosenProduct_empty_vacuum line 1061
  79. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosen_empty_partition line 1072
  80. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.chosen_nonempty_vacuum_zero line 1088

    Source documentation

    Every nonempty fixed unoriented configuration with vacant boundary has vanishing orientation sum on the actual finite honeycomb grid. No turning lemma or assumed graphical cancellation is being invoked.

    theorem chosen_nonempty_vacuum_zero {W H : ℕ} (cfg : Cell W H → Shape)
    (hne : cfg ≠ fun _=>.empty) :
    chosenPartition cfg (fun _=>1) (fun _=>1) (fun _=>1) (fun _=>1)=0 := by
…

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