IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceLogic

   1/-
   2  PrimitiveRecognitionCalculus/TraceLogic.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 11: build logical connectives and quantifier surfaces from
   9    stable trace predicates.
  10
  11  This first pass keeps the logic surface over finite PRC traces. Completed
  12  trace families and model-theoretic inevitability are separate later layers.
  13-/
  14
  15import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.SameDiff
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace PrimitiveRecognitionCalculus
  20
  21/-- A proposition in the first PRC logic pass is a predicate on finite traces
  22that persists under trace extension. -/
  23structure TracePredicate where
  24  holds : Trace → Prop
  25  stable :
  26    ∀ {T U : Trace}, Trace.Extends T U → holds T → holds U
  27
  28namespace TracePredicate
  29
  30/-- Truth is the stable predicate that holds at every trace. -/
  31def top : TracePredicate where
  32  holds := fun _ => True
  33  stable := by
  34    intro _T _U _hTU _h
  35    trivial
  36
  37/-- Falsehood is the stable predicate that holds at no trace. -/
  38def bottom : TracePredicate where
  39  holds := fun _ => False
  40  stable := by
  41    intro _T _U _hTU h
  42    exact False.elim h
  43
  44/-- Conjunction of stable trace predicates. -/
  45def and (P Q : TracePredicate) : TracePredicate where
  46  holds := fun T => P.holds T ∧ Q.holds T
  47  stable := by
  48    intro T U hTU h
  49    exact ⟨P.stable hTU h.1, Q.stable hTU h.2⟩
  50
  51/-- Disjunction of stable trace predicates. -/
  52def or (P Q : TracePredicate) : TracePredicate where
  53  holds := fun T => P.holds T ∨ Q.holds T
  54  stable := by
  55    intro T U hTU h
  56    cases h with
  57    | inl hP => exact Or.inl (P.stable hTU hP)
  58    | inr hQ => exact Or.inr (Q.stable hTU hQ)
  59
  60/-- Implication is persistence along every future extension of the current
  61trace. This makes implication itself stable under extension. -/
  62def imp (P Q : TracePredicate) : TracePredicate where
  63  holds := fun T =>
  64    ∀ U : Trace, Trace.Extends T U → P.holds U → Q.holds U
  65  stable := by
  66    intro T U hTU h V hUV hPV
  67    exact h V (Trace.extends_trans hTU hUV) hPV
  68
  69/-- Negation is implication into falsehood. -/
  70def not (P : TracePredicate) : TracePredicate :=
  71  imp P bottom
  72
  73/-- Universal quantification over a verifier-indexed family of stable trace
  74predicates. The family parameter is verifier bookkeeping; stability is still a
  75finite-trace theorem. -/
  76def all {α : Type} (P : α → TracePredicate) : TracePredicate where
  77  holds := fun T => ∀ a : α, (P a).holds T
  78  stable := by
  79    intro T U hTU h a
  80    exact (P a).stable hTU (h a)
  81
  82/-- Existential quantification over a verifier-indexed family of stable trace
  83predicates. The witness is preserved while the trace is extended. -/
  84def exists_ {α : Type} (P : α → TracePredicate) : TracePredicate where
  85  holds := fun T => ∃ a : α, (P a).holds T
  86  stable := by
  87    intro T U hTU h
  88    rcases h with ⟨a, ha⟩
  89    exact ⟨a, (P a).stable hTU ha⟩
  90
  91theorem top_intro (T : Trace) :
  92    top.holds T := by
  93  trivial
  94
  95theorem and_intro {P Q : TracePredicate} {T : Trace}
  96    (hP : P.holds T) (hQ : Q.holds T) :
  97    (and P Q).holds T := by
  98  exact ⟨hP, hQ⟩
  99
 100theorem and_left {P Q : TracePredicate} {T : Trace}
 101    (h : (and P Q).holds T) :
 102    P.holds T := by
 103  exact h.1
 104
 105theorem and_right {P Q : TracePredicate} {T : Trace}
 106    (h : (and P Q).holds T) :
 107    Q.holds T := by
 108  exact h.2
 109
 110theorem or_inl {P Q : TracePredicate} {T : Trace}
 111    (hP : P.holds T) :
 112    (or P Q).holds T := by
 113  exact Or.inl hP
 114
 115theorem or_inr {P Q : TracePredicate} {T : Trace}
 116    (hQ : Q.holds T) :
 117    (or P Q).holds T := by
 118  exact Or.inr hQ
 119
 120theorem imp_elim {P Q : TracePredicate} {T U : Trace}
 121    (himp : (imp P Q).holds T)
 122    (hTU : Trace.Extends T U)
 123    (hP : P.holds U) :
 124    Q.holds U := by
 125  exact himp U hTU hP
 126
 127theorem not_elim {P : TracePredicate} {T U : Trace}
 128    (hn : (not P).holds T)
 129    (hTU : Trace.Extends T U)
 130    (hP : P.holds U) :
 131    False := by
 132  exact hn U hTU hP
 133
 134theorem all_intro {α : Type} {P : α → TracePredicate} {T : Trace}
 135    (h : ∀ a : α, (P a).holds T) :
 136    (all P).holds T := by
 137  exact h
 138
 139theorem all_elim {α : Type} {P : α → TracePredicate} {T : Trace}
 140    (h : (all P).holds T) (a : α) :
 141    (P a).holds T := by
 142  exact h a
 143
 144theorem exists_intro {α : Type} {P : α → TracePredicate} {T : Trace}
 145    (a : α) (h : (P a).holds T) :
 146    (exists_ P).holds T := by
 147  exact ⟨a, h⟩
 148
 149theorem persists {P : TracePredicate} {T U : Trace}
 150    (hTU : Trace.Extends T U) (hP : P.holds T) :
 151    P.holds U :=
 152  P.stable hTU hP
 153
 154end TracePredicate
 155
 156/-- Headline target for the first trace-logic pass. -/
 157structure TraceLogicCertificate : Prop where
 158  proposition_surface : Nonempty TracePredicate
 159  truth_intro : ∀ T : Trace, TracePredicate.top.holds T
 160  conjunction_intro :
 161    ∀ {P Q : TracePredicate} {T : Trace},
 162      P.holds T → Q.holds T → (TracePredicate.and P Q).holds T
 163  conjunction_left :
 164    ∀ {P Q : TracePredicate} {T : Trace},
 165      (TracePredicate.and P Q).holds T → P.holds T
 166  conjunction_right :
 167    ∀ {P Q : TracePredicate} {T : Trace},
 168      (TracePredicate.and P Q).holds T → Q.holds T
 169  disjunction_left :
 170    ∀ {P Q : TracePredicate} {T : Trace},
 171      P.holds T → (TracePredicate.or P Q).holds T
 172  disjunction_right :
 173    ∀ {P Q : TracePredicate} {T : Trace},
 174      Q.holds T → (TracePredicate.or P Q).holds T
 175  implication_elim :
 176    ∀ {P Q : TracePredicate} {T U : Trace},
 177      (TracePredicate.imp P Q).holds T →
 178        Trace.Extends T U → P.holds U → Q.holds U
 179  negation_elim :
 180    ∀ {P : TracePredicate} {T U : Trace},
 181      (TracePredicate.not P).holds T →
 182        Trace.Extends T U → P.holds U → False
 183  universal_intro :
 184    ∀ {α : Type} {P : α → TracePredicate} {T : Trace},
 185      (∀ a : α, (P a).holds T) → (TracePredicate.all P).holds T
 186  universal_elim :
 187    ∀ {α : Type} {P : α → TracePredicate} {T : Trace},
 188      (TracePredicate.all P).holds T → ∀ a : α, (P a).holds T
 189  existential_intro :
 190    ∀ {α : Type} {P : α → TracePredicate} {T : Trace},
 191      ∀ a : α, (P a).holds T → (TracePredicate.exists_ P).holds T
 192  persistence :
 193    ∀ {P : TracePredicate} {T U : Trace},
 194      Trace.Extends T U → P.holds T → P.holds U
 195  strength_tag : StrengthTag.deltaOnly = StrengthTag.deltaOnly
 196
 197theorem trace_logic_certificate : TraceLogicCertificate where
 198  proposition_surface := ⟨TracePredicate.top⟩
 199  truth_intro := TracePredicate.top_intro
 200  conjunction_intro := by
 201    intro P Q T hP hQ
 202    exact TracePredicate.and_intro hP hQ
 203  conjunction_left := by
 204    intro P Q T h
 205    exact TracePredicate.and_left h
 206  conjunction_right := by
 207    intro P Q T h
 208    exact TracePredicate.and_right h
 209  disjunction_left := by
 210    intro P Q T hP
 211    exact TracePredicate.or_inl hP
 212  disjunction_right := by
 213    intro P Q T hQ
 214    exact TracePredicate.or_inr hQ
 215  implication_elim := by
 216    intro P Q T U himp hTU hP
 217    exact TracePredicate.imp_elim himp hTU hP
 218  negation_elim := by
 219    intro P T U hn hTU hP
 220    exact TracePredicate.not_elim hn hTU hP
 221  universal_intro := by
 222    intro α P T h
 223    exact TracePredicate.all_intro h
 224  universal_elim := by
 225    intro α P T h a
 226    exact TracePredicate.all_elim h a
 227  existential_intro := by
 228    intro α P T a h
 229    exact TracePredicate.exists_intro a h
 230  persistence := by
 231    intro P T U hTU hP
 232    exact TracePredicate.persists hTU hP
 233  strength_tag := rfl
 234
 235end PrimitiveRecognitionCalculus
 236end Foundation
 237end IndisputableMonolith
 238