Foundation Primitive Recognition Calculus Same Diff Trace Judgment

The trace judgment surface

A trace judgment is a rule for comparing two objects at a single moment. In the Recognition Science framework, a ledger, a discrete record of events, must be able to say whether two endpoints are the same object or different objects at each trace, a point in the record. The declaration TraceJudgment packages this comparison into a single structure with three requirements: sameness must be reflexive, symmetric, and transitive; difference must be exclusive with sameness; and the whole thing must be consistent at every trace.

The classical picture is an equivalence relation. If a is the same as b, then b is the same as a; if a is the same as b and b is the same as c, then a is the same as c; and every object is the same as itself. The framework adds one more rule: no pair can be both same and different at the same trace. That exclusivity is what makes the ledger usable, because a record that says both would be contradictory.

The declaration also proves three theorems from its own fields: reflexivity, symmetry, and transitivity of sameness. These are not assumptions; they are extracted from the structure's admissibility field. A separate definition, Consistent, states that no trace ever asserts both sameness and difference for the same pair, and the theorem consistent_of_exclusive shows the exclusivity field guarantees this. A further theorem, substitute, says that if a predicate respects sameness, then replacing one endpoint with another that is judged the same preserves the predicate's truth.

In Recognition Science, this is the primitive layer of comparison. The framework models the ledger's basic act of recognition, deciding whether two things are the same, as this judgment surface. The declaration does not claim that sameness is decidable, that the ledger can compare objects across different traces, or that the judgment surface is the only way to model recognition. It establishes only the local, per-trace rules of consistency and substitution.

/-- K2.6-K2.8. An admissible trace judgment surface. -/
structure TraceJudgment where
  /-- K2.7. Object-level equality at a trace. -/
  same : Trace → Endpoint → Endpoint → Prop
  /-- K2.6. Object-level witnessed difference at a trace. -/
  diff : Trace → Endpoint → Endpoint → Prop
  /-- R5. SameT must be reflexive at each trace. -/
  same_refl_proof : ∀ T : Trace, Reflexive (same T)
  /-- R5. SameT must be symmetric at each trace. -/
  same_symm_proof : ∀ T : Trace, Symmetric (same T)
  /-- R5. SameT must be transitive at each trace. -/
  same_trans_proof : ∀ T : Trace, Transitive (same T)
  /-- R6. SameT and DiffT cannot both hold for the same ordered pair. -/
  same_diff_exclusive :
    ∀ {T : Trace} {a b : Endpoint}, same T a b → diff T a b → False

/-- Reflexivity of SameT, extracted from the admissibility field. -/
theorem same_refl (J : TraceJudgment) (T : Trace) (a : Endpoint) :
    J.same T a a :=
  J.same_refl_proof T a

/-- Symmetry of SameT, extracted from the admissibility field. -/
theorem same_symm (J : TraceJudgment) (T : Trace) {a b : Endpoint}
    (h : J.same T a b) :
    J.same T b a :=
  J.same_symm_proof T h

/-- Transitivity of SameT, extracted from the admissibility field. -/
theorem same_trans (J : TraceJudgment) (T : Trace) {a b c : Endpoint}
    (hab : J.same T a b) (hbc : J.same T b c) :
    J.same T a c :=
  J.same_trans_proof T hab hbc

/-- K2.8. A trace is consistent for a judgment surface if it never asserts
SameT and DiffT for the same endpoints. -/
def Consistent (J : TraceJudgment) (T : Trace) : Prop :=
  ∀ a b : Endpoint, ¬ (J.same T a b ∧ J.diff T a b)

/-- R6. The exclusivity field gives consistency at every trace. -/
theorem consistent_of_exclusive (J : TraceJudgment) (T : Trace) :
    Consistent J T := by
  intro a b h
  exact J.same_diff_exclusive h.1 h.2

/-- K2.10 and R7. Substitution for contexts that respect SameT. -/
theorem substitute
    (J : TraceJudgment) (T : Trace) (P : Endpoint → Prop)
    (hP : RespectsSame J T P) {a b : Endpoint}
    (hsame : J.same T a b) (ha : P a) :
    P b :=
  hP hsame ha

What this page does not claim

The declaration does not claim that sameness is decidable for all endpoints. The declaration does not claim that the ledger can compare objects across different traces. The declaration does not claim that this judgment surface is the only way to model recognition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/SameDiff.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: