Binary Name Comparison

Abstract

Comparison of whole binary names includes length mismatch and paid restoration.

Theorem 1.1 (Restored operands, empty backups and preserved caller frame).

$$\forall a\in \mathrm{List}\left(Bool\right),\forall b\in \mathrm{List}\left(Bool\right),\forall output\in \mathrm{List}\left(Bool\right),\forall frame\in \mathrm{List}\left(Bool\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(compareMachine\right),\mathrm{compareCfg}\left(\mathrm{some}\left(compare\right),(none,none,true),a,b,nil,nil,output,frame\right),\mathrm{some}\left(\mathrm{compareCfg}\left(none,(none,none,true),a,b,nil,nil,\mathrm{cons}\left(\mathrm{decide}\left(a=b\right),output\right),frame\right)\right),2\cdot \left(\mathrm{length}\left(a\right)+\mathrm{length}\left(b\right)\right)+4\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Computability/BinaryNameComparison.name_compare_run (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary Boolean words a and b, previous output and caller frame, the six-stack, four-label machine consumes both operands into backups, including unequal lengths. It restores each operand, empties both backups, pushes their whole-word equality flag onto the previous output and returns with its initial control. The caller frame is preserved literally.

The native transition bound is twice the sum of the operand lengths plus four. Only symbol comparisons occur; binary names are never expanded into unary numbers. This is a routine boundary with restored operands, rather than the clean haltList boundary of the complete converter.

References

• Truth anchor: D5/S0/Computability/BinaryNameComparison.name_compare_run