IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceClosure
Completed traces formalize infinite ledgers of distinction acts in Primitive Recognition Calculus, closing finite δ-traces to infinite limits (K4.13/R9). Researchers on PRC kernel structure, native cost uniqueness, or real-Cauchy completion cite CompletedTrace, canonical prefixes, and TraceClosureCertificate. The module is definitional packaging: finite-prefix constructors, canonical embeddings, orbit ledgers, and a closure claim certificate over Basic/Orbit/Strength data.
claimA completed trace is an infinite ledger of distinction acts (not a finite $\delta$-only path). Finite prefixes of length $n$ embed canonically into that ledger; successor and evaluation lemmas relate the $n$ and $n+1$ truncations. A completed orbit ledger is the orbit-level analogue. A trace-closure certificate asserts that every such orbit ledger admits a completed-trace presentation.
background
Primitive Recognition Calculus builds recognition from successive distinction acts. The imported Basic, Orbit, and Strength modules supply finite traces, act orbits, and strength measures on those finite objects.
This module lifts the finite layer to completed (infinite) traces. Per the module note, a completed trace is an infinite ledger of distinction acts: a trace-closure object, not a finite $\delta$-only trace. Finite prefixes are recovered by truncation; a canonical map sends any finite prefix into the completed ledger and is compatible with acting at a step and with the natural-number indexing of the ledger. CompletedOrbitLedger is the same closure idea at orbit granularity.
The setting is foundation-layer PRC, upstream of kernel statements, native cost uniqueness, and real-Cauchy arguments that consume closed ledgers rather than open finite paths.
proof idea
This is a definition and certificate module, not a deep analytic argument. It introduces CompletedTrace and finitePrefix with base and successor rules (prefix_zero, prefix_succ), a canonical embedding with act-at, toNat, successor, and prefix-existence lemmas, plus CompletedOrbitLedger. The closure statement is packaged as traceClosureClaim together with TraceClosureCertificate. Supporting lemmas are elementary inductive or definitional facts over the finite orbit and strength data imported from Orbit and Strength.
why it matters in Recognition Science
Kernel, PRCNativeCostUniqueness, and RealCauchy all import this module. Closed infinite ledgers are the objects on which kernel structure is stated; native cost uniqueness identifies the cost functional on completed recognition paths rather than open finite $\delta$-traces; RealCauchy passes from discrete completed ledgers toward real limits. The K4.13/R9 label marks the paper step that replaces finite traces by their closures. In the broader RS stack, infinite ledgers are the carriers on which later J-cost, RCL, and $\phi$-ladder structure act, though those landmarks are not proved here.
scope and limits
- Does not prove uniqueness of the PRC native cost functional.
- Does not construct real-analytic Cauchy limits of ledgers.
- Does not derive J-uniqueness or the Recognition Composition Law.
- Does not force phi, eight-tick period, or D = 3.
- Does not extract masses, alpha, or other physical constants from traces alone.
- Does not replace Orbit/Strength finite data; it only closes them.
used by (3)
depends on (3)
declarations in this module (13)
-
structure
CompletedTrace -
def
finitePrefix -
theorem
prefix_zero -
theorem
prefix_succ -
def
canonical -
theorem
canonical_actAt -
theorem
canonical_prefix_exists -
structure
CompletedOrbitLedger -
theorem
canonical_toNat -
theorem
canonical_succ -
def
traceClosureClaim -
structure
TraceClosureCertificate -
theorem
trace_closure_certificate