section Concrete

/-- The (8.6.5) coefficient-state datum with labels summing to `0`: `(a,-2), (-a,-1)`.  Its state is
the Fock excitation `a(-1)·ι(0)` (see `aState_lData`). -/
def lData (a : ℤ) : List (ℤ × ℤ) := [(a, -2), (-a, -1)]

theorem aLabel_lData (a : ℤ) : MM.FLM8.aLabel (lData a) = 0 := by
  simp [lData, MM.FLM8.aLabel]

/-- **THE STATE IDENTITY**: the (8.6.5) coefficient state of the two-entry datum `(a,-2),(-a,-1)` is
the single-creation-mode state `a(-1)·ι(0)`.  The Fock half `E^-(a)_{-2} = a(-1)` is form-independent,
and the second factor `E^-(-a)_{-1} = 1` is the identity. -/
theorem aState_lData {κ : Type} [Fintype κ] [DecidableEq κ] (bL : Module.Basis κ ℤ ℤ) (a : ℤ) :
    MM.FLM8.aState861 (R := instRLInt) (F := ℚ) bL (lData a)
      = creationModeState (R := instRLInt) (F := ℚ) a := by
  rw [show lData a = [(a, -2)] ++ [(-a, -1)] from rfl]
  rw [MM.FLM8.aState861, MM.FLM8.aState_append]
  simp only [MM.FLM8.aFock, List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, mul_one,
    MM.FLM8.aLabel_singleton, add_neg_cancel]
  rw [creationModeState]
  congr 1
  · -- the Fock half: E^-(a)_{-2} = a(-1) in M(1)
    rw [MM.FLM8.creationExpM1]
    rw [if_pos (by norm_num : (0 : ℤ) ≤ -(-2 : ℤ) - 1)]
    rw [MM.FLM8.expField_of_nonneg _ (by norm_num : (0 : ℤ) ≤ 1)]
    norm_num
    rw [MM.FLM8.expCoeff_succ_apply]
    norm_num
    rw [MM.FLM8.creationExponentM1_apply]
    norm_num
    rw [MM.FLM71.modeOf]
    rw [dif_pos (by norm_num : (-1 : ℤ) < 0)]
    norm_num
    rw [MM.FLM71.modeOfVL]
  · rfl

end Concrete