[aidenn0]

Looks like it's a typo; they state:

> 0x47c35000 encodes 10000.0

But by my math that encodes 100000.0 (note the extra zero).