Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic

show as:
view Lean formalization →

Defines the primitive distinction act δ and the discrete trace calculus built from it: sides, endpoints, finite traces, and the append monoid. Recognition Science treats distinction as the sole generative operation before cost, time, or geometry appear. Downstream PRC modules import this vocabulary to state uniqueness of the primitive, orbit structure, and seam closure. The file is almost entirely inductive definitions plus elementary monoid lemmas.

claimThe module introduces the primitive distinction act $\delta$, a two-sided choice type $\mathrm{Side}$, endpoints of a distinction, and finite traces $T$ formed by successive steps. Trace concatenation $\mathrm{append}$ is an associative monoid operation with empty unit, and the extension relation $\mathrm{Extends}$ is the reflexive prefix order induced by append.

background

Recognition Science begins below cost functionals and spacetime. Before the J-cost, the eight-tick octave, or $D=3$, one needs a bare notion of making a cut: something is distinguished from something else. This module (K2.1 in the foundation numbering) packages that cut as the object-level primitive $\delta$, called the distinction act.

From $\delta$ one builds a small discrete calculus. A side labels which pole of a cut is named; an endpoint records where a cut lands; a trace is a finite word of successive distinction steps. Concatenation of traces is ordinary list append, so the empty trace is a two-sided unit and append is associative. Extension is the induced prefix relation: one trace extends another when the latter is an initial segment of the former.

The only import beyond Mathlib is the Strength layer of the same PRC stack, which supplies the ambient strength or intensity language against which bare distinctions are later compared. No continuum, metric, or cost appears here.

proof idea

This is a definition module, not a theorem file. Inductive or structure definitions introduce DistinctionAct, Side, Endpoint, and Trace. The step and append operations are defined by pattern matching on traces; the four monoid identities (append_empty, empty_append, append_extend, append_assoc) are routine inductions on list structure. Extends and extends_refl package the reflexive prefix order. There is no deep proof content beyond those elementary lemmas.

why it matters in Recognition Science

Every later Primitive Recognition Calculus development imports this file as its vocabulary layer. Kernel, Orbit, PRCOnePrimitive, SameDiff, and TraceClosure all build uniqueness, dynamical, and closure statements on top of $\delta$-traces. SeamClosure.Reference likewise consumes the same primitives when sealing identification seams. In the broader forcing chain this sits beneath T5–T8: without a well-typed distinction act one cannot even state the Recognition Composition Law or force $\varphi$ and the eight-tick period. The module therefore anchors the object-level starting point of the RS foundation rather than a derived physical claim.

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)