IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Quotient

   1/-
   2  PrimitiveRecognitionCalculus/Quotient.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchors:
   8    K2.11, K4.4
   9
  10  Quotienting is permitted only after SameT is known to be an equivalence.
  11  This module builds endpoint trace-classes and the corresponding recursion
  12  principle for SameT-respecting maps.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.SameDiff
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21
  22/-- K2.11. The setoid induced by SameT at a fixed trace. -/
  23def sameSetoid (J : TraceJudgment) (T : Trace) : Setoid Endpoint where
  24  r := J.same T
  25  iseqv := {
  26    refl := J.same_refl_proof T
  27    symm := by
  28      intro a b h
  29      exact J.same_symm_proof T h
  30    trans := by
  31      intro a b c hab hbc
  32      exact J.same_trans_proof T hab hbc
  33  }
  34
  35/-- K2.11. Endpoint trace-classes under SameT. -/
  36def EndpointClass (J : TraceJudgment) (T : Trace) : Type :=
  37  Quot (sameSetoid J T)
  38
  39/-- The class of an endpoint. -/
  40def endpointClassOf (J : TraceJudgment) (T : Trace)
  41    (a : Endpoint) : EndpointClass J T :=
  42  Quot.mk (sameSetoid J T) a
  43
  44/-- K4.4. SameT endpoints determine the same quotient class. -/
  45theorem endpointClass_eq_of_same
  46    (J : TraceJudgment) (T : Trace) {a b : Endpoint}
  47    (h : J.same T a b) :
  48    endpointClassOf J T a = endpointClassOf J T b :=
  49  Quot.sound h
  50
  51/-- K4.4. Quotient recursion for SameT-respecting maps. -/
  52def endpointClassLift
  53    (J : TraceJudgment) (T : Trace) {α : Sort _}
  54    (f : Endpoint → α)
  55    (hf : ∀ {a b : Endpoint}, J.same T a b → f a = f b) :
  56    EndpointClass J T → α :=
  57  Quot.lift f (by
  58    intro a b h
  59    exact hf h)
  60
  61@[simp] theorem endpointClassLift_mk
  62    (J : TraceJudgment) (T : Trace) {α : Sort _}
  63    (f : Endpoint → α)
  64    (hf : ∀ {a b : Endpoint}, J.same T a b → f a = f b)
  65    (a : Endpoint) :
  66    endpointClassLift J T f hf (endpointClassOf J T a) = f a := by
  67  rfl
  68
  69end PrimitiveRecognitionCalculus
  70end Foundation
  71end IndisputableMonolith
  72