Foundation Primitive Recognition Calculus Prcone Primitive

The single primitive

In mathematics, a distinction between two things is usually taken for granted: you have a set, and you have an equality relation on it. The framework called Recognition Science asks what must be assumed at the very bottom, and its answer is that comparison is not a second primitive alongside the act of recognition. The module PRCOnePrimitive establishes this by constructing a minimal formal world with exactly two endpoints, named left and right, and showing that any judgment about whether two endpoints are the same or different is forced to be the built-in equality of that structure.

The key construction is a trace: a discrete record of which endpoint was recognized at each step. From the act-generated structure alone, the framework derives a comparison operation. The theorem comparison_is_derived_not_primitive states that for any judgment which is an equivalence relation, is tight (different means not same), and separates the two endpoints, the same/different judgment must coincide exactly with the equality carried by the trace structure. This is a formal proof in the machine-checked library of formal theorems, not a philosophical preference.

The consequence is that "compare" needs no second primitive. The framework models recognition as one act: generating a trace. The comparison falls out as a decidable property of that trace, computed by structural recursion on the constructors. This resolves what the module calls Item 5: the same/different judgment is derived from the act, not an independent assumption. In plain terms, the universe does not need a separate rule for telling things apart; the act of recording already supplies it.

This result matters because it shrinks the foundation. If comparison were a separate primitive, the framework would need two unexplained starting points. Instead, one act generates both the objects and the ability to distinguish them. The proof uses only the admissibility fields of the judgment, namely reflexivity and symmetry of the same relation, plus tightness and separation. Nothing else is assumed. The framework's library proves this once, and the result becomes a load-bearing floor for the rest of the forcing chain that derives constants and dimensions.

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

/-- The forced comparison is decidable, computed purely from the act-generated
inductive structure. This is the formal sense in which "compare" needs no second
primitive: it is `decide` on a freely generated type. -/
instance actJudgment_same_decidable (T : Trace) (a b : Endpoint) :
    Decidable (actJudgment.same T a b) := by
  show Decidable (a = b)
  exact inferInstance

/-- Core forcing lemma. On the two-endpoint type, an equivalence that does not
relate `left` to `right` is equality. Only reflexivity and symmetry of `same`
are used, both supplied by the `TraceJudgment` admissibility fields. -/
theorem genuine_judgment_same_is_equality
    (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 := by
  have hne : ¬ J.same T Endpoint.left Endpoint.right :=
    (htight T Endpoint.left Endpoint.right).mp (hsep T)
  constructor
  · intro hsame
    rcases endpoint_eq_left_or_right a with ha | ha <;>
      rcases endpoint_eq_left_or_right b with hb | hb <;>
      subst ha <;> subst hb
    · rfl
    · exact absurd hsame hne
    · exact absurd (J.same_symm T hsame) hne
    · rfl
  · intro hab
    subst hab
    exact J.same_refl T a

What this page does not claim

This module does not prove that the trace structure itself exists; it assumes a freely generated type with two constructors. This module does not derive the cost function J or any constants; it only establishes that comparison is derived from the act. This module does not claim that equality is the only possible judgment; it shows that any admissible judgment must coincide with equality.

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: