Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.SameDiff

show as:
view Lean formalization →

Defines the admissible same/diff judgment surface on traces (paper items K2.6–K2.8). It packages the equivalence laws for sameness, a consistency predicate, and a substitution rule that any verifier equality judgment must respect. Downstream PRC modules (Kernel, Quotient, TraceLogic, one-primitive) import this surface as the judgment API. Content is definitional plus short algebraic lemmas, not a deep existence proof.

claimAn admissible trace judgment surface: a same-relation on traces that is reflexive, symmetric, and transitive; a consistency predicate (compatible with exclusive same/diff); a respect-same condition; and a substitution rule so that any verifier equality judgment is invariant under same. Covers paper items K2.6–K2.8 in the Primitive Recognition Calculus.

background

Primitive Recognition Calculus (PRC) is the foundation layer that treats recognition events as traces and builds logic from judgments on those traces, before continuum physics is recovered. The parent Basic module supplies the raw trace and judgment vocabulary; this module specializes to the same/diff surface.

Sameness is the equivalence used to identify traces that a verifier cannot distinguish. The siblings encode the standard equivalence laws (refl, symm, trans), a Consistency predicate with a lemma that exclusive same/diff yields consistency, a RespectsSame interface, and a substitute rule tying verifier equality judgments to that equivalence.

Local setting is purely judgmental: no metric, no J-cost, and no forcing-chain constants yet. The surface is the discrete logical substrate later quotiented and kernelized.

proof idea

Definition module with short supporting lemmas, not a single theorem proof. TraceJudgment and the same-relation are introduced as the surface; same_refl, same_symm, and same_trans discharge the equivalence laws. Consistent and consistent_of_exclusive package compatibility of same with exclusive difference. RespectsSame and substitute give the congruence/substitution interface; verifierEqualityJudgment is the equality judgment that must respect same. Argument structure is API assembly plus elementary Prop reasoning from Basic.

why it matters in Recognition Science

This module is the K2.6–K2.8 judgment surface for PRC: without a stable same/diff API, later quotient and kernel constructions have nothing coherent to identify. It is imported by Kernel, PRCOnePrimitive, Quotient, and TraceLogic, which build the one-primitive story, the trace quotient, and the logic of traces on top of this surface.

In the broader Recognition stack it sits below the forcing chain (T0–T8) and the Recognition Composition Law: it does not force J, phi, the eight-tick octave, or D = 3, but it supplies the discrete identity structure those layers eventually act on. Closing or hardening this surface is a prerequisite for any claim that recognition logic is uniquely determined at the trace level.

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)