Foundation Primitive Recognition Calculus Inevitability Prcinevitability Target

The inevitability target

In mathematics, a formal system is a set of symbols and rules for manipulating them. A primitive recognition calculus (PRC) is a minimal such system built around a single act: telling two distinct things apart. The declaration PRCInevitabilityTarget states a precise claim about formal systems: every admissible foundation, meaning every formal system expressive enough to distinguish two endpoints, contains an embedding of the PRC. The machine-checked library of formal theorems proves this claim for any system meeting that admissibility condition.

The proof is short and direct. Given any formal system that can distinguish two endpoints, the theorem constructs the required embedding. The library also shows the PRC itself qualifies as an admissible foundation, so the result applies to its own system. A certificate structure bundles these facts together, marking the admissible-interface theorem as closed.

The declaration does not claim that every conceivable foundation satisfies the condition. A separate target schema handles external foundations: for the inevitability theorem to apply to some external object, that object must first be parsed into an expressive formal system through a faithful-parse relation. The library names this as an open workload, not a proved result. The theorem's reach is therefore conditional on that parsing step being completed for any given external system.

What this establishes in plain terms: if you have a formal system that can tell two things apart, then within that system you already have the primitive recognition calculus. The framework's library proves this as a theorem, not as an assumption. What remains open is whether any particular external foundation, such as a specific logic or type theory, satisfies the parsing condition that would bring it under the theorem's scope.

/-- The exact first inevitability target. -/
def PRCInevitabilityTarget : Prop :=
  ∀ A : AdmissibleFoundation, Nonempty (PRCEmbeddingInto A.system)

/-- 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

theorem PRCAdmissibleFoundation_embeds :
    Nonempty (PRCEmbeddingInto PRCAdmissibleFoundation.system) :=
  any_foundation_presupposes_distinction PRCAdmissibleFoundation

What this page does not claim

The theorem does not claim that every conceivable foundation satisfies the admissibility condition. The theorem does not prove that any particular external foundation, such as a specific logic or type theory, has been parsed into an expressive formal system. The declaration does not claim that the primitive recognition calculus is the only possible minimal formal system.

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: