OAI/Combinatorics/HoneycombChords/PlanarDiagrams.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

Planar cup and cap normalization

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

  1. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.phase line 20
  2. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.phase_ne_zero line 21
  3. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.phase_sq line 22
  4. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.cup line 29
  5. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.loop_value line 32
  6. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.snake_left line 37
  7. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.snake_right line 41
  8. abbrev OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State line 45
  9. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create line 49

    Source documentation

    Insert an adjacent cup at a frontier position. States are zero on words too short for the requested position.

    noncomputable def create : ℕ → State → State
  | 0, f, a::b::xs => cup a b * f xs
  | 0, _, _ => 0
  | i+1, f, a::xs => create i (fun ys => f (a::ys)) xs
  | _+1, _, [] => 0

/-- Contract two adjacent frontier strands with the ordinary transpose cap. -/

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.cup

  10. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract line 56

    Source documentation

    Contract two adjacent frontier strands with the ordinary transpose cap.

    noncomputable def contract : ℕ → State → State
  | 0, f, xs => ∑ a : Bool, ∑ b : Bool, cup a b * f (a::b::xs)
  | i+1, f, a::xs => contract i (fun ys => f (a::ys)) xs
  | _+1, _, [] => 0

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.cup

  11. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create_prefix line 61
  12. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_prefix line 63
  13. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create_zero line 66
  14. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_zero line 78
  15. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_create_same line 88
  16. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_create_next line 104
  17. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_next_create line 120
  18. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create_add line 136
  19. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create_mul line 150
  20. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_mul line 164
  21. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create_mul_apply line 174
  22. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create_sum_bool line 177
  23. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_create_before line 183

    Source documentation

    A cap wholly to the left of a newly inserted cup commutes past it.

    lemma contract_create_before (i gap : ℕ) (f : State) :
    contract i (create (i+gap+2) f) = create (i+gap) (contract i f) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create

  24. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_create_after line 202

    Source documentation

    A cap wholly to the right of a newly inserted cup commutes past it.

    lemma contract_create_after (i gap : ℕ) (f : State) :
    contract (i+gap+2) (create i f) = create i (contract (i+gap) f) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create

  25. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.create_congr_length line 225
  26. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_congr_length line 246
  27. inductive OAI.CriticalHoneycomb.Transfer.PlanarNormalization.CupHistory line 269

    Source documentation

    A planar cup-only normal form. b is the number of through strands (0 for the empty boundary, 1 for one specified oriented path).

    inductive CupHistory (b : ℕ) : ℕ → Type
  | base : CupHistory b 0
  | insert {k : ℕ} (h : CupHistory b k) (i : ℕ) (hi : i ≤ b + 2*k) :
      CupHistory b (k+1)

    Mentions: OAI.CriticalHoneycomb.Transfer.h

  28. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.CupHistory.eval line 274
  29. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.optionEval line 278
  30. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.optionEval_map_insert line 283
  31. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract_history line 294

    Source documentation

    Contracting any adjacent two frontier strands in a planar cup normal form either removes a closed zero-weight loop or gives another cup normal form. This is the local-to-global cancellation step, at exact phase pi/4.

    theorem contract_history {b k : ℕ} (hb : b ≤ 1)
    (h : CupHistory b (k+1)) (j : ℕ) (hj : j ≤ b+2*k) (f : State) :
    ∃ r : Option (CupHistory b k), ∀ xs : List Bool, xs.length = b+2*k →
      contract j (h.eval f) xs = optionEval r f xs := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.CupHistory, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.contract, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.optionEval

  32. inductive OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PlanarWord line 369

    Source documentation

    A sliced planar diagram, with all vacant strands suppressed. The local moves are exactly cup creation and adjacent cap contraction; any number of identity tiles can be inserted without changing this word.

    inductive PlanarWord (b : ℕ) : ℕ → Type
  | start : PlanarWord b 0
  | insert {k : ℕ} (w : PlanarWord b k) (i : ℕ) (hi : i ≤ b+2*k) :
      PlanarWord b (k+1)
  | erase {k : ℕ} (w : PlanarWord b (k+1)) (i : ℕ) (hi : i ≤ b+2*k) :
      PlanarWord b k
  33. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PlanarWord.eval line 376
  34. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.word_normal_form line 381
  35. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.closed_word_zero line 425

    Source documentation

    Every nonempty closed planar arc diagram has zero contraction. This is a proved normalization theorem, not a loop-cancellation assumption.

    theorem closed_word_zero (w : PlanarWord 0 0) (hw : w ≠ .start) (f : State) :
    w.eval f [] = 0 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PlanarWord, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State

  36. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.one_strand_zero_or_identity line 452

    Source documentation

    A one-strand planar rectangle is either killed by a loop or acts as identity on its specified orientation. This gives the phase-1 alternative used for a surviving right-to-left path in the physical matrix expansion.

    theorem one_strand_zero_or_identity (w : PlanarWord 1 0) (f : State) :
    (∀ a : Bool, w.eval f [a] = 0) ∨ (∀ a : Bool, w.eval f [a] = f [a]) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PlanarWord, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.a

  37. abbrev OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin line 465
  38. abbrev OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState line 466
  39. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.occupancy line 468
  40. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.orientations line 469
  41. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed line 470
  42. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_add line 473
  43. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_smul line 478
  44. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_zero line 483
  45. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_false line 485
  46. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_true line 488
  47. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_false_some line 491
  48. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_true_none line 493
  49. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_cons_nil line 495
  50. structure OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights line 498
  51. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.tile line 505
  52. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act line 517
  53. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_add line 523
  54. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_smul line 536
  55. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_zero line 549
  56. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_empty_pair line 552
  57. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_left_pair line 565
  58. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_right_pair line 578
  59. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_full_pair line 591
  60. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_empty_at line 608
  61. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_left_at line 624
  62. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_right_at line 640
  63. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_full_at line 656
  64. inductive OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PlanarSpan line 676

    Source documentation

    Finite linear combinations of sliced planar diagrams with no incoming occupied strand. The count equality fixes the exact frontier arity.

    inductive PlanarSpan (n : ℕ) : DiluteState → Prop
  | zero : PlanarSpan n (fun _ => 0)
  | basis (o : List Bool) (k : ℕ) (w : PlanarWord 0 k)
      (hl : o.length = n) (hc : o.count true = 2*k) :
      PlanarSpan n (embed o (w.eval (fun _ => 1)))
  | add {f g : DiluteState} (hf : PlanarSpan n f) (hg : PlanarSpan n g) :
      PlanarSpan n (fun xs => f xs + g xs)
  | smul (z : ℂ) {f : DiluteState} (hf : PlanarSpan n f) :
      PlanarSpan n (fun xs => z * f xs)

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.PlanarWord, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed

  65. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.two_at line 686
  66. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_span line 704
  67. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_vacuum_pos line 741
  68. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_vacuum_zero line 751
  69. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.erased_empty line 755
  70. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_basis_vacuum line 759
  71. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_vacuum line 801
  72. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.circuit_vacuum line 813

    Source documentation

    A sequence of arbitrary nearest-neighbor dilute planar tiles cannot change the vacuum-to-vacuum coefficient. Nonempty closed diagrams cancel; this is the finite-network statement used in the physical crossing proof.

    theorem circuit_vacuum (n : ℕ) (gates : List (TileWeights × ℕ))
    (hg : ∀ g ∈ gates, g.2+1<n) :
    (gates.foldl (fun f g => act g.1 g.2 f)
      (embed (List.replicate n false) (fun _ => 1))) (List.replicate n none) = 1 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed

  73. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.spinIndex line 835

    Source documentation

    The manuscript's spin order is +,0,-; vacancies are not weighted.

    def spinIndex : Spin → Fin 3
  | none => 1
  | some false => 0
  | some true => 2

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin

  74. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourcePhase line 840
  75. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourcePhase_eq line 842
  76. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceR line 848

    Source documentation

    Verbatim source local R entries.

    noncomputable def sourceR (t : TileWeights) (p q : Fin 3 × Fin 3) : ℂ :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights

  77. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.tile_eq_sourceR line 866

    Source documentation

    The circuit tiles are exactly P R, not a substituted planar model.

    theorem tile_eq_sourceR (t : TileWeights) (i j k l : Spin) :
    tile t i j k l = sourceR t (spinIndex j, spinIndex i) (spinIndex k, spinIndex l) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.tile, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceR, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.spinIndex

  78. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addAux line 874

    Source documentation

    Introduce two vacant auxiliary wires at the input boundary.

    noncomputable def addAux (f : DiluteState) : DiluteState
  | none::none::xs => f xs
  | _ => 0

