gap forcing checks 4
ProvedFreiman.gap_forcing_checks_4freimangaphall-ray
Every terminal of the digit-4 forcing tree is a cap contradiction, a lower/upper table consequence, a below-window bound, or exactly A/B with correct reflection and alignment.
Preamble
import Definitions.Def_Freiman_gapCertificateData
Formal statement
namespace Freiman theorem gap_forcing_checks_4 : gapChecks gapLowerRows gapUpperRows .reduction gapForcingTree4 := by sorry end Freiman
Source
Freiman Hall ray report, certificates/gap/forcing_partition.json