Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy

show as:
view Lean formalization →

Defines the degenerate/discriminating split for Primitive Recognition Calculus foundations: a foundation is degenerate when its discrimination relation is empty, and discriminating otherwise. Proves the two are complementary, that discrimination realizes a nonzero distinction, and that distinction is not optional. Downstream foundation parsers and the shrunk certificate import this dichotomy. The argument is mostly definitional with short equivalence lemmas.

claimA foundation is degenerate when its discrimination relation is empty (it cannot tell any two objects apart). It is discriminating when that relation is nonempty. These are complementary: not degenerate iff discriminating. Any discriminating foundation realizes a nonzero distinction $\Delta$, and conversely realizing $\Delta$ rules out degeneracy. Distinction is therefore not optional for any non-degenerate foundation; named foundations (set theory, type theory, category theory, ZFC) are shown non-degenerate once they admit two distinct objects or expression reflexivity.

background

Primitive Recognition Calculus (PRC) treats a foundation as a formal system equipped with a discrimination relation on expressions or objects. The relation records when the system can tell two things apart. If that relation is empty, the foundation distinguishes nothing: every pair is indistinguishable from inside the system.

This module sits on the inevitability instances layer. It packages the elementary status predicates Degenerate and Discriminating, the witness RealizesDelta (the system exhibits a concrete nonzero distinction), and ExprReflexive (expression-level reflexivity used by named foundations). The local goal is a clean dichotomy: either the foundation is vacuous as a discriminator, or it already carries a distinction that later parsers can exploit.

Upstream, the inevitability instances supply the concrete PRC formal-system carriers against which these predicates are evaluated. No physics constants or J-cost structure appear here; the content is purely foundational status logic.

proof idea

The module is definition-heavy. Degenerate and Discriminating are complementary status predicates on a foundation's discrimination relation; their equivalence is the short lemma not_degenerate_iff_discriminating. RealizesDelta is linked one way by realizesDelta_of_discriminating and the converse direction by not_degenerate_of_realizesDelta, yielding the packaged dichotomy distinction_dichotomy and the slogan distinction_not_optional.

Separate lemmas record that a PRC formal system is expression-reflexive, that any carrier with two distinct objects is expression-reflexive, and that the named foundations are therefore not degenerate. Proofs are short propositional rewrites and instance discharge, not deep constructions.

why it matters in Recognition Science

Without a forced distinction, later claims that set theory, type theory, category theory, or full ZFC "parse" as PRC systems would be vacuous: a foundation that distinguishes nothing cannot underwrite recognition structure. This module supplies that gate.

It is imported by PRCSetTheoryParse, PRCTypeTheoryParse, PRCCategoryTheoryParse, PRCFullZFCParse, and PRCShrunkCertificate. Those modules use the dichotomy and the named-foundations non-degeneracy facts to certify that standard foundations already realize distinction, so the PRC reading is not optional scaffolding. In the broader Recognition chain this is pre-physics foundation hygiene: it ensures the formal substrate can host discrimination before forcing steps (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3) are interpreted on top of it.

scope and limits

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)