Omega
plain-language theorem explainer
Ω is identified with Prop, the subobject classifier of the topos of sets: the type of truth values whose global points are true and false. Category-theory parses of the primitive recognition calculus cite this as the token type for discrimination. The declaration is a one-line abbreviation, not a proved statement.
Claim. Write $\Omega := \mathrm{Prop}$ for the subobject classifier of $\mathbf{Set}$: the type of truth values. Its two global points are $\top$ (truth) and $\bot$ (falsity).
background
In the topos of sets, the subobject classifier $\Omega$ is the object of truth values. Subobjects of the terminal object $1$ (here Unit) are predicates $1 \to \Omega$, and global points of $\Omega$ are exactly the truth values true and false.
This module parses a category-theoretic foundation into the FormalSystem interface used by the primitive recognition calculus. Tokens are global points of $\Omega$; discrimination is inequality of truth values; the endpoints are $\top$ and $\bot$. The local goal is to show that this parse realizes the $\delta$ core (non-degenerate two-point discrimination).
Upstream material supplies continuum and analytic value machinery elsewhere in the foundation stack; here only the elementary identification $\Omega = \mathrm{Prop}$ is needed.
proof idea
One-line abbreviation: $\Omega$ is defined to be Lean's Prop. No tactics, no lemmas. Downstream maps (subobject classification, non-degeneracy) treat True and False as the two global points of this classifier.
why it matters
This abbreviation is the token carrier for the categorical parse of the primitive recognition calculus. It feeds subobjectClassification (bijection between predicates on the terminal object and points of $\Omega$), top_ne_bot (non-degeneracy $\top \neq \bot$), and toposSystem (the FormalSystem whose tokens are points of $\Omega$).
The packaged theorem category_theory_realizes_delta assembles those facts: classification of top and bottom, distinct truth values, and a nonempty embedding of the $\delta$ core into the topos system. In Recognition Science terms this is the elementary categorical witness that a two-point discrimination structure exists before any forcing-chain or continuum construction is invoked.
Peripheral uses in gravity modules (spectral density notation) reuse the name $\Omega$ as a frequency variable and are not part of this foundation parse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.