examples_status
plain-language theorem explainer
examples_status assembles a fixed string reporting completion status for discrete recognition on finite sets, sign and magnitude recognizers on integers, and their composition. Researchers auditing Recognition Geometry examples cite it to confirm the listed properties hold. The body is a static concatenation of text blocks with no computation or lemma calls.
Claim. A status string for recognition geometry examples is the concatenation of messages confirming: discrete recognition on finite sets (indistinguishable iff equal, singleton cells); sign recognizer on integers (same sign iff indistinguishable); magnitude recognizer on integers (same absolute value iff indistinguishable); and composition of sign with magnitude refining distinctions.
background
The module develops concrete recognition geometries to illustrate the framework. Discrete recognition on Fin n yields a quotient isomorphic to the original space. The sign recognizer on integers partitions into three classes (negative, zero, positive). The magnitude recognizer partitions into classes indexed by absolute value, with infinitely many classes.
proof idea
The definition is a direct string concatenation of fixed text blocks. No lemmas or tactics are applied; it is a static definition of the status report.
why it matters
This definition summarizes the examples that demonstrate the composition principle: neither sign nor magnitude alone distinguishes all nonzero integer pairs, but together they do. It supports the module's physical interpretation that discrete cases model eigenvalue detection and observables act as recognizers. It closes the examples section without recorded downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.