PhysicalTiles.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Physical center tensors and local connectivity

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

def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.spinOccupied line 16
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.vacant_support line 18
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.occupied_support line 20
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.empty_support line 22
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.cup_support line 24
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.shapeTensor_support line 29
Source documentation
Nonzero local orientation factors have exactly the selected occupied edges. Thus matching a wire spin also matches the unoriented occupancy.
```
theorem shapeTensor_support (q : Shape) (w n s e : Fin 3)
    (h : shapeTensor q w n s e ≠ 0) :
    spinOccupied w = q.selection.west ∧ spinOccupied n = q.selection.north ∧
      spinOccupied s = q.selection.south ∧ spinOccupied e = q.selection.east := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.shapeTensor, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.spinOccupied
structure OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork line 65
Source documentation
A finite gluing of the exact physical lozenges. A wire label shared by tiles is summed only once; open boundary values are imposed separately.
```
structure TileNetwork (V T : Type*) where
…
```
def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork.orientation line 71
def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork.physical line 76
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.physical_network_expansion line 83
Source documentation
The global finite product expansion, with the exact visited-center weight. No path/loop cancellation is assumed in this algebraic equality.
```
theorem physical_network_expansion {V T : Type*} [Fintype T] [DecidableEq T]
    (A : TileNetwork V T) (σ : V → Fin 3) :
    A.physical σ = ∑ q : T → Shape,
      (kappa:ℂ) ^ (∑ t, (q t).visits) * A.orientation q σ := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.kappa
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.contracted_network_expansion line 97
Source documentation
Full finite contraction with any fixed boundary weight. For a prescribed boundary spin assignment this factor is its zero/one indicator.
```
theorem contracted_network_expansion {V T : Type*} [Fintype V] [Fintype T] [DecidableEq V] [DecidableEq T]
    (A : TileNetwork V T) (boundary : (V → Fin 3) → ℂ) :
    (∑ σ, boundary σ * A.physical σ) =
      ∑ q : T → Shape, (kappa:ℂ) ^ (∑ t, (q t).visits) *
        ∑ σ, boundary σ * A.orientation q σ := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.kappa
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.orientation_support line 113
Source documentation
Every contributing shape assignment is globally consistent on all identified wires; there can be no spurious unmatched occupied half-edge.
```
theorem orientation_support {V T : Type*} [Fintype T] [DecidableEq T]
    (A : TileNetwork V T) (q : T → Shape) (σ : V → Fin 3)
    (h : A.orientation q σ ≠ 0) (t : T) :
    spinOccupied (σ (A.west t)) = (q t).selection.west ∧
    spinOccupied (σ (A.north t)) = (q t).selection.north ∧
    spinOccupied (σ (A.south t)) = (q t).selection.south ∧
    spinOccupied (σ (A.east t)) = (q t).selection.east := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.spinOccupied
def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.upTensor line 132
Source documentation
The three-leg tensor at one actual up triangle center. Its empty state has weight one, and each of the three simple passages has exactly one κ.
```
noncomputable def upTensor (w s m : Fin 3) : ℂ :=
…
```
def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.downTensor line 139
Source documentation
The down-center tensor, with the ordinary, not conjugate, contraction on the internal edge. The order m,n is essential for the snake identity.
```
noncomputable def downTensor (e n m : Fin 3) : ℂ :=
…
```
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.sourceR_eq_center_contraction line 147
Source documentation
Exact factorization through the actual middle honeycomb edge. Thus the integrable physical tile is a contraction of two genuine visited-center tensors, not only a list of formal connectivities.
```
theorem sourceR_eq_center_contraction (w n s e : Fin 3) :
    sourceR (kappa:ℂ) (kappa^2:ℂ) (kappa^2:ℂ) (kappa^2:ℂ) 0 (n,w) (s,e) =
      ∑ m : Fin 3, upTensor w s m * downTensor e n m := by
…
```
Mentions: OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.upTensor, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.downTensor
def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.centerOccupied line 156
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.upTensor_degree line 161
Source documentation
A nonzero occupied center has exactly two selected incident edges. Repeated centers and degree-four crossings are not hidden in the transfer.
```
theorem upTensor_degree (w s m : Fin 3) (h : upTensor w s m ≠ 0) :
    centerOccupied w s m=0 ∨ centerOccupied w s m=2 := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.upTensor, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.centerOccupied
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.downTensor_degree line 166
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.physical_network_center_expansion line 173
Source documentation
In any finite lozenge network, all internal middle-edge indices can be introduced simultaneously. All remaining wire indices are left unchanged.
```
theorem physical_network_center_expansion {V T : Type*} [Fintype T] [DecidableEq T]
    (A : TileNetwork V T) (σ : V → Fin 3) :
    A.physical σ = ∑ μ : T → Fin 3,
      ∏ t, upTensor (σ (A.west t)) (σ (A.south t)) (μ t) *
        downTensor (σ (A.east t)) (σ (A.north t)) (μ t) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.upTensor, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.downTensor
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.contracted_center_expansion line 184
Source documentation
The genuine finite center partition, including any prescribed boundary indicator. This is the exact tensor precursor to selecting the unique chord and cancelling its detached loop components.
```
theorem contracted_center_expansion {V T : Type*} [Fintype V] [Fintype T]
    [DecidableEq V] [DecidableEq T] (A : TileNetwork V T)
    (boundary : (V → Fin 3) → ℂ) :
    (∑ σ, boundary σ * A.physical σ) =
      ∑ σ : V → Fin 3, ∑ μ : T → Fin 3, boundary σ *
        ∏ t, upTensor (σ (A.west t)) (σ (A.south t)) (μ t) *
          downTensor (σ (A.east t)) (σ (A.north t)) (μ t) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.TileNetwork, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.upTensor, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.downTensor
def OAI.CriticalHoneycomb.Transfer.CenterPartition.centerTensor line 201
Source documentation
The tensor sits at an actual honeycomb center, indexed by its actual three honeycomb wires. The order at an up and a down center is the source physical R factorization order, not a symmetrized substitute.
```
noncomputable def centerTensor (σ : Wire → Fin 3) (v : Center) : ℂ :=
…
```
Mentions: OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Center
def OAI.CriticalHoneycomb.Transfer.CenterPartition.centerProduct line 207
def OAI.CriticalHoneycomb.Transfer.CenterPartition.selected line 210
lemma OAI.CriticalHoneycomb.Transfer.CenterPartition.nonzero_center_degree line 212
def OAI.CriticalHoneycomb.Transfer.CenterPartition.configurationOfNonzero line 226
Source documentation
This packages derived, not assumed, local degree conditions.
```
noncomputable def configurationOfNonzero {D : Finset Center}
    (a b : Port (D : Set Center)) (hab : a≠b) (σ : Wire → Fin 3)
    (hboundary : BoundarySelection a b (selected σ))
    (h : centerProduct D σ ≠ 0) : Configuration D a b :=
…
```
Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.CenterPartition.selected, OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.CenterPartition.centerProduct
theorem OAI.CriticalHoneycomb.Transfer.CenterPartition.nonzero_product_contains_chord line 238
Source documentation
Every contributing physical center configuration has an actual simple chord with precisely the prescribed ports. All other occupied components are detached cycles: the ensuing loop cancellation is a separate obligation.
```
theorem nonzero_product_contains_chord {D : Finset Center}
    (a b : Port (D : Set Center)) (hab : a≠b) (σ : Wire → Fin 3)
    (hboundary : BoundarySelection a b (selected σ))
    (h : centerProduct D σ ≠ 0) :
    ∃ (γ : Chord (D : Set Center) a b) (xs : List (Interior D))
      (p : (selectedGraph a b (selected σ)).Walk (.inr false) (.inr true)),
      xs.map Subtype.val = γ.val ∧ p.IsPath ∧
      p.support = Sum.inr false :: (xs.map Sum.inl ++ [Sum.inr true]) ∧
      ((selectedGraph a b (selected σ)) \ p.toSubgraph.spanningCoe).IsCycles :=
…
```
Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.CenterPartition.selected, OAI.CriticalHoneycomb.Transfer.h, OAI.CriticalHoneycomb.Transfer.CenterPartition.centerProduct, OAI.CriticalHoneycomb.Chord