Foundation Primitive Recognition Calculus Same Diff Verifier Equality Judgment

The equality judgment

In mathematics, equality is the relation that says two objects are interchangeable: if a equals b, then anything true of a is true of b. The classical rule is Leibniz's law, named after Gottfried Wilhelm Leibniz, who stated it in the 1680s. A verifier of equality must at minimum respect three properties: reflexivity (a equals a), symmetry (if a equals b then b equals a), and transitivity (if a equals b and b equals c then a equals c). These three together make equality an equivalence relation, the standard foundation for treating objects as the same.

Within the Recognition Science framework, equality is not taken as a given but is modeled as a ledger, a discrete record of events, at each step of a trace, a sequence of recognition events. The declaration verifierEqualityJudgment is a machine-checked definition in the framework's library of formal results. It constructs a concrete instance of a TraceJudgment, a structure that packages two relations: SameT, meaning two endpoints are judged equal at a trace, and DiffT, meaning they are judged different. The definition shows that such a judgment surface is inhabited, that is, that a consistent model of the SameT/DiffT interface exists in the verifier's own language.

The definition carries proofs that SameT is reflexive, symmetric, and transitive at every trace, and that SameT and DiffT are exclusive: no ordered pair can be both same and different at the same trace. From these fields, the library extracts results same_refl, same_symm, and same_trans, and a consistency result consistent_of_exclusive. It also derives a substitution rule: if a predicate respects SameT, meaning it treats judged-equal endpoints alike, then a proof about a transfers to b. This is the framework's analogue of Leibniz's law, stated for its own equality judgment rather than for the ambient type theory's equality.

The honest scope is narrow. The definition is a sanity model, not a claim about how recognition actually works. The docstring is explicit: this is not the object-level primitive of the framework's primitive recognition calculus, but a verifier-level model showing the interface is inhabited. It does not assert that the universe uses this judgment, nor that SameT and DiffT are the only relations a trace can carry. It does not prove that any actual physical process realizes this structure. What it establishes is that the framework's specification of an equality judgment is coherent: a structure satisfying reflexivity, symmetry, transitivity, exclusivity, and substitution can be built in the machine-checked language.

The consequence for a reader is a precise picture of what the framework means when it speaks of equality at a trace. Equality is not an undefined primitive but a judged relation with stated properties, and the judgment is consistent by construction. This matters because later framework claims about recognition and cost depend on having a well-defined notion of sameness and difference at each step. The declaration secures that foundation in the library, and it does so without pretending the model is the reality.

/-- A verifier-level model of the SameT/DiffT interface.

This is not PRC's object-level primitive. It is a sanity model showing the
interface is inhabited in Lean's verifier language. -/
def verifierEqualityJudgment : TraceJudgment where
  same := fun _ a b => a = b
  diff := fun _ a b => a ≠ b
  same_refl_proof := by
    intro T a
    rfl
  same_symm_proof := by
    intro T a b h
    exact h.symm
  same_trans_proof := by
    intro T a b c hab hbc
    exact hab.trans hbc
  same_diff_exclusive := by
    intro T a b hsame hdiff
    exact hdiff hsame

/-- A verifier-level model of the SameT/DiffT interface.

This is not PRC's object-level primitive. It is a sanity model showing the
interface is inhabited in Lean's verifier language. -/
def verifierEqualityJudgment : TraceJudgment where
  same := fun _ a b => a = b
  diff := fun _ a b => a ≠ b
  same_refl_proof := by
    intro T a
    rfl
  same_symm_proof := by
    intro T a b h
    exact h.symm
  same_trans_proof := by
    intro T a b c hab hbc
    exact hab.trans hbc
  same_diff_exclusive := by
    intro T a b hsame hdiff
    exact hdiff hsame

/-- 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

/-- 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

No claim that the universe actually uses this equality judgment. No claim that SameT and DiffT are the only relations a trace can carry. No claim that this model is the object-level primitive of the primitive recognition calculus.

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: