ImmSecondTrace.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The second trace identity for the actual IMM operator in normalized monomial coordinates. Invalid path actions have zero amplitude, so their chosen finite target index does not enter the trace.

def OAI.Problem335.immPathSignedShift line 16

Source documentation

The signed exponent displacement of an actual IMM path.

def immPathSignedShift (n : ℕ) (hn : 0 < n)
    (isV : (Fin n × Fin n × Fin n) → Bool)
    (p : Fin (immPaths n hn).length) : (Fin n × Fin n × Fin n) →₀ ℤ :=
…

Mentions: OAI.Problem335.immPaths

theorem OAI.Problem335.signedOccupation_immPathOccupation line 22

Source documentation

Every nonzero actual path action has its prescribed signed displacement.

theorem signedOccupation_immPathOccupation (n : ℕ) (hn : 0 < n)
    (isV : (Fin n × Fin n × Fin n) → Bool)
    (d : (Fin n × Fin n × Fin n) →₀ ℕ) (p : Fin (immPaths n hn).length)
    (hamp : immPathAmplitude n hn isV d p ≠ 0) :
    signedOccupation (immPathOccupation n hn isV d p) =
      signedOccupation d + immPathSignedShift n hn isV p := by
…

Mentions: OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.signedOccupation, OAI.Problem335.immPathOccupation, OAI.Problem335.immPathSignedShift

def OAI.Problem335.immCoefficientMatrix line 32

Source documentation

A finite submatrix of the genuine normalized IMM operator.

def immCoefficientMatrix {I J : Type*} (n : ℕ)
    (isV : (Fin n × Fin n × Fin n) → Bool)
    (source : I → (Fin n × Fin n × Fin n) →₀ ℕ)
    (target : J → (Fin n × Fin n × Fin n) →₀ ℕ) : Matrix J I ℂ :=
…

theorem OAI.Problem335.immCoefficientMatrix_eq_pathShiftMatrix line 41

Source documentation

The finite normalized coefficient matrix is the actual weighted path matrix whenever all nonzero path actions are represented in its target coordinates.

theorem immCoefficientMatrix_eq_pathShiftMatrix {I J : Type*}
    [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (n : ℕ) (hn : 0 < n) (isV : (Fin n × Fin n × Fin n) → Bool)
    (source : I → (Fin n × Fin n × Fin n) →₀ ℕ)
    (target : J → (Fin n × Fin n × Fin n) →₀ ℕ)
    (htarget : Function.Injective target)
    (shift : I → Fin (immPaths n hn).length → J)
    (hshift : ∀ i p, immPathAmplitude n hn isV (source i) p ≠ 0 →
      target (shift i p) = immPathOccupation n hn isV (source i) p) :
    immCoefficientMatrix n isV source target =
      pathShiftMatrix shift (fun i p => (immPathAmplitude n hn isV (source i) p : ℂ)) := by
…

Mentions: OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.immPathOccupation, OAI.Problem335.immCoefficientMatrix, OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.immCoefficientMatrix_second_trace line 67

Source documentation

Source-eliminated second trace for the genuine finite IMM coefficient matrix. The only coordinate hypothesis says that nonzero path actions stay in the chosen target basis; no trace or moment formula is assumed.

theorem immCoefficientMatrix_second_trace {I J : Type*}
    [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (n : ℕ) (hn : 0 < n) (isV : (Fin n × Fin n × Fin n) → Bool)
    (source : I → (Fin n × Fin n × Fin n) →₀ ℕ)
    (hsource : Function.Injective source)
    (target : J → (Fin n × Fin n × Fin n) →₀ ℕ)
    (htarget : Function.Injective target)
    (shift : I → Fin (immPaths n hn).length → J)
    (hshift : ∀ i p, immPathAmplitude n hn isV (source i) p ≠ 0 →
      target (shift i p) = immPathOccupation n hn isV (source i) p) :
    let A := immCoefficientMatrix n isV source target
…

Mentions: OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.immPathOccupation, OAI.Problem335.immCoefficientMatrix

def OAI.Problem335.immFinitePathShift line 100
Source documentation
A finite target index for each path. The fallback is used only for a zero-amplitude path, and is therefore invisible in the operator matrix.
```
def immFinitePathShift (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ)
    (e0 : ImmTargetIndex n side a b) (d : ImmSourceIndex n side a b)
    (p : Fin (immPaths n hn).length) : ImmTargetIndex n side a b := by
…
```
Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immPaths
theorem OAI.Problem335.immFinitePathShift_val_of_amplitude_ne_zero line 109
theorem OAI.Problem335.immNormalizedMatrix_eq_immCoefficientMatrix line 120
Source documentation
The finite normalized operator matrix is the indicated submatrix of its ambient normalized monomial coefficients.
```
theorem immNormalizedMatrix_eq_immCoefficientMatrix
    (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ) :
    immNormalizedMatrix n side a b =
      immCoefficientMatrix n (fun x => side x.1)
        (fun d : ImmSourceIndex n side a b => d.1)
        (fun e : ImmTargetIndex n side a b => e.1) := by
…
```
Mentions: OAI.Problem335.immNormalizedMatrix, OAI.Problem335.immCoefficientMatrix, OAI.Problem335.ImmSourceIndex, OAI.Problem335.ImmTargetIndex

theorem OAI.Problem335.immNormalizedMatrix_eq_pathShiftMatrix_of_fallback line 132

Source documentation

The actual finite IMM matrix has a weighted finite-path representation.

theorem immNormalizedMatrix_eq_pathShiftMatrix_of_fallback
    (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ)
    (e0 : ImmTargetIndex n side a b) :
    immNormalizedMatrix n side a b =
      pathShiftMatrix (immFinitePathShift n hn side a b e0)
        (fun d p => (immPathAmplitude n hn (fun x => side x.1) d.1 p : ℂ)) := by
…

Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.immNormalizedMatrix, OAI.Problem335.pathShiftMatrix, OAI.Problem335.immFinitePathShift, OAI.Problem335.immPathAmplitude

theorem OAI.Problem335.immNormalizedMatrix_second_trace line 147
Source documentation
Exact source-eliminated second trace of the genuine finite IMM operator. This includes an empty target space: then every path amplitude vanishes. There are no trace, closure, or nonempty-index assumptions in the statement.
```
theorem immNormalizedMatrix_second_trace
    (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ) :
    let A := immNormalizedMatrix n side a b
…
```
Mentions: OAI.Problem335.immNormalizedMatrix