=== Independent exact-rational recheck of BF3 Thm K computer-assisted step ===
intervals=  64 CaseC-empty= 16 boxes=  2784 maxdepth= 6 failures=0 min box margin=2.142e-07 min CaseA slack=2.305e-09
intervals=  32 CaseC-empty=  8 boxes=  1512 maxdepth= 6 failures=0 min box margin=2.538e-05 min CaseA slack=3.032e-07
intervals=  16 CaseC-empty=  4 boxes=   882 maxdepth= 6 failures=0 min box margin=6.995e-04 min CaseA slack=3.032e-07
intervals= 128 CaseC-empty= 32 boxes=  5301 maxdepth= 6 failures=0 min box margin=7.323e-05 min CaseA slack=2.305e-09
intervals= 256 CaseC-empty= 65 boxes= 10400 maxdepth= 6 failures=0 min box margin=3.679e-04 min CaseA slack=2.305e-09

per-interval (j, q0, aA, aB(q0), status, #boxes) for 64-interval cover:
(0, 0.375, 0.3104, 0.7142857142857143, 'ok', 544)
(1, 0.376953125, 0.3132, 0.7041942604856513, 'ok', 460)
(2, 0.37890625, 0.3158, 0.6943231441048034, 'ok', 325)
(3, 0.380859375, 0.3185, 0.6846652267818575, 'ok', 184)
(4, 0.3828125, 0.3211, 0.6752136752136753, 'ok', 160)
(5, 0.384765625, 0.3237, 0.6659619450317125, 'ok', 160)
(6, 0.38671875, 0.3263, 0.6569037656903766, 'ok', 160)
(7, 0.388671875, 0.3288, 0.6480331262939959, 'ok', 88)
(8, 0.390625, 0.3313, 0.639344262295082, 'ok', 88)
(9, 0.392578125, 0.3337, 0.6308316430020284, 'ok', 88)
(10, 0.39453125, 0.3361, 0.6224899598393574, 'ok', 73)
(11, 0.396484375, 0.3385, 0.614314115308151, 'ok', 64)
(12, 0.3984375, 0.3409, 0.6062992125984252, 'ok', 64)
(13, 0.400390625, 0.3432, 0.5984405458089669, 'ok', 40)
(14, 0.40234375, 0.3454, 0.5907335907335908, 'ok', 28)
(15, 0.404296875, 0.3477, 0.5831739961759083, 'ok', 28)
(16, 0.40625, 0.3499, 0.5757575757575758, 'ok', 28)
(17, 0.408203125, 0.352, 0.5684803001876173, 'ok', 28)
(18, 0.41015625, 0.3541, 0.5613382899628253, 'ok', 28)
(19, 0.412109375, 0.3562, 0.5543278084714549, 'ok', 28)
(20, 0.4140625, 0.3583, 0.5474452554744526, 'ok', 16)
(21, 0.416015625, 0.3603, 0.5406871609403255, 'ok', 10)
(22, 0.41796875, 0.3622, 0.5340501792114696, 'ok', 10)
(23, 0.419921875, 0.3641, 0.5275310834813499, 'ok', 10)
(24, 0.421875, 0.366, 0.5211267605633803, 'ok', 10)
(25, 0.423828125, 0.3678, 0.5148342059336823, 'ok', 10)
(26, 0.42578125, 0.3696, 0.5086505190311419, 'ok', 10)
(27, 0.427734375, 0.3714, 0.5025728987993139, 'ok', 4)
(28, 0.4296875, 0.3731, 0.4965986394557823, 'ok', 4)
(29, 0.431640625, 0.3748, 0.49072512647554806, 'ok', 4)
(30, 0.43359375, 0.3764, 0.48494983277591974, 'ok', 4)
(31, 0.435546875, 0.378, 0.4792703150912106, 'ok', 4)
(32, 0.4375, 0.3795, 0.47368421052631576, 'ok', 4)
(33, 0.439453125, 0.381, 0.46818923327895595, 'ok', 4)
(34, 0.44140625, 0.3824, 0.4627831715210356, 'ok', 1)
(35, 0.443359375, 0.3839, 0.45746388443017655, 'ok', 1)
(36, 0.4453125, 0.3852, 0.45222929936305734, 'ok', 1)
(37, 0.447265625, 0.3865, 0.4470774091627172, 'ok', 1)
(38, 0.44921875, 0.3878, 0.44200626959247646, 'ok', 1)
(39, 0.451171875, 0.389, 0.4370139968895801, 'ok', 1)
(40, 0.453125, 0.3902, 0.43209876543209874, 'ok', 1)
(41, 0.455078125, 0.3913, 0.42725880551301687, 'ok', 1)
(42, 0.45703125, 0.3924, 0.42249240121580545, 'ok', 1)
(43, 0.458984375, 0.3934, 0.4177978883861237, 'ok', 1)
(44, 0.4609375, 0.3944, 0.41317365269461076, 'ok', 1)
(45, 0.462890625, 0.3954, 0.4086181277860327, 'ok', 1)
(46, 0.46484375, 0.3963, 0.40412979351032446, 'ok', 1)
(47, 0.466796875, 0.3971, 0.39970717423133234, 'ok', 1)
(48, 0.46875, 0.3979, 0.3953488372093023, 'C empty')
(49, 0.470703125, 0.3987, 0.39105339105339104, 'C empty')
(50, 0.47265625, 0.3994, 0.3868194842406877, 'C empty')
(51, 0.474609375, 0.4, 0.38264580369843526, 'C empty')
(52, 0.4765625, 0.4006, 0.3785310734463277, 'C empty')
(53, 0.478515625, 0.4012, 0.3744740532959327, 'C empty')
(54, 0.48046875, 0.4017, 0.37047353760445684, 'C empty')
(55, 0.482421875, 0.4022, 0.3665283540802213, 'C empty')
(56, 0.484375, 0.4026, 0.3626373626373626, 'C empty')
(57, 0.486328125, 0.403, 0.3587994542974079, 'C empty')
(58, 0.48828125, 0.4033, 0.35501355013550134, 'C empty')
(59, 0.490234375, 0.4036, 0.351278600269179, 'C empty')
(60, 0.4921875, 0.4038, 0.34759358288770054, 'C empty')
(61, 0.494140625, 0.4039, 0.34395750332005315, 'C empty')
(62, 0.49609375, 0.4041, 0.3403693931398417, 'C empty')
(63, 0.498046875, 0.4041, 0.33682830930537355, 'C empty')

Hand cases (table of Sec 9.4):
q=3/8: CaseA ok=True; sign p(-1,0,s-,s+,2)=[-1, 1, -1, -1, 1]; s(aA)>=0.31449>=s-=0.31: True; s(aB)<=1.02062<=s+=1.05: True
q=2/5: CaseA ok=True; sign p(-1,0,s-,s+,2)=[-1, 1, -1, -1, 1]; s(aA)>=0.35355>=s-=0.35: True; s(aB)<=0.75000<=s+=1.0: True
q=5/12: CaseA ok=True; sign p(-1,0,s-,s+,2)=[-1, 1, -1, -1, 1]; s(aA)>=0.37363>=s-=0.36: True; s(aB)<=0.63901<=s+=1.0: True
