Foundation Primitive Recognition Calculus Same Diff Consistent Of Exclusive

The consistency guarantee

In logic and mathematics, a system is consistent when it never asserts a contradiction. The declaration consistent_of_exclusive establishes a precise version of that idea for a specific kind of judgment. It says: if a judgment surface is built so that same and different are exclusive for any pair of endpoints, then the surface is consistent at every trace. A trace is a discrete record of recognition events, and an endpoint is an object being compared. The theorem proves that the exclusivity rule, stated once as a design choice, guarantees the stronger property that no trace ever contains a contradiction.

The proof is direct. The definition of consistency requires that for any two endpoints, it is never the case that both same and different hold. The theorem takes the exclusivity field from the judgment surface and applies it to that definition. The machine-checked library of formal theorems confirms the step. This is a small but load-bearing result: it shows that a local rule, applied to each pair, automatically gives a global guarantee across the whole trace. Without it, a judgment surface could behave well pair by pair and still produce a contradiction somewhere.

The declaration does not claim that any particular judgment surface exists. It does not say which endpoints are the same or different, nor does it prove that a meaningful comparison is possible at all. It only says that if a surface satisfies the exclusivity condition, then consistency follows. The theorem also does not establish that the judgment surface is complete, meaning that for every pair of endpoints one of the two relations must hold. Consistency and completeness are separate properties, and this result addresses only the first.

In Recognition Science, this result anchors the primitive calculus. It lets the framework reason about equality and difference without worrying that a trace might contradict itself. The practical consequence is that any judgment surface built on the exclusivity rule can be trusted to be contradiction-free at every step. That is what the declaration establishes, and nothing more.

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

/-- 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 prove that any particular judgment surface exists. The declaration does not establish that the judgment surface is complete, meaning that for every pair of endpoints one of the two relations must hold.

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: