IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCOnePrimitive

   1/-
   2  PrimitiveRecognitionCalculus/PRCOnePrimitive.lean
   3
   4  Item 5 of the δ frontier: one primitive or two?
   5
   6  Question. Recognition involves an *act* (mark / distinguish, here
   7  `DistinctionAct.delta`, which freely generates `Trace` and `Endpoint`) and a
   8  *judgment* (same / different). Is the judgment an independent second primitive,
   9  or does it reduce to the act?
  10
  11  Answer (proved here). One primitive. The act is the sole primitive. The
  12  same/different judgment is not independent: it is the decidable equality that
  13  the act-generated inductive structure already carries (constructor injectivity
  14  and disjointness, a metatheorem of free generation, not an axiom). More
  15  precisely, ANY judgment that
  16
  17    (i)  is an equivalence at each trace (the `TraceJudgment` admissibility
  18         fields),
  19    (ii) is tight: `diff` is exactly the negation of `same`, and
  20    (iii) actually separates the two sides of a distinction
  21         (`diff T left right` at every trace),
  22
  23  is FORCED to coincide with that derived equality
  24  (`comparison_is_derived_not_primitive`). The only way to escape the
  25  conclusion is to use a degenerate "judgment" that fails to separate the two
  26  sides of a distinction, i.e. one that denies the very distinction it is about.
  27
  28  So the "single primitive" claim is earned, not assumed. The nullary base
  29  (`Trace.empty`) is not a second primitive either: it is the zero-fold
  30  iteration of the single act.
  31
  32  No project-local axioms. No sorry.
  33-/
  34
  35import Mathlib
  36import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic
  37import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.SameDiff
  38
  39namespace IndisputableMonolith
  40namespace Foundation
  41namespace PrimitiveRecognitionCalculus
  42namespace OnePrimitive
  43
  44/-- The comparison apparatus is derived, not posited: decidable equality of the
  45act-generated types is an instance, obtained by structural recursion on the
  46constructors. -/
  47example : DecidableEq Endpoint := inferInstance
  48example : DecidableEq Trace := inferInstance
  49
  50/-- A distinction has exactly two endpoints. -/
  51theorem endpoint_eq_left_or_right (e : Endpoint) :
  52    e = Endpoint.left ∨ e = Endpoint.right := by
  53  obtain ⟨s⟩ := e
  54  cases s with
  55  | left => exact Or.inl rfl
  56  | right => exact Or.inr rfl
  57
  58/-- The judgment the act forces: `same` is equality, `diff` is disequality, both
  59decidable from the act-generated structure. -/
  60def actJudgment : TraceJudgment := verifierEqualityJudgment
  61
  62theorem actJudgment_same (T : Trace) (a b : Endpoint) :
  63    actJudgment.same T a b ↔ a = b := Iff.rfl
  64
  65theorem actJudgment_diff (T : Trace) (a b : Endpoint) :
  66    actJudgment.diff T a b ↔ a ≠ b := Iff.rfl
  67
  68/-- The forced comparison is decidable, computed purely from the act-generated
  69inductive structure. This is the formal sense in which "compare" needs no second
  70primitive: it is `decide` on a freely generated type. -/
  71instance actJudgment_same_decidable (T : Trace) (a b : Endpoint) :
  72    Decidable (actJudgment.same T a b) := by
  73  show Decidable (a = b)
  74  exact inferInstance
  75
  76/-- Core forcing lemma. On the two-endpoint type, an equivalence that does not
  77relate `left` to `right` is equality. Only reflexivity and symmetry of `same`
  78are used, both supplied by the `TraceJudgment` admissibility fields. -/
  79theorem genuine_judgment_same_is_equality
  80    (J : TraceJudgment)
  81    (htight : ∀ (T : Trace) (a b : Endpoint), J.diff T a b ↔ ¬ J.same T a b)
  82    (hsep : ∀ T : Trace, J.diff T Endpoint.left Endpoint.right)
  83    (T : Trace) (a b : Endpoint) :
  84    J.same T a b ↔ a = b := by
  85  have hne : ¬ J.same T Endpoint.left Endpoint.right :=
  86    (htight T Endpoint.left Endpoint.right).mp (hsep T)
  87  constructor
  88  · intro hsame
  89    rcases endpoint_eq_left_or_right a with ha | ha <;>
  90      rcases endpoint_eq_left_or_right b with hb | hb <;>
  91      subst ha <;> subst hb
  92    · rfl
  93    · exact absurd hsame hne
  94    · exact absurd (J.same_symm T hsame) hne
  95    · rfl
  96  · intro hab
  97    subst hab
  98    exact J.same_refl T a
  99
 100/-- **Item 5 resolution.** Recognition is one primitive. For any judgment that is
 101an equivalence (the admissibility fields), tight, and separating, the `same`
 102relation is forced to be the decidable equality carried by the act-generated
 103structure. Hence the same/different judgment is derived from the act, not an
 104independent second primitive. -/
 105theorem comparison_is_derived_not_primitive
 106    (J : TraceJudgment)
 107    (htight : ∀ (T : Trace) (a b : Endpoint), J.diff T a b ↔ ¬ J.same T a b)
 108    (hsep : ∀ T : Trace, J.diff T Endpoint.left Endpoint.right) :
 109    ∀ (T : Trace) (a b : Endpoint),
 110      (J.same T a b ↔ a = b)
 111        ∧ (J.same T a b ↔ actJudgment.same T a b) := by
 112  intro T a b
 113  have h := genuine_judgment_same_is_equality J htight hsep T a b
 114  exact ⟨h, h.trans (actJudgment_same T a b).symm⟩
 115
 116end OnePrimitive
 117end PrimitiveRecognitionCalculus
 118end Foundation
 119end IndisputableMonolith
 120