Freiman lower construction: initial n base n14

import Definitions.Def_Freiman_lowerInitialSeamData
import Definitions.Def_Freiman_lowerInitialNData
import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman

open scoped BigOperators

theorem Freiman.lower_initial_n_base_n14 : certFieldVal (lowerInitialNBase .n14) =
    (let w := lowerInitialNWords .n14
     prefixEval ((w 0).1++(w 0).2) lowerTau + prefixEval ((w 1).1++(w 1).2) lowerTau -
     prefixEval ((w 2).1++(w 2).2) lowerTau - prefixEval ((w 3).1++(w 3).2) lowerTau) := by
  sorry