Foundation Primitive Recognition Calculus Prcone Primitive Genuine Judgment Same

The forced identity

In mathematics, an equivalence relation is a rule that groups things together: it is reflexive (everything relates to itself), symmetric (if A relates to B, then B relates to A), and transitive (if A relates to B and B relates to C, then A relates to C). Equality is the strictest equivalence relation, the one that only relates a thing to itself. The question at stake is whether a system built on acts of recognition can get by with only a primitive notion of 'same' and 'different', or whether it must also assume equality as a separate, unexplained ingredient.

The framework's answer, proved in its machine-checked library of formal theorems, is that equality comes for free. The setting is the simplest possible one: a type with exactly two endpoints, conventionally called left and right. A judgment is an equivalence relation on these endpoints, with the additional properties that 'same' and 'different' are complementary (tight), and that the two endpoints are genuinely distinct (separating). The theorem genuine_judgment_same_is_equality proves that any such judgment must identify 'same' with actual equality: for any two endpoints a and b, the judgment says 'same' if and only if a equals b. There is no room for a looser notion of sameness that groups the two endpoints together.

The proof is short because the structure is austere. With only two endpoints, the separating condition rules out the one non-trivial equivalence relation (the one that would identify left with right). What remains is exactly the diagonal relation, which is equality. The framework reads this as a resolution of a design question: recognition is one primitive, and comparison is derived from it, not an independent second primitive. The decidable equality on the act-generated type is an instance obtained by structural recursion on the constructors, meaning the ability to compare is computed from the act itself.

What the theorem does not claim is broader. It does not say that all equivalence relations in mathematics collapse to equality; it says only that on a two-element type with the tightness and separation conditions, they do. It does not establish anything about the physical world, about what humans perceive as similar, or about the cost function J(x) that drives the framework's later results. It is a lemma about a minimal formal structure, and its significance is architectural: it shows that a recognition calculus can be built without assuming comparison as a separate axiom.

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

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

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

What this page does not claim

This theorem does not claim that all equivalence relations in mathematics collapse to equality. This theorem does not make any claim about the physical world or human perception. This theorem does not establish anything about the cost function J(x) or the golden ratio.

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: