Final upper bound for the 3-parameter recursive algorithm #
This file combines the four b-regions computed in
Distributed2Coloring/UpperBound/Recursive3Param/Regions.lean and
Distributed2Coloring/UpperBound/Recursive3Param/Bound.lean to get an exact rational value for
ClassicalAlgorithm.p recursive3ParamAlg, and derives the numerical bound
ClassicalAlgorithm.p recursive3ParamAlg < 24118/100000.
theorem
Distributed2Coloring.UpperBound.Recursive3Param.exists_algorithm_p_lt :
∃ (alg : ClassicalAlgorithm), alg.p < ENNReal.ofReal (24118 / 100000)