Foundation Primitive Recognition Calculus Same Diff Substitute

The substitution rule

In logic and mathematics, substitution is the rule that if two things are equal, and a statement is true of the first, then it is true of the second. The Recognition Science framework builds its foundation on a specific, formal version of this idea. Its machine-checked library of formal theorems contains a declaration named substitute, which establishes the exact conditions under which this swap is allowed in its primitive recognition calculus.

The framework's starting point is a ledger, a discrete record of events. At each step, the framework records whether two endpoints are judged the same or different. This record is called a trace. The substitute rule says: if a trace records two endpoints as the same, and a property holds for the first endpoint, then that property holds for the second. This is the classical substitution principle, but with one important restriction. The swap is only valid for properties that respect the trace's judgment of sameness. A property respects sameness if, whenever the trace says two endpoints are the same, the property holds for one exactly when it holds for the other. Without this condition, substitution would not be sound.

The declaration also proves that this rule is consistent with the rest of the framework. The trace's judgments of same and different are exclusive: they cannot both hold for the same pair of endpoints. From this, the framework derives that every trace is consistent, meaning it never asserts both sameness and difference for the same pair. The substitute rule then follows directly from the definition of what it means for a property to respect sameness. It is not an additional assumption; it is a theorem extracted from the framework's own definitions.

What the declaration does not do is claim that this substitution rule is the only way to reason about equality. The framework also provides a separate, verifier-level model of the same/different interface, explicitly described as a sanity check that the interface is usable, not as the primitive object-level rule. The substitute rule is a theorem about the framework's own trace judgments, not a claim about equality in any other system. It establishes one precise, machine-checked fact: within this ledger-based calculus, substitution is valid exactly for properties that respect the recorded sameness.

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

/-- A predicate respects SameT at a trace. -/
def RespectsSame (J : TraceJudgment) (T : Trace)
    (P : Endpoint → Prop) : Prop :=
  ∀ {a b : Endpoint}, J.same T a b → P a → P 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

What this page does not claim

This declaration does not prove that substitution is valid for properties that do not respect the trace's sameness judgment. This declaration does not claim that the verifier-level model is the framework's object-level primitive rule. This declaration does not establish substitution for any system other than the framework's own trace judgments.

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: