ChordTensors.lean`

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Orientations and tensor coefficients of chords

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

structure OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath line 18
Source documentation
A literal simple honeycomb path, including its two exterior endpoint centers. It will be applied only when those endpoints lie outside the rectangle.
```
structure CenterPath (n : ℕ) where
…
```
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.edge line 24
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.edge_injective line 27
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.outSpin line 42
Source documentation
Spin zero follows the positive source wire direction: west out of an up center, and middle/south into it. Spin two is the reverse direction.
```
def outSpin (v : Center) (k : Fin 3) : Fin 3 :=
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Center
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.inSpin line 45
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.outSpin_neighbor line 48
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.inSpin_neighbor line 53
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.outSpin_ne_empty line 57
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.spins line 60
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.spins_edge line 63
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.spins_off line 67
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.center line 71
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.in_wire line 74
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.out_wire line 80
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.sides_distinct line 83
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.incident_edge_iff line 92
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.spins_local line 117
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.localTensor line 133
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.localTensor_passage_nonzero line 136
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.center_nonzero line 148
Source documentation
The orientation directed along an actual simple center path has nonzero local weight at every visited center. All positions and slot orders are literal.
```
theorem CenterPath.center_nonzero {n : ℕ} (p : CenterPath n) (i : Fin n) :
    centerTensor p.spins (p.center i) ≠ 0 := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.localTensor_propagate line 158
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.factor line 171
Source documentation
The local tensor along the actual ordered center path, with two selected wires and all other wires vacant.
```
noncomputable def CenterPath.factor {n : ℕ} (p : CenterPath n) (i : Fin n)
    (σ : Fin (n+1) → Fin 3) : ℂ :=
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.in_direction line 176
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.factor_true line 182
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.orientation_unique line 198
Source documentation
Orientation propagates along every actual simple center path. Thus the boundary condition at the first wire determines all occupied wire labels.
```
theorem CenterPath.orientation_unique {n : ℕ} (p : CenterPath n)
    (σ : Fin (n+1) → Fin 3)
    (hroot : σ 0=outSpin (p.point 0) (p.side 0))
    (hf : ∀ i, p.factor i σ≠0) :
    σ=(fun i=>outSpin (p.point i.castSucc) (p.side i)) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Transfer.ChordOrientations.outSpin
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.orientationSum line 222
Source documentation
Literal finite orientation contraction of the actual path, with fixed source arrow and the final arrow summed (it will necessarily be the through arrow). This is not a new abstract kernel substituted for the center model.
```
noncomputable def CenterPath.orientationSum {n : ℕ} (p : CenterPath n) : ℂ := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.orientationSum_eq line 228
Source documentation
There is exactly one contributing orientation for a loop-free chord.
```
theorem CenterPath.orientationSum_eq {n : ℕ} (p : CenterPath n) :
    p.orientationSum=∏ i, centerTensor p.spins (p.center i) := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.orientationSum_ne_zero line 244
Source documentation
Noncancellation for a literal loop-free honeycomb center chord, rather than only for an abstract strand or a tensor with assumed coefficient.
```
theorem CenterPath.orientationSum_ne_zero {n : ℕ} (p : CenterPath n) :
    p.orientationSum≠0 := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.extendedTrace line 254
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.extendedTrace_length line 257
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.extendedTrace_nodup line 260
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.extendedTrace_chain line 272
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord line 300
Source documentation
Conversion of an actual simple chord (with its unweighted boundary ports) to the ordered-center model used in the tensor noncancellation proof.
```
noncomputable def ofChord (γ : Chord D a b) (hab : a.outside≠b.outside) :
    CenterPath γ.val.length := by
…
```
Mentions: OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_point line 314
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord_center line 318
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.chord_orientation_nonzero line 326
Source documentation
The already defined source Chord has a nonzero exact center-tensor orientation coefficient. This identifies the finite transfer coefficient with its path contribution.
```
theorem chord_orientation_nonzero (γ : Chord D a b) (hab : a.outside≠b.outside) :
    (ofChord γ hab).orientationSum ≠ 0 :=
…
```
Mentions: OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.ChordOrientations.ofChord
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.local_of_support line 335
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.factor_of_support line 347
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.full_orientation_unique line 358
Source documentation
Uniqueness concerns the actual full honeycomb wire assignment, not only the ordered list of path coefficients. Vacant wires are fixed to spin one.
```
theorem CenterPath.full_orientation_unique {n : ℕ} (p : CenterPath n) (σ : Wire → Fin 3)
    (hs : ∀ w, w ∉ Set.range p.edge → σ w=1)
    (hroot : σ (p.edge 0)=outSpin (p.point 0) (p.side 0))
    (hn : ∀ i, centerTensor σ (p.center i)≠0) : σ=p.spins := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.ChordOrientations.outSpin
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.point_cases line 373
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.incident_off line 383
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.off_center_one line 399
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.product_nonzero line 408
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.extendFiniteSpins line 420
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.extendFiniteSpins_at line 423
lemma OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.extend_restrict line 426
def OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.finiteContraction line 441
Source documentation
Exact finite center contraction restricted to the occupied set of one literal chord. Vacant wires have the actual spin one; the first boundary arrow is fixed. No orientation coefficient has been supplied as an input.
```
noncomputable def CenterPath.finiteContraction {n : ℕ} (p : CenterPath n)
    (D : Finset Center) (V : Finset Wire) : ℂ := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Wire
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.finiteContraction_eq line 451
Source documentation
The physical full-wire finite contraction is just its single directed path term. This binds noncancellation to actual center products on a domain.
```
theorem CenterPath.finiteContraction_eq {n : ℕ} (p : CenterPath n)
    (D : Finset Center) (V : Finset Wire)
    (he : ∀ i, p.edge i∈V) (hc : ∀ i, p.center i∈D) :
    p.finiteContraction D V=centerProduct D p.spins := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Wire
theorem OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath.finiteContraction_ne_zero line 483
Source documentation
Exact noncancellation of the loop-free component inside any containing finite domain excluding its two exterior endpoints.
```
theorem CenterPath.finiteContraction_ne_zero {n : ℕ} (p : CenterPath n)
    (D : Finset Center) (V : Finset Wire)
    (he : ∀ i, p.edge i∈V) (hc : ∀ i, p.center i∈D)
    (h0 : p.point 0∉D) (hl : p.point (Fin.last (n+1))∉D) :
    p.finiteContraction D V≠0 := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.ChordOrientations.CenterPath, OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Wire
def OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell line 496
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_empty line 503
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_westSouth line 509
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_northEast line 515
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_both line 521
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_westNorth line 527
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_southEast line 533
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_westEast line 539
lemma OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_northSouth line 545
theorem OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell_eq line 553
Source documentation
The fixed physical occupancy term is exactly the source shape tensor, including its two center weights and its actual middle-edge contraction.
```
theorem maskedCell_eq (q : Shape) (w n s e : Fin 3) :
    maskedCell q w n s e=(kappa:ℂ)^q.visits * shapeTensor q w n s e := by
…
```
Mentions: OAI.CriticalHoneycomb.Transfer.PhysicalTiles.Shape, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.maskedCell, OAI.CriticalHoneycomb.kappa, OAI.CriticalHoneycomb.Transfer.PhysicalTiles.shapeTensor