value=2*sum(j<K,1/((2*j+1)*3^(2*j+1))) by a rational fold trace; no limit or inverse-exponential assertion is part of the definition.
Proposed arity: 3. Parameters: K value trace. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.