pi    = [3.141592653589793238462643383279, 3.141592653589793238462643383280]
lam   = [0.554953486817365890372902343686, 0.554953486817365890372902343687]
mu    = [0.890093026365268219254195312627, 0.890093026365268219254195312628]
c_H   = [0.074465754557949078734140241925, 0.074465754557949078734140241926]   (closed form phi(6)-2 lam)
c_H   = [0.074465754557949078734140241925, 0.074465754557949078734140241926]   (direct formula)
tangency defect phi(6) - (2 - mu + c_H) = [-1E-30, 1E-30]

k   Psi(k) = phi(k)-phi(6)                      Psi(k)+nu(k-6) (lower endpoint)      status
3   [0.277855493562998981, 0.277855493562998982]0.187855493563                      OK (>0)
4   [0.105771147919364732, 0.105771147919364733]0.0457711479194                     OK (>0)
5   [0.035580581963278091, 0.035580581963278092]0.00558058196328                    OK (>0)
6   [-1E-18, 1E-18]                             -3.40691086492e-87                  
7   [-0.020607389275078747, -0.020607389275078746]0.00939261072492                    OK (>0)
8   [-0.033648296528488087, -0.033648296528488086]0.0263517034715                     OK (>0)
9   [-0.042439349943293027, -0.042439349943293026]0.0475606500567                     OK
10  [-0.048653596092241967, -0.048653596092241966]0.0713464039078                     OK
12  [-0.056656836131293229, -0.056656836131293228]0.123343163869                      OK
20  [-0.068114859270178884, -0.068114859270178883]0.35188514073                       OK
50  [-0.073454135776528376, -0.073454135776528375]1.24654586422                       OK
100 [-0.074213010981948114, -0.074213010981948113]2.74578698902                       OK
1000[-0.074463227653624809, -0.074463227653624808]29.7455367723                       OK

admissible nu for k in {3,...,8}: [0.020607, 0.035581]
k>=9: trivial bound Psi(k) >= -c_H, and c_H/3 = 0.024821918185983026 < nu = 0.03 -> True
limit Psi(infinity) = 2 lam - phi(6) = -c_H : [-0.07446575455794907874, -0.07446575455794907873] vs [-0.07446575455794907874, -0.07446575455794907873]

(C) direct interval check, Lipschitz grid (|D_k'| <= max(mu, 2-mu) < 1.12; D_k convex)
k=3: grid min D_k = 0.18785556 at t=0.8600;  rigorous lower bound on [t_lo,t_hi] >= 0.18673556;  D at ends: 0.357577, 0.561399
      => D_k > 0 for all t > 0: True
k=4: grid min D_k = 0.04577152 at t=0.9740;  rigorous lower bound on [t_lo,t_hi] >= 0.04465152;  D at ends: 0.188976, 0.168805
      => D_k > 0 for all t > 0: True
k=5: grid min D_k = 0.00558138 at t=0.9940;  rigorous lower bound on [t_lo,t_hi] >= 0.00446138;  D at ends: 0.111981, 0.069044
      => D_k > 0 for all t > 0: True
k=6: grid min D_k = -0.00000000 at t=1.0000;  rigorous lower bound on [t_lo,t_hi] >= -0.00112000;  D at ends: 0.079526, 0.039475
      (k=6: min is 0 at t=1, by tangency; slack-lower-bound only)
k=7: grid min D_k = 0.00939365 at t=1.0020;  rigorous lower bound on [t_lo,t_hi] >= 0.00827365;  D at ends: 0.070333, 0.036590
      => D_k > 0 for all t > 0: True
k=8: grid min D_k = 0.02635183 at t=1.0020;  rigorous lower bound on [t_lo,t_hi] >= 0.02523183;  D at ends: 0.074262, 0.046342
      => D_k > 0 for all t > 0: True

Lipschitz constant check: max(mu, 2-mu) = 1.1099069736347318 < 1.12: True
ALL CERTIFIED: True
