length_le_of_extends
plain-language theorem explainer
Finite-trace length is monotone under extension: whenever one finite trace extends another, the extended trace is at least as long. Anyone wiring a FormalSystem whose expression order is derivation length cites this fact. The proof unpacks extension as an append witness and inducts on the appended suffix, using the successor inequality on naturals.
Claim. If a finite trace $T$ extends a finite trace $U$ (equivalently, $U$ is $T$ with some finite suffix appended), then $\mathrm{length}(T) \le \mathrm{length}(U)$.
background
In the Primitive Recognition Calculus, a finite trace is a finite sequence of primitive recognition events. Trace extension means one trace is an initial segment of another: there exists a (possibly empty) suffix whose append recovers the longer trace. Length is the usual natural-number count of events in the sequence.
This module builds concrete FormalSystem instances for the inevitability argument: tokens come from a carrier with two distinct primitives, expressions are natural numbers (trace lengths), and expression extension is the ordinary order on lengths. Monotonicity of length under genuine trace extension is the bridge that makes that order well-defined relative to the underlying append structure.
The local import is the FormalSystem interface; the argument itself is pure finite-sequence arithmetic and does not depend on the RS gauge, Clifford bridge, or Hamiltonian evolution operators that appear elsewhere in Foundation.
proof idea
Unpack the extension hypothesis to a witness suffix $V$ with $U = \mathrm{append}(T,V)$. Prove the key lemma that for every suffix $W$, $\mathrm{length}(T) \le \mathrm{length}(\mathrm{append}(T,W))$, by induction on $W$: the empty case is reflexivity (simp); the extend case applies $\mathrm{Nat.le_succ_of_le}$ to the inductive hypothesis and simplifies. Rewrite along the witness equality and instantiate the key lemma at $V$.
why it matters
This is the length-order sanity check used when packaging any two-distinct-primitive carrier as a FormalSystem (ofTwoDistinct), and again when parsing topos theory, full ZFC, HF set theory, and MLTT into that same interface. Downstream docs fix expression extension to be the derivation-length order (m ≤ n); without monotone length under genuine trace extension, that identification would not preserve the intended append geometry of recognition traces.
In the broader Recognition Science foundation, these FormalSystem instances feed the inevitability / embed-δ story: every sufficiently expressive formal system must realize the primitive discrimination structure. The lemma is small bookkeeping, but it is cited at every parse site that equates expression order with length.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.