ImmPathShifts.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.occupationShift_immInternalPathEdges line 14
Source documentation
The signed creation/annihilation shift of the actual IMM edge list is exactly the layered vertex-path shift.
```
theorem occupationShift_immInternalPathEdges (d : ℕ) (side : Fin (d + 1) → Bool)
    (p : Fin d → Fin (d + 1)) :
    occupationShift (fun e => side e.1) (immInternalPathEdges d p) =
      pathShift (fun t => if side t then (-1 : ℤ) else 1)
        (immInternalPathVertices d p) := by
…
```
Mentions: OAI.Problem335.occupationShift, OAI.Problem335.immInternalPathEdges, OAI.Problem335.pathShift, OAI.Problem335.immInternalPathVertices

theorem OAI.Problem335.occupationShift_immInternalPathEdges_injective line 24

Source documentation

Different IMM paths have different signed occupation shifts.

theorem occupationShift_immInternalPathEdges_injective (d : ℕ)
    (side : Fin (d + 1) → Bool) :
    Function.Injective (fun p : Fin d → Fin (d + 1) =>
      occupationShift (fun e => side e.1) (immInternalPathEdges d p)) := by
…

Mentions: OAI.Problem335.occupationShift, OAI.Problem335.immInternalPathEdges

theorem OAI.Problem335.immInternalPath_target_injective_of_amplitudes_ne_zero line 36

Source documentation

Nonzero normalized IMM path actions cannot collide at a natural occupation.

theorem immInternalPath_target_injective_of_amplitudes_ne_zero (d : ℕ)
    (side : Fin (d + 1) → Bool)
    (M : (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) →₀ ℕ)
    (p q : Fin d → Fin (d + 1))
    (hp : ((immInternalPathEdges d p).map
      (occupationAmplitude (fun e => side e.1) M)).prod ≠ 0)
    (hq : ((immInternalPathEdges d q).map
      (occupationAmplitude (fun e => side e.1) M)).prod ≠ 0)
    (heq : pathOccupation (fun e => side e.1) (immInternalPathEdges d p) M =
      pathOccupation (fun e => side e.1) (immInternalPathEdges d q) M) : p = q := by
…

Mentions: OAI.Problem335.immInternalPathEdges, OAI.Problem335.occupationAmplitude, OAI.Problem335.pathOccupation

theorem OAI.Problem335.immInternalPath_collision_zero line 54

Source documentation

The collision-zero hypothesis of the first-trace expansion for genuine IMM paths.

theorem immInternalPath_collision_zero (d : ℕ) (side : Fin (d + 1) → Bool)
    (M : (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) →₀ ℕ)
    (p q : Fin d → Fin (d + 1)) (hpq : p ≠ q)
    (heq : pathOccupation (fun e => side e.1) (immInternalPathEdges d p) M =
      pathOccupation (fun e => side e.1) (immInternalPathEdges d q) M) :
    ((immInternalPathEdges d p).map (occupationAmplitude (fun e => side e.1) M)).prod *
      ((immInternalPathEdges d q).map (occupationAmplitude (fun e => side e.1) M)).prod = 0 := by
…

Mentions: OAI.Problem335.pathOccupation, OAI.Problem335.immInternalPathEdges, OAI.Problem335.occupationAmplitude