/-- Cap two vacant auxiliary wires at the output boundary. Boundary K is
implemented by one adjacent tile before this cap. -/

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.K, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.tile

  79. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.removeAux line 880

    Source documentation

    Cap two vacant auxiliary wires at the output boundary. Boundary K is implemented by one adjacent tile before this cap.

    noncomputable def removeAux (f : DiluteState) : DiluteState :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState

  80. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addAux_embed line 883
  81. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.removeAux_embed line 893
  82. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.addAux_span line 909
  83. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.removeAux_span line 941
  84. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates_span line 957
  85. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.gates_vacuum line 964
  86. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.auxNetwork line 974
  87. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.auxNetwork_span line 977
  88. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.auxNetwork_vacuum line 984

    Source documentation

    Inserting and then removing the two auxiliary wires preserves the same vacuum coefficient, so products of double-row networks do as well.

    theorem auxNetwork_vacuum {n : ℕ} (gs : List (TileWeights × ℕ))
    (hg : ∀ g ∈ gs, g.2+1<n+2) {f : DiluteState} (hf : PlanarSpan n f) :
    auxNetwork gs f (List.replicate n none) = f (List.replicate n none) := by
…

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

  89. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.boundaryWeights line 995
  90. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.K line 996
  91. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.boundary_input line 1001
  92. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.boundary_output line 1004
  93. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rEntry line 1010

    Source documentation

    The unswapped source R matrix, in the vacant/occupied encoding.

    noncomputable def rEntry (t : TileWeights) (a b p q : Spin) : ℂ :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin

  94. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rAux line 1015

    Source documentation

    Source R_{aux,i}: the auxiliary is the first wire, physical site i is at position i+1. All other wires are spectators.

    noncomputable def rAux (t : TileWeights) : ℕ → DiluteState → DiluteState
  | 0, f, a::b::xs => ∑ p : Spin, ∑ q : Spin, rEntry t a b p q * f (p::q::xs)
  | 0, _, _ => 0
  | i+1, f, a::b::xs =>
      rAux t i (fun zs => match zs with
        | p::ys => f (p::b::ys)
        | [] => 0) (a::xs)
  | _+1, _, _ => 0

