length_extend
plain-language theorem explainer
Extending a finite recognition trace by one distinction act raises its length by exactly one. Workers in the primitive recognition calculus (K2) cite this as the basic length recurrence on traces. The proof is pure definitional reflexivity from the recursive clause of length.
Claim. For every finite trace $T$ and every distinction act $a$, the length of the one-step extension of $T$ by $a$ equals the successor of the length of $T$: $\mathrm{length}(T\mathbin{::}a)=\mathrm{succ}(\mathrm{length}(T))$.
background
In the primitive recognition calculus, a distinction act is the atomic object-level generator $\delta$ (K2.1). A finite trace is the free inductive structure built from the empty trace by successive one-step extensions by distinction acts (K2.4): empty, or extend previous trace by one act.
Length is the Nat-valued measure of that structure: the empty trace has length 0, and each extension increments length by the successor. The same inductive spine underlies the arithmetic-from-logic successor, so length is the recognition-side count of how many distinction acts have been recorded.
This module sits at the foundation layer that turns recognition acts into discrete combinatorial objects before cost, forcing, or geometry enter.
proof idea
One-line definitional proof. Length is defined by pattern match: on Trace.extend T _ it returns Nat.succ (length T). The goal is literally that defining equation, so rfl closes it. Marked @[simp] so later rewrites unfold extension length automatically.
why it matters
This is the elementary length law for K2 traces. The immediately following comment previews K2.12: the length of the $n$th orbit trace is $n$. Without a simp-friendly successor identity, orbit-length bookkeeping and any later comparison of traces to eight-tick or ladder indices would need manual unfolding.
No downstream consumers are wired yet in the graph, so the lemma is infrastructure rather than a forcing-chain step. It does not touch T5–T8, RCL, or the mass ladder; it only locks the discrete counting of distinction acts that those layers will later quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.