Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic

show as:
view Lean formalization →

Defines the primitive distinction act δ and the basic combinatorial objects of Primitive Recognition Calculus: sides, endpoints, finite traces, and the extends relation. Anyone working on K2-level foundation or seam closure cites this module for the raw vocabulary. It is a pure definition layer: inductive types, list-style append lemmas, and reflexivity of extension, with no deep theorems.

claimThe module introduces the primitive distinction act $\delta$ (K2.1), together with sides, endpoints, finite traces of successive distinctions, the step and append operations on traces, and the reflexive extends relation on traces.

background

Primitive Recognition Calculus sits at the base of the Recognition Science foundation stack. Before costs, forcing chains, or the eight-tick octave, one needs a bare object-level act of making a distinction. The module doc labels this K2.1: the primitive distinction act, written $\delta$ at the object level.

The vocabulary is combinatorial. A distinction has two sides and produces endpoints; a trace is a finite sequence of such acts. Append and step build longer traces from shorter ones, with the usual monoid laws (empty unit, associativity). Extends is the prefix-style order on traces, introduced so later modules can talk about refinement and closure without committing to a metric or a cost functional yet.

The only import beyond Mathlib is the Strength submodule, which supplies the ambient strength or intensity language that later kernels and orbits will use. Nothing here yet mentions $J$, $\phi$, or the Recognition Composition Law.

proof idea

This is a definition module, not a theorem module. The body introduces inductive or structure types for the distinction act, sides, endpoints, and traces, then proves elementary list-style facts: append with empty is a unit on both sides, append is associative, and extends is reflexive. There is no forcing argument and no appeal to uniqueness of $J$.

why it matters in Recognition Science

Every subsequent Primitive Recognition Calculus development imports this file as the raw alphabet. Downstream modules Kernel, Orbit, PRCOnePrimitive, SameDiff, and TraceClosure all build on $\delta$, traces, and extends; SeamClosure.Reference pulls the same vocabulary into the seam-closure layer. Without a fixed object-level distinction act, later claims that there is one primitive, that same-difference relations close, or that orbits are well-defined would have no carrier. In the broader RS chain this is pre-T5 infrastructure: it does not force $J$ or $\phi$, but it is the substrate on which those forcing steps eventually act.

scope and limits

used by (6)

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 (18)