Foundation Primitive Recognition Calculus Same Diff Same Refl

Reflexivity in the ledger

In the Recognition Science framework, reality keeps a ledger, a discrete record of recognition events. The declaration same_refl establishes the most basic rule of identity within that ledger: for any endpoint a, at any trace T, the judgment "a is the same as a" holds. It is the formal statement that every object is identical to itself, at every moment the ledger records.

This is not a discovery about the world. It is a structural requirement, one of five admissibility conditions that any consistent ledger must satisfy. The declaration extracts this requirement from the TraceJudgment structure, which defines what a trace judgment is: an object-level statement of equality or difference between endpoints at a given trace. The same_refl theorem is the reflexivity part of that structure, alongside symmetry and transitivity, which together make the "same" relation an equivalence relation at each trace.

The declaration also carries a consistency guarantee. The framework requires that SameT and DiffT cannot both hold for the same ordered pair at the same trace. This exclusivity condition is what makes the ledger coherent: a trace cannot simultaneously assert that two endpoints are the same and that they are different. The consistent_of_exclusive theorem proves this directly from the structure's fields.

In Recognition Science, the declaration does not claim that reflexivity is derived from anything deeper. It is an axiom, a postulate of the framework. It does not claim that the ledger's equality is the same as equality in ordinary mathematics or in the ambient type theory. The verifierEqualityJudgment definition provides a sanity model showing the interface is inhabited in the verifier's language, but this is explicitly not the object-level primitive. The declaration establishes a rule for the ledger, not a metaphysical claim about the nature of identity.

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

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

What this page does not claim

The declaration does not claim that reflexivity is derived from deeper principles; it is an axiom of the framework. The declaration does not claim that ledger equality is the same as equality in ordinary mathematics or the ambient type theory. The declaration does not claim anything about the physical world beyond the formal structure of the ledger.

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: