Foundation Primitive Recognition Calculus Basic Append Assoc

Joining traces

A trace is a finite record of events, built one step at a time. In the Recognition Science framework, the events are primitive distinction acts: each act marks a single side, left or right. A trace is either empty or an existing trace extended by one such act. The operation append joins two traces into one, placing the events of the second after the events of the first.

The declaration append_assoc proves that this joining operation is associative. For any three traces T, U, and V, appending T to U and then appending V gives the same trace as appending T to the result of appending U to V. In symbols: append (append T U) V = append T (append U V). This is a structural property of the record itself, not a claim about what the events mean.

The proof is carried out in a machine-checked library of formal theorems. It proceeds by induction on the structure of the third trace, showing the equality holds for the empty trace and is preserved when a new distinction act is added. The result is tagged as a theorem in the framework's library, meaning it is a proved statement rather than a definition or a hypothesis.

What the declaration does not claim is just as important. It does not say that all traces are the same, or that the order of events never matters. It only says that the way traces are grouped when joined does not change the final record. It also does not claim that the append operation is commutative: joining T to U is not asserted to equal joining U to T. The theorem is about association, not about reordering.

This associativity result is a foundation for later work. It guarantees that the record of events can be built up in pieces without ambiguity about grouping, which is a necessary condition for any larger structure built on traces to be well-defined. The property is a basic algebraic sanity check: the ledger of distinctions behaves predictably under composition.

/-- R4. Trace append is associative. -/
theorem append_assoc (T U V : Trace) :
    append (append T U) V = append T (append U V) := by
  induction V with
  | empty => rfl
  | extend V a ih =>
      simp [append, ih]

/-- K2.4. A finite trace is empty or extended by one distinction act. -/
inductive Trace where
  | empty
  | extend : Trace → DistinctionAct → Trace
  deriving DecidableEq, Repr

/-- Append two traces. This is the syntactic composition operation. -/
def append : Trace → Trace → Trace
  | T, Trace.empty => T
  | T, Trace.extend U a => Trace.extend (append T U) a

What this page does not claim

The theorem does not claim that append is commutative or that the order of events never matters. The theorem does not claim anything about the meaning or interpretation of the distinction acts themselves. The theorem does not establish any property of traces beyond the syntactic grouping of appended records.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Basic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: