Foundation Primitive Recognition Calculus Formal System

The formal system interface

A formal system is a language with fixed rules for building and comparing expressions. In mathematics, familiar examples include first-order logic, type theory, and the grammar of arithmetic. Each has tokens, the smallest meaningful symbols, and expressions, the larger statements built from them. The framework's foundation module defines this idea abstractly, then proves a structural fact about it.

The definition is deliberately spare. A formal system has a type of tokens, a type of expressions, a relation that says when one token distinguishes another, and a relation that says when one expression extends another. The only requirement is that extending a trace, a finite sequence of recognition events, must be preserved when traces are mapped into expressions. This is the minimal interface the framework's inevitability theorem needs.

Within this interface, the framework constructs its own minimal calculus, the primitive recognition calculus. Its tokens are the two endpoints of a primitive distinction, its expressions are finite traces, and its distinction relation is simple inequality. The framework proves this calculus is expressive: it can distinguish its two endpoint tokens. It then proves the embedding target: any formal system that can distinguish two endpoints admits an embedding of the primitive calculus that preserves both distinction and extension.

The module closes with a certificate bundling these results. The certificate records that the formal system surface is nonempty, the primitive calculus is expressive, the embedding theorem holds, and the strength tag is deltaOnly. This is a machine-checked theorem in the framework's library, not a claim about every conceivable foundation. The docstring is explicit: the broader claim that every external foundation satisfies this interface is the next inevitability layer, not hidden here.

What this establishes in plain language is a bridge. The framework's most primitive structure, a record of two distinguishable events and their finite extensions, can be represented inside any formal system that has at least that much expressive power. The bridge is one-way and conditional: it requires the target system to distinguish two tokens. Where that condition holds, the primitive calculus's structure is preserved, which is what later inevitability arguments build on.

theorem FormalSystemEmbeddingTarget_proved :
    FormalSystemEmbeddingTarget := by
  intro F hF
  exact ⟨PRCEmbeddingInto.ofExpressive F hF⟩

theorem PRCFormalSystem_expressive :
    PRCFormalSystem.Expressive := by
  exact Endpoint.left_ne_right

theorem formal_system_certificate : FormalSystemCertificate where
  formal_system_surface := ⟨PRCFormalSystem⟩
  prc_system_expressive := PRCFormalSystem_expressive
  prc_system_embedding := PRCFormalSystem_embedding
  embedding_target := FormalSystemEmbeddingTarget_proved
  embedding_from_expressive := FormalSystemEmbeddingTarget_proved
  strength_tag := rfl

What this page does not claim

No claim that every conceivable formal system satisfies the interface; the certificate explicitly leaves that to the next layer. No claim that the primitive recognition calculus is the only formal system, only that it embeds into any expressive one. No claim about what the embedding theorem implies for physics; that connection is not established in this module.

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