By: ValentinHirschi <valentin.hirschi@gmail.com>
Add opt-in projective sections to bilinear_general (contract extension)
`solver.projective_sections` (default false, bilinear_general only, not
with merge = "aggressive") is an explicit contract extension: a cell's
upper boundary may be a projective section, RootIndexDomain::
PositiveOrInfinity = "the index-th distinct strictly positive root of P,
or +infinity where fewer exist". Cells stay connected open cylindrical
cells in the compactified coordinate x/(1+x).
With the replayed ratio orders a<=c, b<=d, c<=d and Delta = m*G^2 (m>0),
the positive fiber of F = (a*y+b)*x + (c*y+d) over a base point is empty
for d<0 and exactly {0<y<Y*, 0<x<X(y)} for d>0 (Y*, X: positive root of
c*y+d, of F in x, or +infinity). The planner then uses the single piece
{d>0} (no split) plus the empty claim {d<0}; without the premises it
keeps the strict plan. The verifier requires the option, the Square
separator, the three replayed orders, a non-constant d and exactly the
projective piece and claim, verifies the piece and rebuilds every cell.
Every other verifier rejects positive_or_infinity bounds, the
compatibility merge refuses them, and comparison and the sanity sampler
treat a missing root as +infinity. Option off: plans, piece files and
results are unchanged.
Positive Gluza33 (original constraints, guide U, optimized base, anchor
x4, order [x4,x7,x2,x1,x0,x6,x3,x5] and the x3-last variant): 2,372
verified cells in about 0.4 s.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>