Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCFoundationsParsed

show as:
view Lean formalization →

Aggregates the three classical foundations (set theory, type theory, category theory) after each is parsed into the FormalSystem interface. Each admits a Primitive Recognition Calculus embedding that realizes the δ core via its own distinction mechanism. Anyone comparing foundational systems under PRC cites the package theorems here. The module is a thin re-export and conjunction layer over the four parse submodules.

claimSet theory, type theory, and category theory, each parsed as a formal system with its native distinction mechanism, each admit a PRC embedding realizing the $\delta$ core. In particular the three foundations jointly realize $\delta$, are non-degenerate, and own their distinctions; set theory with Infinity also realizes $\delta$.

background

Primitive Recognition Calculus (PRC) treats a formal system through a distinction mechanism and asks whether that system embeds into a recognition core whose generator is the cost defect $\delta$. The ambient interface is FormalSystem: a carrier of judgments together with a distinguished relation that plays the role of "this differs from that."

Four sibling parse modules supply the concrete embeddings. Set theory (with and without a full ZFC package) uses membership and separation as distinction. Type theory uses inhabitation and judgmental equality. Category theory uses morphisms and the failure of two arrows to coincide. Each parse produces a PRC embedding candidate.

This module sits one level above those parses. It does not redefine the embeddings; it packages the claim that all three named foundations realize $\delta$, are non-degenerate under the embedding, and own their distinctions internally.

proof idea

Definition-and-aggregation module, not a single proof. It imports the four parse modules (set theory, full ZFC, type theory, category theory) and exposes conjunction-style theorems: the three foundations realize $\delta$; they are non-degenerate; each owns its distinction; and set theory with Infinity realizes $\delta$. Each such statement is discharged by applying the corresponding embedding lemmas already proved in the parse submodules, then packaging the three (or four) witnesses.

why it matters in Recognition Science

In the Recognition Science foundation layer, physics is forced from a single functional equation only after the logical substrate is shown not to smuggle structure. Showing that the three standard foundations each realize the same $\delta$ core means the forcing chain (T0–T8), including J-uniqueness and the eight-tick octave, does not depend on a partisan choice of set theory versus type theory versus categories.

Downstream consumers are any theorems that quantify over "any foundation that realizes $\delta$" or that compare distinction mechanisms across foundations. The sibling package results (three_foundations_realize_delta, non-degeneracy, own-distinction, and the Infinity variant) are the citation surface. No further used-by edges are recorded at this module boundary; the module is the aggregation point itself.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (4)