Foundation Primitive Recognition Calculus Prccategory Theory Parse

The categorical foundation

Category theory is a branch of mathematics that studies structures through the arrows, or morphisms, between them. One of its central objects is the topos of sets, a universe where sets are the objects and functions are the arrows. In this universe, a special object called the subobject classifier plays the role of a truth-value selector: it distinguishes the parts of a set from the whole. In the topos of sets, this classifier is simply the type of truth values, with two global points: truth and falsity.

The module in question, PRCCategoryTheoryParse.lean, takes this classical categorical setup and shows that it satisfies the requirements of a more primitive framework. Recognition Science models reality as a ledger, a discrete record of events, where each event is a recognition of a distinction. The framework's foundational core, called the δ core, requires a system with at least two distinct tokens that can be told apart. The module proves that the topos of sets, with its two truth values, provides exactly such a system.

The key result is a formal theorem: the categorical foundation contains the δ core. This is established by constructing a mapping from the truth-value system into the framework's formal system, showing that the two truth values are distinct, and verifying that this system is not degenerate. In plain language, the module demonstrates that the basic machinery of category theory, specifically the distinction between true and false, is sufficient to instantiate the primitive recognition calculus. This is not a claim that category theory is the only foundation, but rather that it is one valid starting point.

Within the framework, this result is significant because it provides a bridge between a well-established mathematical discipline and the framework's own axioms. It shows that the framework's starting point, the need for distinct tokens, is not an arbitrary invention but a property shared by a classical mathematical structure. This connection allows the framework to draw on the extensive body of categorical results while maintaining its own distinct vocabulary of ledgers and recognition events.

/-- **The categorical foundation contains the δ core.** -/
theorem toposSystem_embeds_delta : Nonempty (PRCEmbeddingInto toposSystem) :=
  FormalSystemEmbeddingTarget_proved toposSystem toposSystem_expressive

/-- **Non-degeneracy.** The two truth values are distinct: ⊤ ≠ ⊥. A topos with
⊤ = ⊥ is degenerate (the terminal category, where 0 ≅ 1). -/
theorem top_ne_bot : (True : Omega) ≠ False := by
  intro h
  rw [eq_iff_iff] at h
  exact h.mp trivial

/-- The subobject classifier Ω of the topos of sets: the type of truth values. Its
two global points are truth and falsity. -/
abbrev Omega := Prop

What this page does not claim

This module does not claim that category theory is the only possible foundation for the recognition calculus. It does not derive any physical constants or empirical predictions. It does not prove that the topos of sets is equivalent to the full recognition calculus, only that it contains its core.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCategoryTheoryParse.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: