OAI/Combinatorics/HoneycombChords/BoundarySystems.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

All-boundary chord decompositions

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

  1. def OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryWire line 16

    Source documentation

    The actual four rectangle cuts; internal edges are not constrained.

    def BoundaryWire {W H : ℕ} : GridWire W H → Prop
  | .inl (i,_) => i=0 ∨ i=Fin.last W
  | .inr (_,j) => j=0 ∨ j=Fin.last H

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.GridWire

  2. def OAI.CriticalHoneycomb.Transfer.RasterGrid.SameBoundary line 20
  3. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sameBoundary_refl line 23
  4. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sameBoundary_symm line 24
  5. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sameBoundary_trans line 26
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sameBoundary_hasBoundary line 29
  7. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.erase_sameBoundary line 50
  8. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.fill_sameBoundary line 61
  9. instance OAI.CriticalHoneycomb.Transfer.RasterGrid.(instance at line 72) line 72
  10. def OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm line 74
  11. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm_ne_zero line 78
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm_eq_masked line 85
  13. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.arbitrary_boundary_path_factorization line 98

    Source documentation

    Removing one actual oriented component, retaining every other boundary port in the residual path system.

    theorem arbitrary_boundary_path_factorization {W H n : ℕ} (hW : 0<W) (hH : 0<H)
    (cfg cfgR : Cell W H → Shape)
    (p : CenterPath n) (x₀ : Assignment W H)
    (hx₀ : relativeTerm cfg x₀ x₀≠0)
    (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)
    (hcover : ∀ i, p.edge i∈Set.range (wireEmbedding (W:=W) (H:=H)))
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment, OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Transfer.RasterGrid.wireEmbedding

  14. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.localTensor_pair_unique line 204
  15. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.orientation_agree line 213

    Source documentation

    Unique propagation for either orientation of an actual path.

    lemma CenterPath.orientation_agree {n : ℕ} (p : CenterPath n)
    (σ τ : Fin (n+1)→Fin 3) (hr : σ 0=τ 0)
    (hs : ∀ i,p.factor i σ≠0) (ht : ∀ i,p.factor i τ≠0) : σ=τ := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath

  16. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.selected_orientation_agree line 225
  17. def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.restrictSpins line 240
  18. def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.superpose line 242
  19. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.restrict_center line 244
  20. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.restrict_off line 254
  21. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.restrict_product_ne_zero line 260
  22. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.restrict_center_agree line 272
  23. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.remove_reference_product line 280
  24. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.superpose_tensor line 297
  25. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.superpose_off line 308
  26. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.superpose_product line 315
  27. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.erase_superpose line 328
  28. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.superpose_erase line 335
  29. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.selected_superpose_congr line 342
  30. def OAI.CriticalHoneycomb.Transfer.RasterGrid.superposeAssignment line 354
  31. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.superposeAssignment_spins line 357
  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.superpose_sameBoundary line 364
  33. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.all_orientation_path_factorization line 375
  34. instance OAI.CriticalHoneycomb.Transfer.AllPorts.portFintype line 481
  35. abbrev OAI.CriticalHoneycomb.Transfer.AllPorts.Vertices line 491
  36. def OAI.CriticalHoneycomb.Transfer.AllPorts.selectedRel line 493
  37. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.selectedRel_symm line 498
  38. def OAI.CriticalHoneycomb.Transfer.AllPorts.graph line 511
  39. instance OAI.CriticalHoneycomb.Transfer.AllPorts.graphDecidable line 520
  40. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.port_neighbors line 523
  41. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.port_degree line 529
  42. def OAI.CriticalHoneycomb.Transfer.AllPorts.sideNeighbor line 535
  43. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.side_unique line 538
  44. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.neighbor_unique line 543
  45. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.side_has_neighbor line 560
  46. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.side_adj line 569
  47. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.adj_side line 575
  48. def OAI.CriticalHoneycomb.Transfer.AllPorts.neighborEquiv line 582
  49. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.center_degree line 600
  50. theorem OAI.CriticalHoneycomb.Transfer.AllPorts.selected_port_partner line 616

    Source documentation

    A selected boundary component ends at another selected boundary port. This is derived from the actual local 0/2 rule and the finite handshake lemma, with no prescribed pairing assumed.

    theorem selected_port_partner {D : Finset Center} (s : Wire→Bool)
    (hd : ∀ v∈D,selectedSideCount s v=0 ∨ selectedSideCount s v=2)
    (a : Port (D : Set Center)) (ha : s a.wire=true) :
    ∃ b : Port (D : Set Center), b≠a ∧ s b.wire=true ∧
      ∃ p : (graph D s).Walk (.inr a) (.inr b),p.IsPath ∧
        ∀ v∈p.support,p.toSubgraph.neighborSet v=(graph D s).neighborSet v := by
…

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Transfer.AllPorts.graph

  51. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.port_degree_le_one line 668
  52. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.port_mem_support_ends line 679
  53. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.list_all_inl_many line 703
  54. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.support_decomposition_many line 716

    Source documentation

    The inside trace of any simple component between degree-one ports; other marked boundary ports cannot occur in its interior.

    lemma support_decomposition_many (G : SimpleGraph (α⊕β)) [DecidableRel G.Adj]
    (hd : ∀ q : β,G.degree (.inr q)≤1) {a b : β} (hab : a≠b)
    (p : G.Walk (.inr a) (.inr b)) (hp : p.IsPath) :
    ∃ xs : List α,p.support=Sum.inr a::(xs.map Sum.inl++[Sum.inr b]) ∧ xs.Nodup := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.a

  55. def OAI.CriticalHoneycomb.Transfer.AllPorts.hardRel line 752
  56. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.selected_hard line 757
  57. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.chain_snoc_ports line 766
  58. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.chain_ports line 785
  59. def OAI.CriticalHoneycomb.Transfer.AllPorts.vertexCenter line 802
  60. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.selected_to_actual line 805
  61. lemma OAI.CriticalHoneycomb.Transfer.AllPorts.chord_edges line 828
  62. theorem OAI.CriticalHoneycomb.Transfer.AllPorts.nonzero_contains_chord line 852

    Source documentation

    At each selected port of an actual nonzero configuration, its isolated component is a literal simple-center chord, even with other marked ports.

    theorem nonzero_contains_chord {D : Finset Center} (σ : Wire→Fin 3)
    (h : centerProduct D σ≠0) (a : Port (D : Set Center))
    (ha : σ a.wire≠1) :
    ∃ b : Port (D : Set Center),b≠a ∧ σ b.wire≠1 ∧
      ∃ γ : Chord (D : Set Center) a b,
        ∀ hab : a.outside≠b.outside,∀ i,σ ((ofChord γ hab).edge i)≠1 := by
…

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

  63. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.port_exhaustive line 880
  64. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.port_outside_injective line 891
  65. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sameBoundary_port line 909
  66. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm_change_reference line 922
  67. def OAI.CriticalHoneycomb.Transfer.RasterGrid.occupiedWires line 929
  68. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.erase_occupied_subset line 932
  69. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.erase_occupied_card_lt line 945
  70. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.boundary_recursion_step line 964

    Source documentation

    One genuine all-boundary recursion step: an actual chord is removed, any detached cycles remain in the residual sum, and the finite support strictly decreases. No global path expansion is assumed.

    theorem boundary_recursion_step {W H : ℕ} (cfg : Cell (W+1) (H+1)→Shape)
    (x : Assignment (W+1) (H+1))
    (hx : relativeTerm cfg x x≠0)
    (a : Port (domain (W+1) (H+1) : Set Center))
    (ha : assignmentSpins x a.wire≠1) :
    ∃ (b : Port (domain (W+1) (H+1) : Set Center)) (hab : a.outside≠b.outside)
      (γ : Chord (domain (W+1) (H+1) : Set Center) a b)
      (cfgR : Cell (W+1) (H+1)→Shape),
      let p:=ofChord γ hab
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment, OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Transfer.RasterGrid.domain, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.RasterGrid.assignmentSpins, OAI.CriticalHoneycomb.Chord

  71. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.ports_vacuum_sameBoundary line 1011
  72. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.relative_sum_vacuum line 1031
  73. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.nonzero_vacuum_empty line 1040
  74. structure OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord line 1067

    Source documentation

    Literal chord components with endpoints on any two distinct rectangle ports.

    structure BoundaryChord (W H : ℕ) where
