“I know (or could readily rediscover) how to build a binary adder from logic gates. If I can figure out how to make individual logic gates from Legos or ant trails or rolling ping-pong balls, then I can add two 32-bit unsigned integers using Legos or ant trails or ping-pong balls.”
To me this sounds pretty much like a domain error. Your ‘theoretical’ binary adder, is a function of Binary x Binary → Binary x Binary. Your Lego adder has a different domain, it’s function is: Lego x Universe\Lego → Lego x Universe\Lego
Now you need a tranformation from Lego x Universe\Lego → Binary x Binary, so you can check whether they are doing the same operation, addition that is.
Now, if you’re saying they are doing the same kind of addition, then I can show you a counter-example by just destroying the Lego adder before it mechanically ends its ‘addition’ (remember I am part of Universe\Lego!).
You’ve got two choices: Either the Lego adder is not doing ‘addition’, or your assumption what ‘addition’ is, is wrong.
“I know (or could readily rediscover) how to build a binary adder from logic gates. If I can figure out how to make individual logic gates from Legos or ant trails or rolling ping-pong balls, then I can add two 32-bit unsigned integers using Legos or ant trails or ping-pong balls.”
To me this sounds pretty much like a domain error. Your ‘theoretical’ binary adder, is a function of Binary x Binary → Binary x Binary. Your Lego adder has a different domain, it’s function is: Lego x Universe\Lego → Lego x Universe\Lego
Now you need a tranformation from Lego x Universe\Lego → Binary x Binary, so you can check whether they are doing the same operation, addition that is.
Now, if you’re saying they are doing the same kind of addition, then I can show you a counter-example by just destroying the Lego adder before it mechanically ends its ‘addition’ (remember I am part of Universe\Lego!). You’ve got two choices: Either the Lego adder is not doing ‘addition’, or your assumption what ‘addition’ is, is wrong.