recognizer_status
plain-language theorem explainer
The recognizer_status definition assembles a fixed string that reports completion of the recognition map structures under axiom RG2. Researchers auditing the Recognition Geometry layer would reference it to confirm that recognizers, local recognizers, and fiber partitions have been declared. The definition is a direct string concatenation with no computation or lemma applications.
Claim. The module status string is the concatenation of messages verifying the recognizer structure, the local recognizer combining locality and recognition, enforcement of nontriviality, local image and fiber definitions, the fiber partition theorem, and event realization, ending with the declaration that recognition maps under RG2 are complete.
background
In this module a recognizer is a function R from a configuration space C to an event space E such that the image of R contains at least two distinct elements. The LocalRecognizer structure extends a local configuration space with this recognizer property. The Fiber definition from the probability module supplies the set of underlying states that project to a given outcome value, and the partition property states that every state belongs to exactly one such fiber.
proof idea
This is a definition that constructs the string value by direct concatenation of literal messages. No lemmas from the upstream list are invoked; the construction is a static literal assembly.
why it matters
The definition closes the Recognition Maps (RG2) module by supplying a readable confirmation that the required structures exist. It documents the implementation of the axiom that at least one nontrivial recognizer maps configurations to events, consistent with the module's statement that configurations are what the world does and events are what recognizers see. No parent theorems or open questions are referenced in the downstream results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.