Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy

show as:
view Lean formalization →

In Primitive Recognition Calculus, every foundation is either degenerate (discrimination relation empty) or discriminating (can separate some pair of objects). The module proves the dichotomy, links discrimination to realizing a nonzero distinction, and shows named foundations (set theory, type theory, category theory, ZFC) are non-degenerate. Downstream parse and certificate modules cite it to rule out empty discrimination.

claimA foundation is degenerate when its discrimination relation is empty (no two objects are told apart). It is discriminating when some pair is separated. These are complementary: non-degenerate iff discriminating. Discriminating foundations realize a nonzero distinction $\Delta$; realizing $\Delta$ implies non-degeneracy. Hence distinction is not optional for any foundation that can express two distinct objects, and the named formal systems are non-degenerate.

background

Primitive Recognition Calculus treats a foundation as a formal system equipped with a discrimination relation on expressions or objects: the relation records which pairs the system can tell apart. Degeneracy means that relation is empty; the system cannot separate any two objects. Discrimination is the complementary property that at least one pair is separated.

The module sits on the inevitability instances layer: once a system can host two distinct expressions (or an explicit two-object witness), reflexivity and distinction structure become available. Related notions include expression-reflexivity (the system can refer to its own expressions) and realizing $\Delta$ (witnessing a nonzero distinction in the PRC sense).

The local claim is structural, not computational: either the discrimination relation is empty, or the foundation already carries enough distinction to feed later parse and certificate arguments.

proof idea

Definitions introduce Degenerate, Discriminating, ExprReflexive, and RealizesDelta. Equivalence lemmas show non-degenerate iff discriminating, that discriminating systems realize $\Delta$, and that realizing $\Delta$ implies non-degeneracy. The main dichotomy packages these into a single alternative. A short chain then shows distinction is not optional once two distinct objects exist, that PRC formal systems and two-distinct witnesses are expression-reflexive, and that the named foundations are non-degenerate by exhibiting discrimination (or by the two-object witness).

why it matters in Recognition Science

Recognition Science needs foundations that actually distinguish structure; an empty discrimination relation cannot support the forcing chain, RCL, or later physics extraction. This module supplies the dichotomy and the non-degeneracy facts used by the parse layers: category-theory, set-theory, type-theory, and full ZFC parses import it, as does the shrunk certificate path. Those consumers treat non-degeneracy as a gate: only discriminating foundations proceed into PRC readings of standard mathematics. The result is foundational hygiene rather than a new physical constant: it closes the loophole that a "foundation" might name objects yet distinguish nothing.

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)