IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FormalSystem
Defines the minimal formal-system interface that the Primitive Recognition Calculus (PRC) inevitability theorem needs: token and expression carriers, plus the distinguishability and extension relations that make the recognition defect δ visible inside an arbitrary formal system. Downstream inevitability and kernel modules import this interface to state embedding and expressiveness claims. The module is definitional scaffolding rather than a proof package.
claimA formal system $F$ is given by carriers $\mathrm{Token}$ and $\mathrm{Expr}$, together with relations $\mathrm{distinguishes}$ and $\mathrm{exprExtends}$ that record when expressions separate tokens and when one expression extends another, so that the recognition defect $\delta$ is interpretable inside $F$. Expressiveness and PRC-embedding predicates then assert that $F$ can host the PRC structure.
background
Primitive Recognition Calculus (PRC) argues that any sufficiently expressive formal system must already contain the recognition defect structure that forces the RS cost $J$ and the forcing chain. Before inevitability can be stated, one needs a thin, verifier-side interface for "what counts as a formal system" without committing to a particular syntax (type theory, set theory, etc.).
This module supplies that interface. Token and Expr are abstract carriers; distinguishes says when an expression separates two tokens; exprExtends records hierarchical extension of expressions. Together they make $\delta$ (the recognition defect) visible as a formal relation rather than a metatheoretic aside. The upstream import is TraceLogic, which supplies the trace-level logical substrate on which these carriers sit.
Sibling definitions package the interface into a structure FormalSystem, predicates Expressive and PRCEmbeddingInto, a concrete PRC instance PRCFormalSystem, and a certificate bundle used by later inevitability proofs.
proof idea
This is a definition module, not a proof package. It introduces the FormalSystem structure (token/expression carriers plus distinguish and extend relations), expressiveness and embedding predicates, a canonical PRC formal-system instance with its expressiveness and embedding witnesses, and a FormalSystemCertificate bundling those facts for downstream consumption. Any proved lemmas are thin wrappers assembling those witnesses; the mathematical content lives in the interface design.
why it matters in Recognition Science
Inevitability, Kernel, and PRCInevitabilityInstances all import this module. Without a shared formal-system interface, the claim that "any expressive system already contains PRC" cannot even be typed. The doc-comment states the purpose directly: the minimal interface needed by the PRC inevitability theorem, with distinguishes and exprExtends recording the structure that makes $\delta$ visible.
In the broader RS forcing picture this sits under Foundation: it is the logical front-end that lets inevitability connect an arbitrary formal system to the T5–T8 chain (unique $J$, $\varphi$, eight-tick octave, $D=3$) once expressiveness is assumed. The certificate object is the hand-off point for instance proofs in PRCInevitabilityInstances.
scope and limits
- Does not prove inevitability; only defines the interface inevitability consumes.
- Does not fix a concrete object language (no particular FOL, type theory, or set theory).
- Does not derive $J$, $\varphi$, or dimensional forcing; those live upstream in the forcing chain.
- Does not assert that every mathematical practice meets the Expressive predicate.
- Does not define the recognition defect $\delta$ itself; only the relations that host it.