Foundation Primitive Recognition Calculus Trace Closure Completed Trace

The completed trace

A completed trace is an infinite ledger: a discrete record of events indexed by every natural number, with no last entry. In the Recognition Science framework, each entry is a distinction act, a primitive operation that marks a separation. The declaration CompletedTrace defines this object as a function from natural numbers to distinction acts, so the trace never stops and never branches. It is the completed form of a finite trace, the kind of record that has a beginning but no end.

The framework proves that every finite prefix of a completed trace is itself a finite trace. The function finitePrefix cuts the infinite ledger at any natural number n, producing the record of the first n acts. Two theorems, prefix_zero and prefix_succ, verify that this cutting behaves correctly: the prefix of length zero is the empty trace, and the prefix of length n+1 extends the prefix of length n by the act at position n. These are definitional facts, true by construction, not empirical claims.

The framework also defines a canonical completed trace, one that repeats the same primitive distinction act at every step. Its every prefix is a finite trace, which the theorem canonical_prefix_exists records. A companion object, the completed orbit ledger, tracks the position of a verifier at each natural-number step; its canonical form sends each index n to the nth position, a fact the framework proves in canonical_toNat.

In Recognition Science, the completed trace is a trace-closure object. The framework labels it with the strength tag traceClosure, meaning it extends finite primitive recognition calculus by closure under infinite iteration, not by adding new axioms. A certificate theorem, trace_closure_certificate, confirms that completed traces and completed orbit ledgers exist and that the canonical orbit verifier is faithful: its position at index n is exactly n.

What the declaration does not claim: it does not assert that any physical process actually produces an infinite ledger. It defines a mathematical object and proves its basic properties. It does not claim that the completed trace is unique, nor that it is the only way to extend finite traces. It does not derive any physical constant or empirical law. The completed trace is a structural primitive, a formal tool for talking about infinite sequences of distinction acts, not a statement about the observable world.

/-- K4.13/R9. A completed trace is an infinite ledger of distinction acts.
This is a trace-closure object, not a finite δ-only trace. -/
structure CompletedTrace where
  actAt : Nat → DistinctionAct

/-- The finite prefix of length `n` cut out of a completed trace. -/
def finitePrefix (S : CompletedTrace) : Nat → Trace
  | 0 => Trace.empty
  | Nat.succ n => Trace.extend (finitePrefix S n) (S.actAt n)

@[simp] theorem prefix_zero (S : CompletedTrace) :
    S.finitePrefix 0 = Trace.empty := by
  rfl

@[simp] theorem prefix_succ (S : CompletedTrace) (n : Nat) :
    S.finitePrefix (Nat.succ n) = Trace.extend (S.finitePrefix n) (S.actAt n) := by
  rfl

@[simp] theorem canonical_toNat (n : Nat) :
    (canonical.positionAt n).toNat = n := by
  exact DistinctionNat.toNat_ofNat n

/-- K4.13. The trace-closure boundary is inhabited and tagged honestly. -/
theorem trace_closure_certificate : TraceClosureCertificate where
  completed_trace_exists := ⟨CompletedTrace.canonical⟩
  canonical_completed_trace_exists := ⟨CompletedTrace.canonical⟩
  completed_orbit_ledger_exists := ⟨CompletedOrbitLedger.canonical⟩
  canonical_orbit_verifier_faithful := CompletedOrbitLedger.canonical_toNat
  strength_tag := rfl

What this page does not claim

The completed trace does not assert that any physical process produces an infinite ledger. The completed trace is not claimed to be unique. The completed trace does not derive any physical constant or empirical law.

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/TraceClosure.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: