neg_pos_dist
plain-language theorem explainer
The theorem shows that -1 and 1 map to distinct events under the sign recognizer on the integers and are therefore distinguishable. Model builders working with concrete recognition geometries cite it to verify that the sign partition yields exactly three classes. The proof is a one-line simplification that unfolds the recognizer and sign function definitions.
Claim. Under the sign recognizer on the integers, the configurations $-1$ and $1$ are distinguishable: they do not satisfy $r.R(-1) = r.R(1)$ where $r$ is the sign recognizer.
background
The sign recognizer on the integers is built from the sign function that sends each integer to one of three events: negative, zero, or positive. Indistinguishable configurations are those that produce identical recognition events under a given recognizer. The module develops concrete examples of recognition geometries, including the sign recognizer whose quotient consists of exactly three classes and the magnitude recognizer whose classes are the absolute values.
proof idea
The proof is a one-line wrapper that applies simplification to the definitions of Indistinguishable, signRecognizer, and signOf. This immediately shows that the sign events for -1 and 1 differ.
why it matters
The result confirms that the sign recognizer separates positive and negative integers, feeding directly into the examples_status definition that illustrates the composition principle with the magnitude recognizer. It supports the framework's construction of recognizers that induce nontrivial partitions on the integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.