Foundation Primitive Recognition Calculus Trace Logic

Trace Logic

Trace logic is a way of making statements about a trace (a discrete record of events that can be extended by adding more events at the end). Its core rule is persistence: if a proposition holds for a record, it must continue to hold for every longer record that extends it. This is not an extra assumption; it is built into the definition of what a proposition is. The module defines a trace predicate as a property of traces that is stable under extension, so a claim made at one stage of a record cannot be undone by later growth.

The logic then provides the standard connectives: truth holds at every trace, falsehood holds at none, conjunction and disjunction work pointwise, and implication is defined as persistence along every future extension. Negation is implication into falsehood. Quantification ranges over a verifier-indexed family of predicates, where the index is bookkeeping for the verifier and stability remains a finite-trace theorem. Each connective is proved to preserve stability, so the whole language stays inside the class of persistent predicates.

This design matters because it gives a logic that is sound for a process that only ever adds information. A predicate that holds now cannot be invalidated by later events. The module proves introduction and elimination rules for each connective, and a certificate theorem packages the whole first pass as a single target: the structure TraceLogicCertificate is inhabited, meaning the first trace-logic pass is complete.

In Recognition Science, this is the foundation for later steps: the framework's cost function, its uniqueness theorem, and the forcing chain that derives constants all build on a ledger of recognition events. Trace logic supplies the language in which those later claims are stated. It is a first pass, not the final one; the certificate is a milestone, and the framework's own library records it as such.

/-- A proposition in the first PRC logic pass is a predicate on finite traces
that persists under trace extension. -/
structure TracePredicate where
  holds : Trace → Prop
  stable :
    ∀ {T U : Trace}, Trace.Extends T U → holds T → holds U

/-- Conjunction of stable trace predicates. -/
def and (P Q : TracePredicate) : TracePredicate where
  holds := fun T => P.holds T ∧ Q.holds T
  stable := by
    intro T U hTU h
    exact ⟨P.stable hTU h.1, Q.stable hTU h.2⟩

/-- Disjunction of stable trace predicates. -/
def or (P Q : TracePredicate) : TracePredicate where
  holds := fun T => P.holds T ∨ Q.holds T
  stable := by
    intro T U hTU h
    cases h with
    | inl hP => exact Or.inl (P.stable hTU hP)
    | inr hQ => exact Or.inr (Q.stable hTU hQ)

/-- Implication is persistence along every future extension of the current
trace. This makes implication itself stable under extension. -/
def imp (P Q : TracePredicate) : TracePredicate where
  holds := fun T =>
    ∀ U : Trace, Trace.Extends T U → P.holds U → Q.holds U
  stable := by
    intro T U hTU h V hUV hPV
    exact h V (Trace.extends_trans hTU hUV) hPV

/-- Negation is implication into falsehood. -/
def not (P : TracePredicate) : TracePredicate :=
  imp P bottom

theorem trace_logic_certificate : TraceLogicCertificate where
  proposition_surface := ⟨TracePredicate.top⟩
  truth_intro := TracePredicate.top_intro
  conjunction_intro := by
    intro P Q T hP hQ
    exact TracePredicate.and_intro hP hQ
  conjunction_left := by
    intro P Q T h
    exact TracePredicate.and_left h
  conjunction_right := by
    intro P Q T h
    exact TracePredicate.and_right h
  disjunction_left := by
    intro P Q T hP
    exact TracePredicate.or_inl hP
  disjunction_right := by
    intro P Q T hQ
    exact TracePredicate.or_inr hQ
  implication_elim := by
    intro P Q T U himp hTU hP
    exact TracePredicate.imp_elim himp hTU hP
  negation_elim := by
    intro P T U hn hTU hP
    exact TracePredicate.not_elim hn hTU hP
  universal_intro := by
    intro α P T h
    exact TracePredicate.all_intro h
  universal_elim := by
    intro α P T h a
    exact TracePredicate.all_elim h a
  existential_intro := by
    intro α P T a h
    exact TracePredicate.exists_intro a h
  persistence := by
    intro P T U hTU hP
    exact TracePredicate.persists hTU hP
  strength_tag := rfl

What this page does not claim

This module does not derive the cost function or any constants; it only sets up the logic layer. The certificate is a milestone, not a final theorem; later passes may extend it.

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