Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.SameDiff

show as:
view Lean formalization →

Defines the admissible trace judgment surface for Primitive Recognition Calculus (paper K2.6–K2.8): a “same” relation on traces with reflexivity, symmetry, and transitivity, plus consistency and substitution. Anyone building quotiented traces, kernel structure, or trace logic cites this layer. The module is mostly definitions and short algebraic lemmas discharging the equivalence and exclusivity axioms.

claimAn admissible trace judgment surface: a binary relation $\mathrm{same}$ on traces that is reflexive, symmetric, and transitive; a consistency predicate on judgments (including consistency from exclusivity); a respect-same condition; and a substitution principle, together with a verifier equality judgment.

background

Primitive Recognition Calculus treats recognition events as traces that may be compared before any metric or cost functional is imposed. This module sits on the Basic layer of that calculus and isolates the judgment surface: when two traces count as the same for downstream reasoning.

The central object is a trace judgment carrying a binary relation $\mathrm{same}$. The siblings same_refl, same_symm, and same_trans package the three equivalence laws. Consistency (and the lemma that exclusivity implies consistency) rules out contradictory same/diff verdicts on a single pair. RespectsSame and substitute ensure predicates and rewrites are invariant under the relation; verifierEqualityJudgment specializes equality for verifier-side checks.

Notation is intentionally pre-metric: no $J$-cost, $\phi$-ladder, or dimension count appears here. The module only fixes the logical surface that later quotient and kernel constructions will use.

proof idea

Definition-heavy module. Equivalence laws are discharged by short reflexivity/symmetry/transitivity proofs on the underlying same relation. Consistency is obtained either directly or via the exclusivity-implies-consistency lemma. Respect-same and substitution are structural lemmas: if a predicate respects same, equal traces may be rewritten in judgments. No deep analytic argument; the work is axiomatic packaging for importers.

why it matters in Recognition Science

This is the K2.6–K2.8 judgment surface that later PRC modules import wholesale. Kernel, PRCOnePrimitive, Quotient, and TraceLogic all depend on it: Quotient needs same as an equivalence to form trace classes; Kernel and TraceLogic need consistency and substitution so derived rules stay well-defined; PRCOnePrimitive uses the surface when reducing to a single primitive. Without a clean same/diff layer, the forcing chain’s later recognition composition and cost uniqueness steps would lack a stable carrier for “indistinguishable traces.” The module does not itself force $\phi$, eight-tick structure, or $D=3$; it only supplies the judgment substrate those results sit on.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)