neg_indist
plain-language theorem explainer
The theorem shows that -5 and -3 are indistinguishable under the sign recognizer on the integers because both map to the negative label. Researchers building concrete examples of recognition geometries cite this to confirm the sign recognizer partitions the integers into three equivalence classes. The proof is a direct simplification that unfolds the definitions of indistinguishability, the sign recognizer, and the sign function to verify label equality.
Claim. Under the sign recognizer on the integers, which assigns each integer to one of three classes (negative, zero, positive), the configurations -5 and -3 are indistinguishable because they share the negative class: the recognizer produces identical events for both.
background
The module supplies concrete recognition geometries to illustrate the framework. The sign recognizer on the integers is defined by the sign function that returns negative for inputs less than zero, zero for exactly zero, and positive otherwise. Indistinguishability holds between two configurations exactly when they produce the same event under a given recognizer, forming the fundamental equivalence relation of recognition geometry.
proof idea
The proof is a one-line wrapper that applies simplification using the definitions of indistinguishability, the sign recognizer, and the sign function. Unfolding these definitions immediately shows that both -5 and -3 receive the negative label, so the produced events are equal.
why it matters
This result feeds the examples_status definition that summarizes the module's recognition geometries. It illustrates the sign recognizer's three-class partition and supports the composition principle that sign and magnitude together refine distinctions for nonzero integers. In the Recognition Science setting the example aligns with the development of recognizers that induce equivalence classes from shared events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.