Foundation Primitive Recognition Calculus Trace Logic All Elim

What all_elim does

A trace, in this framework, is a finite record of recognition events, a discrete list that can grow as more events are recorded. A trace predicate is a property of such a trace that, once true, stays true when the trace is extended with further events. The declaration all_elim is a rule of inference in the framework's machine-checked library of formal theorems: if a predicate holds for every trace in a family indexed by some type, then it holds for any particular trace you name. In symbols, from a proof of (all P).holds T and a choice of index a, it derives (P a).holds T. This is the standard elimination rule for universal quantification, adapted so that it works inside the stable-predicate setting.

The rule matters because it is one of the basic moves that let the framework build larger proofs from smaller ones. Without it, a statement like "every trace with property X also has property Y" could not be applied to a concrete trace, and the whole edifice of derived theorems would stall. The declaration is part of a first pass at a trace logic, a deliberate foundation for later work. It is a theorem in the formal library, proved by applying the universal witness directly, with no hidden assumptions beyond the ambient type theory.

In Recognition Science, the framework models physical structure as arising from a ledger of recognition events, and this logic is a step toward making that modeling precise. The rule itself is modest: it establishes a basic logical operation, not any physical law. It does not claim that any particular trace exists, that any predicate is satisfiable, or that the framework's larger goals are achieved. It is a tool, and its value lies in being a correct and verified one.

theorem all_elim {α : Type} {P : α → TracePredicate} {T : Trace}
    (h : (all P).holds T) (a : α) :
    (P a).holds T := by
  exact h a

What this page does not claim

It does not prove that any particular trace exists or that any predicate is satisfiable. It does not establish any physical law or constant. It does not define the semantics of the trace logic beyond the stable-predicate structure.

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: