Foundation Primitive Recognition Calculus Trace Logic Top Intro

The trivial truth

In classical logic, truth is a property of a proposition that holds regardless of circumstances. In the Recognition Science framework, a proposition is instead a predicate on traces, which are discrete records of events that only ever grow by extension. A proposition is then not a static assertion but a claim about every possible future of the record. The framework's declaration top_intro establishes the most basic fact of this system: the proposition that is true at every trace, the one that holds no matter what the record contains, is simply the statement that the record exists. It is the logical constant top, and it is true at every trace by definition.

The declaration is a theorem in the framework's machine-checked library of formal theorems. It states that for any trace T, the proposition top holds at T. The proof is immediate, a single step of trivial reasoning. This is not a deep result, but it is a foundational one. It is the first brick in a logic where every proposition must be stable under extension: if a proposition holds at a trace, it must also hold at any longer trace that extends it. top satisfies this requirement vacuously, since it holds everywhere. The declaration top_intro is the introduction rule for this constant, the rule that says you may assert top at any point in the record.

The importance of top_intro is not in what it proves, but in what it makes possible. It is the base case for a system of logical connectives, each of which is also defined to be stable under trace extension. Conjunction, disjunction, implication, negation, and quantifiers are all built on this same foundation. The framework proves that each of these connectives, when applied to stable predicates, yields another stable predicate. This is the first pass of a trace logic, a logic where the central notion is not truth in a static world, but persistence along a growing record. top_intro is the anchor of that system, the trivial truth that everything else hangs from.

In Recognition Science, this is the starting point for a much larger project. The framework aims to derive physical structure from the cost of recognition events, and this trace logic is the substrate on which that derivation is built. The declaration top_intro does not, by itself, establish any physical law or any constraint on the cost function. It is a purely logical statement about the framework's own formalism. It says only that the always-true proposition is true, a tautology in the most literal sense. Its role is to be the first step in a chain, the trivial foundation on which the framework's more substantive claims are constructed.

theorem top_intro (T : Trace) :
    top.holds T := by
  trivial

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

/-- Truth is the stable predicate that holds at every trace. -/
def top : TracePredicate where
  holds := fun _ => True
  stable := by
    intro _T _U _hTU _h
    trivial

What this page does not claim

The declaration top_intro does not establish any physical law or constraint on the cost function. The stability of trace predicates does not imply that all propositions are decidable or that the logic is classical. The trace logic does not yet provide a semantics for the cost function J(x).

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: