k=n+8; s=floor_sqrt(2*2^(2*k))/2^k; L=Log2Partial(k); t=L/s; u=ExpPartial(t,k+2). trace witnesses these actual computations; (up-um)/ud=u. No error bound is assumed.
Proposed arity: 5. Parameters: n up um ud trace. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.