Foundation Primitive Recognition Calculus Formal System Formal System Certificat

The certificate

A formal system is a set of rules for writing and transforming expressions. The certificate at issue here establishes a precise interface between such a system and a simpler structure called the primitive recognition calculus (PRC). The PRC is the minimal ledger: a discrete record of events, each event being one of two distinguishable endpoints, left or right, with finite traces of those events as its expressions. The certificate proves that if any formal system can distinguish those two endpoints, then that system can faithfully represent the PRC's structure. This is a theorem, checked by a machine, not a philosophical assertion.

The theorem's content is a guarantee of expressiveness. It says that any formal system meeting a single, plain condition, that it can tell the two endpoints apart, can embed the PRC. The embedding preserves two things: the distinction between the endpoints and the relation of one trace extending another. The proof is constructive: given a formal system with the required distinguishing power, the certificate explicitly builds the embedding. It does so by mapping each PRC endpoint to its corresponding token in the formal system and each finite trace to an expression, using the system's own structure. The result is that the PRC's basic operations are representable inside the larger system without loss.

In Recognition Science, this certificate is a step in a larger program. The framework models reality as a ledger of recognition events, and the PRC is the minimal such ledger. The certificate shows that this minimal ledger is not an isolated construct: it can live inside any formal system that meets the expressiveness condition. This matters because it means the PRC's structure, and whatever follows from it, is portable across formal settings. The certificate is not a claim about any particular external foundation, such as set theory or type theory; it is a claim about the interface any such foundation must satisfy to host the PRC.

The certificate explicitly does not claim that every external foundation does satisfy this interface. That broader claim is named as the next layer of work, not hidden inside this theorem. The certificate also does not claim that the PRC is the only formal system, nor that its two-endpoint structure is the only possible primitive distinction. It establishes a conditional: if a formal system can distinguish the endpoints, then it can embed the PRC. The proof is complete for that conditional, and the certificate's strength tag records that it is a delta-only step, meaning it is one specific, closed piece of a larger build order.

What a reader can now see is a precise, machine-checked statement of what it takes for a formal system to host the primitive recognition calculus. The condition is minimal: distinguish two endpoints. The payoff is a faithful embedding. This is the kind of exact claim that lets a larger framework proceed without hand-waving about formalization.

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

/-- Step 12 certificate: the formal-system surface and embedding theorem are
closed. The broader claim that every external foundation satisfies this
interface is the next inevitability layer, not hidden here. -/
structure FormalSystemCertificate : Prop where
  formal_system_surface : Nonempty FormalSystem
  prc_system_expressive : PRCFormalSystem.Expressive
  prc_system_embedding : Nonempty (PRCEmbeddingInto PRCFormalSystem)
  embedding_target : FormalSystemEmbeddingTarget
  embedding_from_expressive :
    ∀ F : FormalSystem, F.Expressive → Nonempty (PRCEmbeddingInto F)
  strength_tag : StrengthTag.deltaOnly = StrengthTag.deltaOnly

What this page does not claim

The certificate does not prove that any particular external foundation, such as set theory or type theory, satisfies the expressiveness condition. The certificate does not claim that the two-endpoint structure is the only possible primitive distinction for a formal system. The certificate does not establish any empirical or physical claims about the actual universe.

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: