FourPathTrace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Elimination of the second source index in the four-path trace formula.

theorem OAI.Problem335.sum_source_eq_zeroExtend line 16

Source documentation

Extending finite source weights by zero gives the unique weight at a specified occupation vector; this lemma also handles invalid occupations.

theorem sum_source_eq_zeroExtend {I : Type u_1} {G : Type u_3}
    [Fintype I] [AddCommGroup G] [DecidableEq G] (occupation : I → G)
    (hinj : Function.Injective occupation) (weight : I → ℝ) (x : G) :
    (∑ k, if occupation k = x then weight k else 0) =
      Function.extend occupation weight (fun _ => 0) x := by
…

theorem OAI.Problem335.fourPath_eliminate_source line 33

Source documentation

The second source in a compatible four-path term is uniquely determined. The zero extension records absent (invalid) source occupations exactly.

theorem fourPath_eliminate_source (occupation : I → G)
    (hinj : Function.Injective occupation) (wq ws : I → ℝ)
    (M ep eq er es : G) (A C : ℝ) :
    (∑ k, if M + ep = occupation k + eq ∧ M + er = occupation k + es then
      A * wq k * C * ws k else 0) =
      if ep - eq = er - es then
        A * Function.extend occupation wq (fun _ => 0) (M + ep - eq) * C *
          Function.extend occupation ws (fun _ => 0) (M + ep - eq)
      else 0 := by
…

theorem OAI.Problem335.fourPath_sum_eliminate_source line 83

Source documentation

The full four-path sum with the second source eliminated and invalid source occupations retained through zero extension.

theorem fourPath_sum_eliminate_source [Fintype P]
    (occupation : I → G) (hinj : Function.Injective occupation)
    (eps : P → G) (weight : I → P → ℝ) :
    (∑ i, ∑ k, ∑ p, ∑ q, ∑ r, ∑ s,
      if occupation i + eps p = occupation k + eps q ∧
        occupation i + eps r = occupation k + eps s then
        weight i p * weight k q * weight i r * weight k s else 0) =
    ∑ i, ∑ p, ∑ q, ∑ r, ∑ s,
      if eps p - eps q = eps r - eps s then
        weight i p * Function.extend occupation (fun k => weight k q) (fun _ => 0)
          (occupation i + eps p - eps q) * weight i r *
        Function.extend occupation (fun k => weight k s) (fun _ => 0)
…

theorem OAI.Problem335.complex_path_second_trace_eliminate_source line 118

Source documentation

The complex four-path trace with its second source removed. The signed shift identity is required only for nonzero path weights, so invalid-path fallback target indices do not affect the identity.

theorem complex_path_second_trace_eliminate_source
    {J : Type*} [Fintype J] [Fintype P] [DecidableEq I] [DecidableEq J]
    (occupation : I → G) (hinj : Function.Injective occupation)
    (targetOccupation : J → G) (htarget : Function.Injective targetOccupation)
    (eps : P → G) (shift : I → P → J) (weight : I → P → ℝ)
    (hshift : ∀ i p, weight i p ≠ 0 →
      targetOccupation (shift i p) = occupation i + eps p) :
    let A := pathShiftMatrix shift (fun i p => (weight i p : ℂ))
…

Mentions: OAI.Problem335.pathShiftMatrix