Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Inevitability

show as:
view Lean formalization →

Defines the admissible-foundation interface for the first Primitive Recognition Calculus inevitability theorem: a formal system must be expressive enough to separate the two endpoints of the elementary distinction δ. Downstream Kernel and RecognizerBridge import this package to state that any such foundation already embeds the PRC kernel. The module is mostly structure and certificates rather than a single deep proof.

claimAn admissible foundation $F$ is a formal system rich enough to distinguish the two endpoints of the elementary distinction $\delta$. The module packages the inevitability target, the embedding of the PRC admissible foundation into any such $F$, and a certificate object asserting that inevitability holds for that class of foundations.

background

Primitive Recognition Calculus (PRC) is the foundational layer of Recognition Science: before costs, ladders, or forcing (T0–T8), one needs a minimal formal account of recognition as distinction. The imported FormalSystem module supplies the ambient notion of a formal system in which such distinctions can be stated.

The elementary distinction $\delta$ has two endpoints; any foundation that cannot tell them apart is too weak to host a recognition calculus. This module therefore isolates admissibility as expressiveness sufficient to separate those endpoints, rather than as a laundry list of logical axioms.

Sibling structures name the inevitability target, the PRC-admissible foundation, its embedding into an arbitrary admissible $F$, and external parsing targets used when comparing outside foundations to the PRC kernel.

proof idea

Definition-and-interface module, not a single monolithic proof. It introduces admissible foundations, the inevitability target proposition, and embedding/certificate structures. The substantive claim that any foundation presupposes distinction, and that the PRC admissible foundation embeds into every admissible $F$, is packaged here for Kernel and RecognizerBridge to consume; detailed derivations live in those dependents or in FormalSystem lemmas.

why it matters in Recognition Science

Inevitability is the claim that PRC is not an optional formalism but what any foundation capable of hosting recognition must already contain. This module is the gate: Kernel and RecognizerBridge import it to attach the PRC kernel and the recognizer bridge to a precise admissibility hypothesis.

In the broader RS forcing chain, that matters because later uniqueness results (J-cost, $\varphi$, eight-tick octave, $D=3$) sit on a recognition substrate. If every admissible foundation already embeds PRC, those later steps inherit a forced starting point rather than a free choice of logic. The certificate object is the portable witness downstream modules cite when closing the first inevitability theorem.

scope and limits

used by (2)

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 (8)