Foundation Primitive Recognition Calculus Inevitability Admissible Foundation

The admissible foundation

In formal logic, a formal system is a set of symbols and rules for manipulating them. A system is expressive when it can represent a distinction, meaning it can tell two different things apart. The Recognition Science declaration AdmissibleFoundation packages exactly this idea: it is a formal system together with a proof that the system is expressive. The declaration itself is a definition, a choice of vocabulary, not a discovery.

The framework's machine-checked library of formal theorems then proves a striking consequence: any admissible foundation already contains a copy of the primitive recognition calculus (PRC), the framework's basic ledger of events. The theorem, named any_foundation_presupposes_distinction, states that for every admissible foundation A, there exists an embedding of PRC into A's system. The proof is short: because A is expressive, it can distinguish two endpoints, and that ability is exactly what PRC needs to operate. In plain language, any system that can tell two things apart can already simulate the framework's primitive ledger.

This is a theorem about formal systems, proved in the library. It does not claim that every formal system in existence has been checked. The theorem applies to any foundation that has already been parsed into the admissible interface, meaning it has been shown to be expressive. The work of checking that external foundations, such as the axioms of set theory or the rules of a programming language, actually satisfy this expressiveness condition is a separate target, named ExternalFoundationParsingTarget. That parsing workload is explicitly not hidden inside the theorem; it is left as an open task.

The declaration also includes a certificate, PRCInevitabilityCertificate, which bundles the theorem and its targets into a single object. This certificate is a way of saying: here is the closed theorem, and here is the separate, named workload for external foundations. The certificate itself is a theorem, proved in the library, that the admissible-interface theorem is closed and the external parsing workload is named separately. This separation is a deliberate design choice: it keeps the proved part clean and the unproved part visible.

What this means for a reader is that the framework's claim of inevitability is conditional. The condition is expressiveness. If a system can represent a distinction, then PRC is already inside it. If a system cannot, the theorem does not apply. The framework does not claim to have surveyed all possible foundations; it claims to have proved a conditional statement about any foundation that meets its one condition.

/-- An admissible foundation for the first inevitability theorem is a formal
system that is expressive enough to distinguish the two endpoints of δ. -/
structure AdmissibleFoundation where
  system : FormalSystem
  expressive : system.Expressive

/-- Any foundation already parsed into the admissible interface presupposes a
PRC trace core. -/
theorem any_foundation_presupposes_distinction :
    PRCInevitabilityTarget := by
  intro A
  exact FormalSystemEmbeddingTarget_proved A.system A.expressive

/-- Any foundation already parsed into the admissible interface presupposes a
PRC trace core. -/
theorem any_foundation_presupposes_distinction :
    PRCInevitabilityTarget := by
  intro A
  exact FormalSystemEmbeddingTarget_proved A.system A.expressive

/-- The exact remaining external parsing target schema: once a corpus of
external foundations and a faithful-parse relation are fixed, every external
object in that corpus must parse to an expressive formal system before the
inevitability theorem applies to it. -/
def ExternalFoundationParsingTarget
    (ExternalFoundation : Type)
    (FaithfulParse : ExternalFoundation → FormalSystem → Prop) : Prop :=
  ∀ E : ExternalFoundation,
    ∃ F : FormalSystem, FaithfulParse E F ∧ F.Expressive

theorem prc_inevitability_certificate :
    PRCInevitabilityCertificate where
  admissible_foundation_surface := ⟨PRCAdmissibleFoundation⟩
  prc_admissible := ⟨PRCAdmissibleFoundation⟩
  inevitability_target := any_foundation_presupposes_distinction
  any_foundation_embedding := any_foundation_presupposes_distinction
  prc_embedding := PRCAdmissibleFoundation_embeds
  external_parsing_target_schema := by
    intro ExternalFoundation FaithfulParse
    rfl
  strength_tag := rfl

What this page does not claim

The theorem does not claim that every formal system in existence has been checked for expressiveness. The declaration does not prove that the primitive recognition calculus is the only possible formal system. The certificate does not establish that any specific external foundation, such as set theory, satisfies the expressiveness condition.

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/Inevitability.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: