IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCInevitabilityInstances
Concrete formal-system instances for Primitive Recognition Calculus: Boolean logic, Peano arithmetic, set foundations, and type theory, each shown to embed a two-element distinction. Anyone arguing that ordinary foundations already force recognition-level distinction cites this file. Content is mostly instance definitions plus short embedding and monotonicity lemmas, not a long derivation.
claimThe module assembles instances of formal systems that realize a two-element distinction $\Delta$: Boolean logic, Peano arithmetic, a set-theoretic foundation, and type theory. It also records that finite-trace length is monotone under trace extension, and that any two distinct carriers yield an expressive system embedding $\Delta$.
background
Primitive Recognition Calculus treats recognition as a formal system acting on finite traces. The imported FormalSystem layer supplies the abstract interface: carriers, distinction structure, expressiveness, and embeddings of a minimal two-point distinction $\Delta$.
This file does not redefine that interface. It populates it with standard mathematical foundations so later dichotomy theorems can name concrete witnesses rather than quantify over an empty class of systems.
Sibling material includes monotonicity of finite-trace length under extension, a generic construction from any two distinct elements, and named systems (boolLogicSystem, peanoSystem, setFoundationSystem, typeTheorySystem) with embedding lemmas into $\Delta$.
proof idea
Definition-and-instance module, not a single theorem proof. It builds concrete FormalSystem values for Boolean logic, Peano arithmetic, set foundations, and type theory, then discharges short lemmas that each system is expressive and embeds $\Delta$. A generic path constructs a system from any two distinct carriers. One auxiliary fact records that finite-trace length is monotone under trace extension. Downstream files import these witnesses rather than reprove existence.
why it matters in Recognition Science
Feeds PRCDistinctionDichotomy, which needs inhabited, named examples of formal systems that already carry a minimal distinction. Without these instances, inevitability claims about recognition-level dichotomy would float over an abstract class with no standard mathematical models.
In the Recognition Science foundation layer this closes the gap between the abstract PRC interface and everyday foundations (logic, arithmetic, sets, types). It supports the broader forcing narrative that distinction is not an optional extra: ordinary formal systems already realize $\Delta$, so later uniqueness and octave arguments can treat distinction as given rather than postulated ad hoc.
scope and limits
- Does not prove the distinction dichotomy itself; only supplies instances.
- Does not derive physics constants, J-uniqueness, or the eight-tick octave.
- Does not claim these embeddings are unique or universal among all formal systems.
- Does not analyze computational complexity or proof-theoretic strength of the systems.
- Does not replace the abstract FormalSystem interface; it only inhabits it.
used by (1)
depends on (1)
declarations in this module (14)
-
theorem
length_le_of_extends -
def
ofTwoDistinct -
theorem
ofTwoDistinct_expressive -
theorem
two_distinct_realizes_delta -
def
boolLogicSystem -
theorem
boolLogicSystem_expressive -
theorem
boolLogicSystem_embeds_delta -
def
peanoSystem -
theorem
peanoSystem_embeds_delta -
def
setFoundationSystem -
theorem
setFoundationSystem_embeds_delta -
def
typeTheorySystem -
theorem
typeTheorySystem_embeds_delta -
theorem
named_foundations_embed_delta