Foundation Primitive Recognition Calculus Trace Closure Trace Closure Claim

Trace closure

A completed trace is an infinite ledger, a discrete record of events, of distinction acts: at every natural number step, it records one act of drawing a distinction. The framework's library, a machine-checked collection of formal theorems, defines a completed trace as a function from natural numbers to distinction acts, and it defines a completed orbit ledger as the matching infinite sequence of finite orbit positions. The claim named traceClosureClaim is a labeled statement, tagged with the strength tag for trace closure, that says: completed traces and completed orbit ledgers extend finite primitive recognition calculus by trace closure.

What the claim establishes is modest and precise. The library proves a certificate, a formal witness, that the boundary is inhabited: there exists a completed trace, there exists a canonical completed trace that repeats the primitive distinction act at every step, there exists a completed orbit ledger, and the canonical orbit ledger is faithful in the sense that its position at index n maps back to the natural number n. These are existence and consistency facts. The certificate also records that the claim carries the trace-closure tag, so the boundary is tagged honestly.

What the claim does not claim is just as important. It does not assert that any particular physical process produces an infinite ledger. It does not assert that the canonical completed trace is the only completed trace, or that trace closure forces any particular structure beyond the existence of these infinite objects. It does not prove that the natural numbers exist; it assumes them as the index set. The claim is a boundary marker: it names the point where finite traces are extended to infinite ones, and it provides a machine-checked witness that the extension is coherent.

In Recognition Science, this matters because the framework's larger results, such as the forcing chain that derives the golden ratio and three spatial dimensions, depend on moving from finite recognition records to completed, infinite ones. The trace closure claim is the hinge: it certifies that the move is available and that the framework's own strength tags mark it as such. The reader can now see that the framework does not silently assume infinite records; it declares the assumption and proves a certificate for it.

/-- 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

/-- 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 claim does not assert that any physical process produces an infinite ledger. The claim does not prove that the canonical completed trace is unique. The claim does not derive the existence of natural numbers; it assumes them as the index set.

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: