Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Inevitability

show as:
view Lean formalization →

Defines admissible foundations for the first inevitability theorem in Primitive Recognition Calculus: formal systems expressive enough to distinguish the two endpoints of the elementary defect δ. Introduces the inevitability target, embedding of the PRC foundation, and a certificate that any such foundation already presupposes distinction. Cited by the PRC kernel and the recognizer bridge. Mostly interface and certificate packaging rather than deep calculation.

claimAn admissible foundation is a formal system rich enough to separate the two endpoints of the elementary defect $\delta$. The module packages the inevitability target, the claim that any such foundation presupposes distinction, the embedding of the PRC admissible foundation, and a certificate object witnessing that packaging.

background

Primitive Recognition Calculus (PRC) is the foundation layer that treats recognition, distinction, and cost before ordinary physical postulates. The imported FormalSystem module supplies the ambient notion of a formal system in which those primitives are stated.

The elementary defect $\delta$ has two endpoints; distinguishing them is the minimal act of recognition. An admissible foundation, in the sense of this module, is any formal system expressive enough to make that distinction. The module then records that this requirement is not optional: any foundation used to host the first inevitability theorem already presupposes distinction.

Sibling names mark the main objects: the admissibility predicate, the inevitability target, the embedding of the PRC foundation into that class, external parsing targets, and a certificate bundling the inevitability claim.

proof idea

Definition-and-certificate module rather than a long calculation. It introduces the admissibility interface (formal systems that can distinguish the endpoints of $\delta$), states the inevitability target, records that any foundation in that class presupposes distinction, and packages an embedding plus a certificate object for downstream use. Substantive forcing and kernel arguments live in the modules that import this one.

why it matters in Recognition Science

Sits at the entry of the PRC inevitability chain: before one can force J-cost uniqueness, $\phi$, the eight-tick octave, or $D=3$ (T5–T8 in the unified forcing chain), one must fix what counts as a legal host theory. This module supplies that host class and the claim that distinction is already presupposed.

It is imported by the PRC Kernel and by RecognizerBridge, which connect the abstract inevitability packaging to the working recognizer and kernel theorems. Without an explicit admissibility and certificate layer, later inevitability results would float free of any stated foundation class.

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)