DistinctionAct
plain-language theorem explainer
The primitive distinction act is a singleton type whose only inhabitant is δ. It is the atomic recognition event from which every finite trace is built by successive extension. Anyone working in the Primitive Recognition Calculus cites it as the generator of Trace and of one-step extension. The declaration is a one-constructor inductive with decidable equality and a printer.
Claim. There is a type of distinction acts containing exactly one element $\delta$, called the primitive distinction act (K2.1).
background
The Primitive Recognition Calculus begins with a single atomic event: the act of drawing a distinction. At the object level that act is written $\delta$. The present declaration packages $\delta$ as a Lean inductive with one constructor, so that later constructions can quantify over acts without smuggling in extra structure.
Finite histories are then built by adjoining acts one at a time. The sibling inductive Trace is either empty or an extension of a prior trace by one distinction act; the one-step map simply extends by $\delta$. Downstream, completed (bi-infinite) traces are maps from $\mathbb{N}$ into this same act type, and the canonical completed trace is the constant map at $\delta$.
The module sits in the Foundation layer of Recognition Science, before cost functionals and the forcing chain are applied. The act type itself carries no metric or cost data; those enter only when traces are interpreted through the J-cost and the Recognition Composition Law.
proof idea
Pure definition: a one-constructor inductive DistinctionAct with sole constructor delta, deriving DecidableEq and Repr. There is no proof obligation beyond the inductive declaration itself.
why it matters
This is K2.1, the seed of the entire Primitive Recognition Calculus. Every finite trace is empty or extended by a distinction act; the one-step operator is extension by $\delta$; append and length lemmas are stated for arbitrary acts of this type. Trace closure builds the canonical completed trace as the constant sequence of $\delta$, and seam-closure generation reuses the same act. Without a singleton act type there is no discrete generator for the eight-tick octave or for later forcing of $D=3$. The declaration is scaffolding-free infrastructure: it does not itself force uniqueness of $\delta$ from the J-cost, but it supplies the object that later uniqueness and cost theorems act upon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.