Foundation Primitive Recognition Calculus Trace Closure Completed Orbit Ledger

The completed orbit ledger

A completed orbit ledger is an infinite list of positions. In the Recognition Science framework, a position is a point in a discrete counting structure called a distinction act, which is the primitive event of marking one thing as different from another. The ledger assigns to every natural number n a position, so it is a function from the counting numbers to the set of positions. The canonical example sends each number n to the n-th position, meaning the ledger simply counts upward forever.

The definition lives in a machine-checked library of formal theorems. The library proves that the canonical ledger is faithful: the position at index n always converts back to the number n. It also proves that every finite prefix of the canonical completed trace, which is the companion infinite sequence of distinction acts, is a finite trace. These are structural facts about the objects, not claims about the physical world.

In Recognition Science, the completed orbit ledger is the natural-number side of trace closure. Trace closure is the operation that extends a finite record of events into an infinite one. The framework models this extension by defining the ledger as an infinite sequence, and it tags the claim that completed traces extend finite ones with a specific strength label. The label marks the statement as a trace-closure boundary, meaning it is a definitional extension of the calculus, not a theorem forced by the cost function.

What the declaration does not claim is as important as what it does. It does not claim that the infinite ledger exists in any physical sense; it merely defines a mathematical object and proves its internal consistency. It does not claim that the completed ledger is unique, since other infinite sequences of positions could satisfy the same structure. It does not claim that trace closure derives any physical constant, dimension, or particle property. The certificate theorem only shows that the structures are inhabited and that the canonical example behaves correctly.

The practical consequence is a clean boundary in the framework. Researchers can build on completed traces and ledgers as infinite objects without pretending the framework has proved their physical reality. The declaration gives a precise, machine-checked definition of what an infinite recognition record would be, and it honestly labels the step as a trace-closure extension, not a forced result.

/-- K4.13. A completed orbit ledger is the infinite sequence of finite
δ-orbit positions. This is the natural-number side of trace closure. -/
structure CompletedOrbitLedger where
  positionAt : Nat → DistinctionNat

/-- The canonical completed trace repeats the primitive distinction act. -/
def canonical : CompletedTrace where
  actAt := fun _ => DistinctionAct.delta

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

/-- K1/R9. Audit record: completed traces require the trace-closure tag. -/
def traceClosureClaim : StrengthClaim where
  label := "K4.13_trace_closure_boundary"
  tag := StrengthTag.traceClosure
  statement := "Completed traces and completed orbit ledgers extend finite PRC by trace closure."

/-- 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 orbit ledger is not claimed to be physically real, only mathematically defined. The declaration does not claim uniqueness of the infinite ledger. Trace closure does not derive any physical constant or dimension.

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: