IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.SameDiff

   1/-
   2  PrimitiveRecognitionCalculus/SameDiff.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchors:
   8    K2.6-K2.10, R5-R7, K4.2-K4.3
   9
  10  This module does not define object equality as Lean equality. It defines
  11  an admissible trace-judgment surface: SameT, DiffT, consistency, and the
  12  substitution rule for contexts that respect SameT.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21
  22/-- K2.6-K2.8. An admissible trace judgment surface. -/
  23structure TraceJudgment where
  24  /-- K2.7. Object-level equality at a trace. -/
  25  same : Trace → Endpoint → Endpoint → Prop
  26  /-- K2.6. Object-level witnessed difference at a trace. -/
  27  diff : Trace → Endpoint → Endpoint → Prop
  28  /-- R5. SameT must be reflexive at each trace. -/
  29  same_refl_proof : ∀ T : Trace, Reflexive (same T)
  30  /-- R5. SameT must be symmetric at each trace. -/
  31  same_symm_proof : ∀ T : Trace, Symmetric (same T)
  32  /-- R5. SameT must be transitive at each trace. -/
  33  same_trans_proof : ∀ T : Trace, Transitive (same T)
  34  /-- R6. SameT and DiffT cannot both hold for the same ordered pair. -/
  35  same_diff_exclusive :
  36    ∀ {T : Trace} {a b : Endpoint}, same T a b → diff T a b → False
  37
  38namespace TraceJudgment
  39
  40/-- Reflexivity of SameT, extracted from the admissibility field. -/
  41theorem same_refl (J : TraceJudgment) (T : Trace) (a : Endpoint) :
  42    J.same T a a :=
  43  J.same_refl_proof T a
  44
  45/-- Symmetry of SameT, extracted from the admissibility field. -/
  46theorem same_symm (J : TraceJudgment) (T : Trace) {a b : Endpoint}
  47    (h : J.same T a b) :
  48    J.same T b a :=
  49  J.same_symm_proof T h
  50
  51/-- Transitivity of SameT, extracted from the admissibility field. -/
  52theorem same_trans (J : TraceJudgment) (T : Trace) {a b c : Endpoint}
  53    (hab : J.same T a b) (hbc : J.same T b c) :
  54    J.same T a c :=
  55  J.same_trans_proof T hab hbc
  56
  57end TraceJudgment
  58
  59/-- K2.8. A trace is consistent for a judgment surface if it never asserts
  60SameT and DiffT for the same endpoints. -/
  61def Consistent (J : TraceJudgment) (T : Trace) : Prop :=
  62  ∀ a b : Endpoint, ¬ (J.same T a b ∧ J.diff T a b)
  63
  64/-- R6. The exclusivity field gives consistency at every trace. -/
  65theorem consistent_of_exclusive (J : TraceJudgment) (T : Trace) :
  66    Consistent J T := by
  67  intro a b h
  68  exact J.same_diff_exclusive h.1 h.2
  69
  70/-- A predicate respects SameT at a trace. -/
  71def RespectsSame (J : TraceJudgment) (T : Trace)
  72    (P : Endpoint → Prop) : Prop :=
  73  ∀ {a b : Endpoint}, J.same T a b → P a → P b
  74
  75/-- K2.10 and R7. Substitution for contexts that respect SameT. -/
  76theorem substitute
  77    (J : TraceJudgment) (T : Trace) (P : Endpoint → Prop)
  78    (hP : RespectsSame J T P) {a b : Endpoint}
  79    (hsame : J.same T a b) (ha : P a) :
  80    P b :=
  81  hP hsame ha
  82
  83/-- A verifier-level model of the SameT/DiffT interface.
  84
  85This is not PRC's object-level primitive. It is a sanity model showing the
  86interface is inhabited in Lean's verifier language. -/
  87def verifierEqualityJudgment : TraceJudgment where
  88  same := fun _ a b => a = b
  89  diff := fun _ a b => a ≠ b
  90  same_refl_proof := by
  91    intro T a
  92    rfl
  93  same_symm_proof := by
  94    intro T a b h
  95    exact h.symm
  96  same_trans_proof := by
  97    intro T a b c hab hbc
  98    exact hab.trans hbc
  99  same_diff_exclusive := by
 100    intro T a b hsame hdiff
 101    exact hdiff hsame
 102
 103end PrimitiveRecognitionCalculus
 104end Foundation
 105end IndisputableMonolith
 106