IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FormalSystem

   1/-
   2  PrimitiveRecognitionCalculus/FormalSystem.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 12: define expressivity and embeddings in enough
   9    generality to prove the inevitability surface.
  10
  11  This module is not claiming that every historical foundation has already
  12  been parsed into the interface. It closes the exact theorem-shaped interface:
  13  any formal system that supplies distinguishable endpoint tokens and preserves
  14  trace extension admits a PRC trace embedding.
  15-/
  16
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceLogic
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- Minimal formal-system interface needed by the PRC inevitability theorem.
  24`Token` and `Expr` are verifier-side carriers for an arbitrary formal system,
  25while `distinguishes` and `exprExtends` record the structure that makes δ
  26visible inside it. -/
  27structure FormalSystem where
  28  Token : Type
  29  Expr : Type
  30  distinguishes : Token → Token → Prop
  31  exprExtends : Expr → Expr → Prop
  32  endpointToken : Endpoint → Token
  33  traceExpr : Trace → Expr
  34  traceExpr_extends :
  35    ∀ {T U : Trace}, Trace.Extends T U → exprExtends (traceExpr T) (traceExpr U)
  36
  37namespace FormalSystem
  38
  39/-- A formal system is expressive for the first inevitability pass when it can
  40distinguish the two endpoints of the primitive distinction. -/
  41def Expressive (F : FormalSystem) : Prop :=
  42  F.distinguishes (F.endpointToken Endpoint.left) (F.endpointToken Endpoint.right)
  43
  44end FormalSystem
  45
  46/-- A PRC embedding into a formal system preserves the primitive endpoint
  47distinction and finite trace extension. -/
  48structure PRCEmbeddingInto (F : FormalSystem) where
  49  endpointMap : Endpoint → F.Token
  50  traceMap : Trace → F.Expr
  51  preserves_distinction :
  52    F.distinguishes (endpointMap Endpoint.left) (endpointMap Endpoint.right)
  53  preserves_trace_extension :
  54    ∀ {T U : Trace}, Trace.Extends T U → F.exprExtends (traceMap T) (traceMap U)
  55
  56/-- The canonical embedding supplied by an expressive formal system's own trace
  57and endpoint interpretation fields. -/
  58def PRCEmbeddingInto.ofExpressive
  59    (F : FormalSystem) (hF : F.Expressive) : PRCEmbeddingInto F where
  60  endpointMap := F.endpointToken
  61  traceMap := F.traceExpr
  62  preserves_distinction := hF
  63  preserves_trace_extension := F.traceExpr_extends
  64
  65/-- Exact target for Build Order step 12. -/
  66def FormalSystemEmbeddingTarget : Prop :=
  67  ∀ F : FormalSystem, F.Expressive → Nonempty (PRCEmbeddingInto F)
  68
  69theorem FormalSystemEmbeddingTarget_proved :
  70    FormalSystemEmbeddingTarget := by
  71  intro F hF
  72  exact ⟨PRCEmbeddingInto.ofExpressive F hF⟩
  73
  74theorem Endpoint.left_ne_right :
  75    Endpoint.left ≠ Endpoint.right := by
  76  intro h
  77  have hside := congrArg Endpoint.side h
  78  cases hside
  79
  80/-- PRC itself as the minimal formal system: endpoint tokens are endpoints,
  81expressions are finite traces, and expression extension is trace extension. -/
  82def PRCFormalSystem : FormalSystem where
  83  Token := Endpoint
  84  Expr := Trace
  85  distinguishes := fun a b => a ≠ b
  86  exprExtends := Trace.Extends
  87  endpointToken := id
  88  traceExpr := id
  89  traceExpr_extends := by
  90    intro T U hTU
  91    exact hTU
  92
  93theorem PRCFormalSystem_expressive :
  94    PRCFormalSystem.Expressive := by
  95  exact Endpoint.left_ne_right
  96
  97theorem PRCFormalSystem_embedding :
  98    Nonempty (PRCEmbeddingInto PRCFormalSystem) :=
  99  FormalSystemEmbeddingTarget_proved PRCFormalSystem PRCFormalSystem_expressive
 100
 101/-- Step 12 certificate: the formal-system surface and embedding theorem are
 102closed. The broader claim that every external foundation satisfies this
 103interface is the next inevitability layer, not hidden here. -/
 104structure FormalSystemCertificate : Prop where
 105  formal_system_surface : Nonempty FormalSystem
 106  prc_system_expressive : PRCFormalSystem.Expressive
 107  prc_system_embedding : Nonempty (PRCEmbeddingInto PRCFormalSystem)
 108  embedding_target : FormalSystemEmbeddingTarget
 109  embedding_from_expressive :
 110    ∀ F : FormalSystem, F.Expressive → Nonempty (PRCEmbeddingInto F)
 111  strength_tag : StrengthTag.deltaOnly = StrengthTag.deltaOnly
 112
 113theorem formal_system_certificate : FormalSystemCertificate where
 114  formal_system_surface := ⟨PRCFormalSystem⟩
 115  prc_system_expressive := PRCFormalSystem_expressive
 116  prc_system_embedding := PRCFormalSystem_embedding
 117  embedding_target := FormalSystemEmbeddingTarget_proved
 118  embedding_from_expressive := FormalSystemEmbeddingTarget_proved
 119  strength_tag := rfl
 120
 121end PrimitiveRecognitionCalculus
 122end Foundation
 123end IndisputableMonolith
 124