gap seed centre
ProvedFreiman.gap_seed_centrefreimangaphall-ray
Both marked seeds have central digit4, with exactly the stated left/right outward indexing.
Preamble
import Definitions.Def_Freiman_gapModel
Formal statement
namespace Freiman theorem gap_seed_centre (a : ℤ → ℕ+) (hs : gapMatch a 0 gapSeedA ∨ gapMatch a 0 gapSeedB) : localValue a 0 = 4 + cfValue (gapLeftTail a) + cfValue (gapRightTail a) := by sorry end Freiman
Source
Freiman Hall ray report, m3_maximum.tex and m3_minimum.tex; marked words