Foundation Primitive Recognition Calculus Basic Trace

The Trace

A trace is a finite, ordered record of distinction acts. In the Recognition Science framework, a distinction act is the primitive event of marking a difference, and a trace is the sequence built from such acts. The framework defines a trace as either empty or as a previous trace extended by one distinction act. This recursive definition gives every trace a clear structure: it is a list, and its length is the number of acts it contains.

The framework proves basic properties of this structure. Appending two traces is associative, meaning the order of grouping does not change the result. The empty trace acts as a neutral element for this operation. One trace extends another when the first is the second followed by some additional suffix. This extension relation is reflexive, every trace extends itself, and transitive, if one trace extends a second and the second extends a third, then the first extends the third. These are the algebraic facts the declaration establishes.

In Recognition Science, the trace is the ledger of recognition events. It is the discrete record that the framework's later results build upon. The framework models a sequence of primitive acts, and the theorems about appending and extending traces are the groundwork for that model.

The declaration does not claim that a trace is a physical object or that it exists in space and time. It does not claim that the framework's later results, such as the forcing of three spatial dimensions, follow from the trace alone. The trace is a syntactic structure, a definition, and the theorems about it are about that structure's formal properties.

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

/-- 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.5. `Extends T U` means `U` is `T` followed by some suffix trace. -/
def Extends (T U : Trace) : Prop :=
  ∃ V : Trace, append T V = U

/-- R4. Trace extension is reflexive. -/
theorem extends_refl (T : Trace) :
    Extends T T := by
  exact ⟨Trace.empty, rfl⟩

/-- R4. Trace extension is transitive. -/
theorem extends_trans {T U V : Trace}
    (hTU : Extends T U) (hUV : Extends U V) :
    Extends T V := by
  rcases hTU with ⟨A, hA⟩
  rcases hUV with ⟨B, hB⟩
  refine ⟨append A B, ?_⟩
  rw [← append_assoc, hA, hB]

What this page does not claim

The trace is a physical object or exists in space and time. The framework's later results, such as the forcing of three spatial dimensions, follow from the trace alone. The trace definition provides a complete model of recognition.

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: