Foundation Primitive Recognition Calculus Prcone Primitive Structure

The primitive structure

Recognition Science is a formal framework that attempts to build mathematical structure from a single starting point: a discrete record of events, called a ledger. The framework's foundational layer asks what is needed to make even the simplest comparison, the judgment that two things are the same or different. The answer, proved in the framework's machine-checked library of formal theorems, is that comparison needs no second primitive. On a structure with exactly two endpoints, any judgment that behaves like an equivalence relation, is decidable, and separates the two endpoints is forced to be the ordinary equality of the structure itself.

The key theorem, comparison_is_derived_not_primitive, states this precisely. If a judgment J satisfies three conditions, that it is an equivalence relation, that its "different" relation is the negation of its "same" relation, and that it treats the two endpoints as distinct, then for any trace and any two endpoints, J's "same" relation is equivalent to equality. The proof uses only the admissibility fields of the judgment, meaning reflexivity and symmetry, and the fact that the two-endpoint type is freely generated. The framework's own act judgment, which is defined as the verifier's equality judgment, is then shown to coincide with this forced judgment.

This result resolves what the framework calls "Item 5": the question of whether recognition requires a separate comparison primitive. The framework's answer is that it does not. The comparison is derived from the act of recognition itself, computed purely from the inductive structure of the generated type. In plain terms, the framework shows that if you have a structure with two distinct elements and a judgment that respects the basic laws of equivalence, then that judgment cannot be anything other than the equality you already have. There is no room for a second, independent notion of sameness.

What the framework does not claim is equally important. This theorem does not say that all judgments in all contexts reduce to equality. It applies to the specific two-endpoint structure with the stated conditions. It does not claim that the framework's starting point, the act of recognition itself, is justified or derived; it is the primitive assumption. The theorem also does not claim anything about the physical world directly. It is a formal result about a formal structure, and any application to physics is a separate step that the framework's later layers attempt but this theorem alone does not establish.

The consequence of this result is that the framework can proceed with a single primitive. The act of recognition, modeled as the generation of a two-endpoint type, carries with it the ability to compare. This is the first rung in the framework's ladder, and it is a rung that the framework proves is stable: the comparison it needs is not an extra assumption but a consequence of the structure it already has.

/-- **Item 5 resolution.** Recognition is one primitive. For any judgment that is
an equivalence (the admissibility fields), tight, and separating, the `same`
relation is forced to be the decidable equality carried by the act-generated
structure. Hence the same/different judgment is derived from the act, not an
independent second primitive. -/
theorem comparison_is_derived_not_primitive
    (J : TraceJudgment)
    (htight : ∀ (T : Trace) (a b : Endpoint), J.diff T a b ↔ ¬ J.same T a b)
    (hsep : ∀ T : Trace, J.diff T Endpoint.left Endpoint.right) :
    ∀ (T : Trace) (a b : Endpoint),
      (J.same T a b ↔ a = b)
        ∧ (J.same T a b ↔ actJudgment.same T a b) := by
  intro T a b
  have h := genuine_judgment_same_is_equality J htight hsep T a b
  exact ⟨h, h.trans (actJudgment_same T a b).symm⟩

theorem actJudgment_same (T : Trace) (a b : Endpoint) :
    actJudgment.same T a b ↔ a = b := Iff.rfl

What this page does not claim

This theorem does not claim that all judgments in all contexts reduce to equality. This theorem does not justify the primitive act of recognition itself, which is assumed. This theorem does not make any direct claim about the physical world.

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