OAI/Combinatorics/HoneycombChords/ColumnTransfer.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Column transfer and occupancy normalization

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

  1. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_prefix line 15
  2. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_prefix line 24
  3. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.sum_spin_vectors_succ line 37
  4. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.columnContraction line 44

    Source documentation

    Contract the vertical wires within a literal column and all right-side input wires; the left-side output and upper auxiliary are not summed.

    noncomputable def columnContraction (t : TileWeights) (n : ℕ) (f : DiluteState)
    (west : Fin n → Spin) (north : Spin) : ℂ :=
…

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

  5. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.columnContraction_zero line 50
  6. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.columnContraction_succ line 55
  7. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_eq_columnContraction line 85

    Source documentation

    This is the exact tensor contraction equality for an arbitrary column, including each internal spin once. No cancellation or eigenvalue input.

    theorem planarRow_eq_columnContraction (t : TileWeights) (n : ℕ) (f : DiluteState)
    (west : Fin n → Spin) (north : Spin) :
    planarRow 0 (List.replicate n t) f (List.ofFn west ++ [north]) =
      columnContraction t n f west north := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.columnContraction

  8. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.columnKernelSpin line 99
  9. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.columnContraction_delta line 106
  10. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_delta line 120
  11. def OAI.CriticalHoneycomb.Transfer.RasterGrid.spinEquiv line 132
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.spinEquiv_apply line 138
  13. def OAI.CriticalHoneycomb.Transfer.RasterGrid.physicalWeights line 140
  14. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sourceR_eq line 143
  15. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.tile_physical line 146
  16. def OAI.CriticalHoneycomb.Transfer.RasterGrid.columnSpinEquiv line 154

    Source documentation

    Changing from vacant/arrow spins to the manuscript's +,0,- ordering.

    def columnSpinEquiv (H : ℕ) : (Fin H → PlanarNormalization.Spin) ≃ Column H :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.RasterGrid.Column

  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.columnSpinEquiv_apply line 157
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.columnKernel_eq_spin line 160
  19. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.columnKernel_eq_planarRow line 187

    Source documentation

    Exact physical lattice-column transfer as the already normalized planar cup/cap circuit. The boundary delta has not been replaced by any probability or connectivity assumption.

    theorem columnKernel_eq_planarRow (H : ℕ) (south north : PlanarNormalization.Spin)
    (west east : Fin H → PlanarNormalization.Spin) :
    columnKernel H (spinEquiv south) (spinEquiv north)
      (columnSpinEquiv H west) (columnSpinEquiv H east) =
      PlanarNormalization.planarRow 0 (List.replicate H physicalWeights)
        (fun xs => if xs=south::List.ofFn east then 1 else 0)
        (List.ofFn west++[north]) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Spin, OAI.CriticalHoneycomb.Transfer.RasterGrid.columnKernel, OAI.CriticalHoneycomb.Transfer.RasterGrid.spinEquiv, OAI.CriticalHoneycomb.Transfer.RasterGrid.columnSpinEquiv, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow, OAI.CriticalHoneycomb.Transfer.RasterGrid.physicalWeights

  20. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask line 202

    Source documentation

    Fix all occupied edges of a frontier, without fixing their orientations.

    noncomputable def mask (o : List Bool) (f : DiluteState) : DiluteState :=
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState

  21. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask_embed line 205
  22. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask_add line 218
  23. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask_smul line 224
  24. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask_zero line 230
  25. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask_span line 234
  26. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask_vacuum line 246
  27. structure OAI.CriticalHoneycomb.Transfer.PlanarNormalization.MaskedGate line 254

    Source documentation

    A fully resolved occupancy history. Summation now remains only over orientations; it is not a sum over different unoriented configurations.

    structure MaskedGate where
…
  28. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.maskedAct line 259
  29. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.maskedAct_span line 262
  30. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.maskedAct_vacuum line 266
  31. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.masked_history_vacuum line 272
  32. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.nonempty_closed_history_zero line 287

    Source documentation

    Exact cancellation of each nonempty closed unoriented configuration, not only cancellation after all configurations have been summed.

    theorem nonempty_closed_history_zero {n : ℕ} (gs : List MaskedGate)
    (hg : ∀ g ∈ gs, g.site+1<n)
    (hne : ∃ g ∈ gs, g.output ≠ List.replicate n false) :
    (gs.foldl (fun f g => maskedAct g f)
      (embed (List.replicate n false) (fun _ => 1))) (List.replicate n none) = 0 := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.MaskedGate, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.maskedAct, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed

  33. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolvedWeights line 307

    Source documentation

    Physical tile with the positive center-count factor removed. The forbidden double-return connectivity still has coefficient exactly zero.

    noncomputable def resolvedWeights : TileWeights := ⟨1,1,1,1,0⟩

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.TileWeights

  34. inductive OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Resolved line 311

    Source documentation

    After fixing all occupied wire sets, a physical honeycomb history is a single planar word or zero, not a linear superposition of connectivities.

    inductive Resolved (b n : ℕ) (root : State) : DiluteState → Prop
  | zero : Resolved b n root (fun _ => 0)
  | basis (o : List Bool) (k : ℕ) (w : PlanarWord b k)
      (hl : o.length=n) (hc : o.count true=b+2*k) :
      Resolved b n root (embed o (w.eval root))

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

  35. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.mask_disjoint_pair line 317
  36. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolved_mask_pair line 330
  37. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolved_step line 341

    Source documentation

    Exact source physical local action at fixed input and output occupancy. The positive κ-factors can be restored after this orientation calculation.

    lemma resolved_step {b n i : ℕ} (hb : b≤1) (hi : i+1<n) (out : List Bool)
    {root : State} {f : DiluteState} (hf : Resolved b n root f) :
    Resolved b n root (mask out (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.mask, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolvedWeights

  38. structure OAI.CriticalHoneycomb.Transfer.PlanarNormalization.ResolvedGate line 383
  39. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolvedAct line 387
  40. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolved_history line 390
  41. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.arrowState line 402

    Source documentation

    Put the same orientation on the occupied positions of a frontier. This is used only for frontiers with exactly one occupied edge.

    def arrowState (o : List Bool) (a : Bool) : List Spin :=
…

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

  42. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.occupancy_arrowState line 405
  43. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.orientations_arrowState line 411
  44. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.embed_arrowState line 418
  45. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolved_one_strand line 424

    Source documentation

    The exact phase normalization with every unoriented history fixed. There is no positivity assumption on the complex local phases.

    theorem resolved_one_strand {n : ℕ} {root : State} {f : DiluteState}
    (hf : Resolved 1 n root f) (out : List Bool) (hout : out.count true=1) :
    (∀ a : Bool, f (arrowState out a)=0) ∨
    (∀ a : Bool, f (arrowState out a)=root [a]) := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.PlanarNormalization.State, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.DiluteState, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.Resolved, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.PlanarNormalization.arrowState

  46. theorem OAI.CriticalHoneycomb.Transfer.PlanarNormalization.resolved_history_one_strand line 440