sign_indist_3_5
plain-language theorem explainer
The declaration shows that 3 and 5 produce the same recognition event under the sign recognizer on the integers. Researchers building concrete examples in recognition geometry cite it to demonstrate the three-class partition of ℤ. The proof is a one-line simp wrapper that reduces the claim by unfolding the recognizer and indistinguishability definitions.
Claim. Under the sign recognizer on the integers, $3$ and $5$ are indistinguishable: they map to the same recognition event.
background
The Recognition Geometry module supplies concrete examples to illustrate the framework. The sign recognizer on ℤ is built from the sign function that assigns negative, zero, or positive. Indistinguishable is defined as the relation where two configurations produce identical events under a recognizer. The module documentation states that the sign recognizer yields exactly three equivalence classes on ℤ.
proof idea
This is a one-line simp wrapper. It unfolds the definitions of Indistinguishable, signRecognizer, and signOf, reducing the goal to equality of the positive sign for both 3 and 5.
why it matters
The result feeds the examples_status definition, which records that the sign recognizer partitions ℤ into three classes and that sign combined with magnitude refines distinctions. It supplies the concrete illustration of the three-class partition noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.