pow=2^k by the existing Pow graph, and integer-square-root trace establishes z²<=2*pow²<(z+1)². Bracket endpoints z/pow and (z+1)/pow.
Proposed arity: 4. Parameters: k z pow trace. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.