The endpoint-balanced E0/S0 lens inequality

The positive distance terms are first replaced by quadratic norm tangents. The two second-child radii are then divided into a small rational cover. On every rectangle, an explicit three-square Gram majorant, corrected by elementary two-vector squares, proves the required strict bound.

theorem LeanPool.Besicovitch.endpointBalancedE0S0LensBound_of_admissible {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) : EndpointBalancedE0S0LensBound configuration

The endpoint-balanced E0/S0 lens separator is negative for every admissible six-point configuration.