/-- Move the auxiliary from the front to position i, preserving the
order of all physical sites. This is only a permutation, not a trace. -/

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rEntry

  95. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.moveAux line 1026

    Source documentation

    Move the auxiliary from the front to position i, preserving the order of all physical sites. This is only a permutation, not a trace.

    noncomputable def moveAux : ℕ → DiluteState → DiluteState
  | 0, f => f
  | i+1, f => fun xs => match xs with
    | x::ys => moveAux i (fun zs => match zs with
      | a::ws => f (a::x::ws)
      | [] => 0) ys
    | [] => 0

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

  96. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rAux_nil line 1034
  97. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rAux_singleton line 1036
  98. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_moveAux line 1040

    Source documentation

    The exact local permutation identity behind the planar row drawing.

    theorem act_moveAux (t : TileWeights) (i : ℕ) (f : DiluteState) :
    act t i (moveAux i f) = moveAux (i+1) (rAux t i f) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.moveAux, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rAux

  99. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.unswappedRow line 1067

    Source documentation

    Apply a row in visiting order; source U is this composition with its physical sites listed N,...,1, since the rightmost matrix acts first.

    noncomputable def unswappedRow : ℕ → List TileWeights → DiluteState → DiluteState
  | _, [], f => f
  | i, t::ts, f => unswappedRow (i+1) ts (rAux t i f)

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

  100. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow line 1071
  101. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_eq line 1077

    Source documentation

    A whole row of adjacent P R gates is exactly the source row of R matrices followed by moving its auxiliary wire to the output.

    theorem planarRow_eq (i : ℕ) (ts : List TileWeights) (f : DiluteState) :
    planarRow i ts (moveAux i f) =
      moveAux (i+ts.length) (unswappedRow i ts f) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.moveAux, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.unswappedRow

  102. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.moveAux_at line 1089
  103. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rAux_at line 1097
  104. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_at line 1107
  105. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.behind line 1118

    Source documentation

    Lift an operator through a spectator wire.

    noncomputable def behind (F : DiluteState → DiluteState) (f : DiluteState) : DiluteState
  | a::xs => F (fun ys => f (a::ys)) xs
  | [] => 0

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

  106. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_behind line 1122
  107. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_behind line 1128
  108. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.BCoordinates line 1139

    Source documentation

    Equivalence of coordinates when B is moved past n physical sites, with the A auxiliary fixed at the front.

    def BCoordinates (n : ℕ) (f g : DiluteState) : Prop :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState

  109. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.behind_move_B line 1143
  110. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.one_at line 1150
  111. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.rAux_BCoordinates line 1165
  112. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.unswappedRow_BCoordinates line 1183
  113. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_under line 1191
  114. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_BCoordinates line 1199
  115. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sourceTwoRows line 1211

    Source documentation

    Source U_A U_B in its original, unswapped spin labels A,B,sites.

    noncomputable def sourceTwoRows (tsA tsB : List TileWeights) (f : DiluteState) : DiluteState :=
…

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

  116. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.two_rows_eq line 1214