Foundation Primitive Recognition Calculus Quotient Endpoint Class Of

Endpoint classes and what they do not claim

In mathematics, a quotient is a way of treating distinct objects as equivalent when a chosen relation says they should be. The declaration endpointClassOf builds exactly that: given a trace (a finite sequence of recognition events) and a judgment that says when two endpoints are the same, it maps each endpoint to its equivalence class. Two endpoints land in the same class precisely when the judgment declares them the same. This is a definition, not a discovery; it packages an existing relation into a new type.

The construction appears in the Recognition Science framework's ledger, a discrete record of events. The formal library proves one theorem about it: if the judgment says two endpoints are the same, then their classes are equal. That is the only substantive result attached to endpointClassOf. It also provides a standard tool for defining functions on classes, but that tool merely restates the quotient property.

What the declaration does not claim is more important. It does not say that the judgment is correct, that it matches physical identity, or that any two endpoints are actually the same object. It does not assert that the relation is the right one for physics. It only says: if you give me a relation, I will form the classes. The choice of relation lives elsewhere, and the physical interpretation remains open.

In plain terms, endpointClassOf is a bookkeeping device. It takes a decision about sameness and makes it usable in the formal language. The decision itself is not made here.

/-- K4.4. SameT endpoints determine the same quotient class. -/
theorem endpointClass_eq_of_same
    (J : TraceJudgment) (T : Trace) {a b : Endpoint}
    (h : J.same T a b) :
    endpointClassOf J T a = endpointClassOf J T b :=
  Quot.sound h

/-- The class of an endpoint. -/
def endpointClassOf (J : TraceJudgment) (T : Trace)
    (a : Endpoint) : EndpointClass J T :=
  Quot.mk (sameSetoid J T) a

What this page does not claim

The declaration does not assert that the judgment is correct or physically meaningful. It does not claim that any two distinct endpoints are actually the same object. It does not define which endpoints are physically identical.

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/Quotient.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: