import PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains

set_option backward.isDefEq.respectTransparency false

open PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains

-- Every field is visible; no supplied treatment or suppression proposition.
example (last : Nat) (leading correction : Complex) : firstOrderCountingContext last leading correction =
    { contributesAt := fun n _ q => n <= last ∧ q <= 0 ∧ (n : Int) - 1 = q
      noLaterThan := fun q s => q <= s
      suppressedRelativeTo := fun _ n m => 1 <= last ∧ n = 1 ∧ m = 0 ∧ ‖correction‖ < ‖leading‖
      retainedThrough := fun n q => q <= 0 ∧ ∃ vertices : List Nat,
        vertices ≠ [] ∧ n ∈ vertices ∧ (∀ j, j ∈ vertices -> j <= last) ∧
          (vertices.sum : Int) - 1 <= q
      resummedAt := fun n _ => ∀ bound : Nat, ∃ vertices : List Nat,
        vertices ≠ [] ∧ (∀ j, j ∈ vertices -> j <= last) ∧
          vertices.sum <= 1 ∧ bound < vertices.count n
      perturbativeAt := fun n _ => n <= last ∧ ∃ bound : Nat, ∀ vertices : List Nat,
        vertices ≠ [] -> (∀ j, j ∈ vertices -> j <= last) ->
          vertices.sum <= 1 -> vertices.count n <= bound } := rfl

-- Reduced vertex product and exactly one PDS factor per internal bubble.
example (g : Nat -> Real) (mu p : Real) (vertices : List Nat) :
    amplitude g mu p vertices =
      -((vertices.map (fun n => (g n : Complex))).prod *
        (p : Complex) ^ (2 * vertices.sum) *
        (-((mu : Complex) + Complex.I * (p : Complex))) ^ (vertices.length - 1)) := rfl

-- Complex-valued controls detect sign errors invisible in norm bounds.
example : amplitude (fun n => if n = 0 then -2 else 2) 1 1 [0] = 2 := by
  norm_num [amplitude]

example : amplitude (fun n => if n = 0 then -2 else 2) 1 1 [0, 0] =
    4 + 4 * Complex.I := by
  norm_num [amplitude]
  ring

example : amplitude (fun n => if n = 0 then -2 else 2) 1 1 [0, 1, 0] =
    -16 * Complex.I := by
  norm_num [amplitude, Complex.ext_iff, Complex.mul_re, Complex.mul_im, pow_two]

example : amplitude (fun _ => 1) 3 2 [2] = -16 := by
  norm_num [amplitude]

-- An allowed first derivative insertion need not be nonzero.
example (mu p : Real) : amplitude (fun n => if n = 0 then -2 else 0) mu p [0, 1, 0] = 0 := by
  simp [amplitude]