…
  75. def OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.path line 1072
  76. def OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.amplitude line 1074
  77. def OAI.CriticalHoneycomb.Transfer.RasterGrid.systemAmplitude line 1077
  78. inductive OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem line 1083

    Source documentation

    A fully selected list of actual path components, ending with no occupied wire. This is a structural conclusion, not an axiom enumerating tensor terms.

    inductive SelectedSystem {W H : ℕ} : Assignment (W+1) (H+1)→List (BoundaryChord W H)→Prop
  | nil : SelectedSystem ((fun _=>1),(fun _=>1)) []
  | cons (x : Assignment (W+1) (H+1)) (c : BoundaryChord W H) (cs : List (BoundaryChord W H))
      (selected : ∀ i,assignmentSpins x (c.path.edge i)≠1)
      (nonzero : ∀ i,centerTensor (assignmentSpins x) (c.path.center i)≠0)
      (rest : SelectedSystem (eraseAssignment c.path x) cs) : SelectedSystem x (c::cs)

/-- No detached polygon survives the all-boundary orientation sum. Every
nonzero resolved shape is a finite system of literal honeycomb chords,
and its coefficient is the exact product of their isolated amplitudes. -/

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment, OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord, OAI.CriticalHoneycomb.Transfer.c, OAI.CriticalHoneycomb.Transfer.RasterGrid.assignmentSpins, OAI.CriticalHoneycomb.Transfer.RasterGrid.eraseAssignment, OAI.CriticalHoneycomb.Transfer.a

  79. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.all_boundary_shape_decomposition line 1093

    Source documentation

    No detached polygon survives the all-boundary orientation sum. Every nonzero resolved shape is a finite system of literal honeycomb chords, and its coefficient is the exact product of their isolated amplitudes.

    theorem all_boundary_shape_decomposition {W H : ℕ} (cfg : Cell (W+1) (H+1)→Shape)
    (x : Assignment (W+1) (H+1)) (hx : relativeTerm cfg x x≠0)
    (hn : (∑ y : Assignment (W+1) (H+1),relativeTerm cfg x y)≠0) :
    ∃ cs : List (BoundaryChord W H),SelectedSystem x cs ∧
      (∑ y : Assignment (W+1) (H+1),relativeTerm cfg x y)=systemAmplitude x cs := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment, OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm, OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord, OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem, OAI.CriticalHoneycomb.Transfer.RasterGrid.systemAmplitude

  80. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.physical_phase_norm line 1127
  81. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.localTensor_norm_nonempty line 1129
  82. lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.restrict_product_norm line 1141
  83. def OAI.CriticalHoneycomb.Transfer.RasterGrid.systemNodes line 1168
  84. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.nodes_mem line 1170
  85. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord.amplitude_norm line 1180
  86. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.amplitude_norm line 1189
  87. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.empty_center line 1198
  88. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.nodes_nodup line 1220
  89. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.edge_union line 1242
  90. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.selected_eq line 1259
  91. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.shape_unique line 1270
  92. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.all_boundary_literal_norm line 1279

    Source documentation

    Full all-boundary shape decomposition at exactly its actual κ-weight, including center-disjointness and the uniqueness required for subsequent mass comparisons.

    theorem all_boundary_literal_norm {W H : ℕ} (cfg : Cell (W+1) (H+1)→Shape)
    (x : Assignment (W+1) (H+1)) (hx : relativeTerm cfg x x≠0)
    (hn : (∑ y : Assignment (W+1) (H+1),relativeTerm cfg x y)≠0) :
    ∃ cs : List (BoundaryChord W H),SelectedSystem x cs ∧ (systemNodes cs).Nodup ∧
      ‖∑ y : Assignment (W+1) (H+1),relativeTerm cfg x y‖=kappa^(systemNodes cs).length := by
…

    Mentions: OAI.CriticalHoneycomb.Transfer.RasterGrid.Cell, OAI.CriticalHoneycomb.Transfer.RasterGrid.Assignment, OAI.CriticalHoneycomb.Transfer.RasterGrid.relativeTerm, OAI.CriticalHoneycomb.Transfer.RasterGrid.BoundaryChord, OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem, OAI.CriticalHoneycomb.Transfer.RasterGrid.systemNodes, OAI.CriticalHoneycomb.kappa