IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceClosure

   1/-
   2  PrimitiveRecognitionCalculus/TraceClosure.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchors:
   8    K1 (`δ + trace-closure`), R9, K4.13
   9
  10  This module records the first completed-trace boundary. It does not claim
  11  that completed infinity is δ-only. It explicitly carries the
  12  `traceClosure` strength tag.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
  18import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Strength
  19
  20namespace IndisputableMonolith
  21namespace Foundation
  22namespace PrimitiveRecognitionCalculus
  23
  24/-- K4.13/R9. A completed trace is an infinite ledger of distinction acts.
  25This is a trace-closure object, not a finite δ-only trace. -/
  26structure CompletedTrace where
  27  actAt : Nat → DistinctionAct
  28
  29namespace CompletedTrace
  30
  31/-- The finite prefix of length `n` cut out of a completed trace. -/
  32def finitePrefix (S : CompletedTrace) : Nat → Trace
  33  | 0 => Trace.empty
  34  | Nat.succ n => Trace.extend (finitePrefix S n) (S.actAt n)
  35
  36@[simp] theorem prefix_zero (S : CompletedTrace) :
  37    S.finitePrefix 0 = Trace.empty := by
  38  rfl
  39
  40@[simp] theorem prefix_succ (S : CompletedTrace) (n : Nat) :
  41    S.finitePrefix (Nat.succ n) = Trace.extend (S.finitePrefix n) (S.actAt n) := by
  42  rfl
  43
  44/-- The canonical completed trace repeats the primitive distinction act. -/
  45def canonical : CompletedTrace where
  46  actAt := fun _ => DistinctionAct.delta
  47
  48@[simp] theorem canonical_actAt (n : Nat) :
  49    canonical.actAt n = DistinctionAct.delta := by
  50  rfl
  51
  52/-- Every prefix of the canonical completed trace is a finite trace. -/
  53theorem canonical_prefix_exists (n : Nat) :
  54    Nonempty Trace := by
  55  exact ⟨canonical.finitePrefix n⟩
  56
  57end CompletedTrace
  58
  59/-- K4.13. A completed orbit ledger is the infinite sequence of finite
  60δ-orbit positions. This is the natural-number side of trace closure. -/
  61structure CompletedOrbitLedger where
  62  positionAt : Nat → DistinctionNat
  63
  64namespace CompletedOrbitLedger
  65
  66/-- The canonical completed orbit sends verifier index `n` to the `n`th
  67δ-orbit position. -/
  68def canonical : CompletedOrbitLedger where
  69  positionAt := DistinctionNat.ofNat
  70
  71@[simp] theorem canonical_toNat (n : Nat) :
  72    (canonical.positionAt n).toNat = n := by
  73  exact DistinctionNat.toNat_ofNat n
  74
  75theorem canonical_succ (n : Nat) :
  76    canonical.positionAt (Nat.succ n) =
  77      DistinctionNat.succ (canonical.positionAt n) := by
  78  rfl
  79
  80end CompletedOrbitLedger
  81
  82/-- K1/R9. Audit record: completed traces require the trace-closure tag. -/
  83def traceClosureClaim : StrengthClaim where
  84  label := "K4.13_trace_closure_boundary"
  85  tag := StrengthTag.traceClosure
  86  statement := "Completed traces and completed orbit ledgers extend finite PRC by trace closure."
  87
  88/-- K4.13. First trace-closure certificate. -/
  89structure TraceClosureCertificate : Prop where
  90  completed_trace_exists : Nonempty CompletedTrace
  91  canonical_completed_trace_exists : Nonempty CompletedTrace
  92  completed_orbit_ledger_exists : Nonempty CompletedOrbitLedger
  93  canonical_orbit_verifier_faithful :
  94    ∀ n : Nat, (CompletedOrbitLedger.canonical.positionAt n).toNat = n
  95  strength_tag : traceClosureClaim.tag = StrengthTag.traceClosure
  96
  97/-- K4.13. The trace-closure boundary is inhabited and tagged honestly. -/
  98theorem trace_closure_certificate : TraceClosureCertificate where
  99  completed_trace_exists := ⟨CompletedTrace.canonical⟩
 100  canonical_completed_trace_exists := ⟨CompletedTrace.canonical⟩
 101  completed_orbit_ledger_exists := ⟨CompletedOrbitLedger.canonical⟩
 102  canonical_orbit_verifier_faithful := CompletedOrbitLedger.canonical_toNat
 103  strength_tag := rfl
 104
 105end PrimitiveRecognitionCalculus
 106end Foundation
 107end IndisputableMonolith
 108