Witnessed Boolean Contracts: Sound Local Distance Guarantees for Approximate Implicit CSG
Hard min/max operations preserve the sign of exact implicit solids but generally destroy signed-distance semantics. Arbitrarily small, sign-preserving value perturbations can rotate the normalized gradient by nearly a right angle and displace a gradient-projected boundary witness by a finite amount. We formalize this as the absence of a value-only stability modulus for witness projection. We introduce a witnessed Boolean contract checking value and gradient errors, positive reach, active-branch separation, and a Lipschitz visibility margin at the approximate witness. A sharp normalization lemma bounds the normal-direction error. An enlarged neighborhood permits transfer of the inactive operand's bound between the approximate witness and the true foot point. Under the stated analytic and domain assumptions, passing the checks identifies a true point on the union boundary and bounds distance deficiency by the active operand's pointwise value error. Failed or unavailable checks return Unknown. The argument extends to finite hard unions by testing every inactive operand. An executable proof-chain audit finds no violations on 75,738 certified samples. A broader analytic stress test covers spheres, capsules, ring tori, three Boolean operators, and a four-leaf union. Of 96,000 narrow-band samples, 87,469 pass with zero oracle violations; per-case coverage ranges from 72.67% to 98.30%. Removing visibility admits 75 truly invalid witnesses, showing that branch separation alone is insufficient. Non-union cases remain empirical tests, not new theorems.