Gregory Lacefield

Provenance-Tracked State Estimation

A non-collapsible four-channel architecture — formally proven, adversarially tested, with a real vulnerability found and closed.

Problem

Most state-estimation systems can't prove their internal signals haven't been silently rewritten after the fact — no structural guarantee, just trust.

Approach

Four channels, one-way write dependency, proven non-collapsible: a later signal can never rewrite an earlier one. Checked by proof, then checked again by trying to break it.

Evidence

A real gap between the proof and the first implementation was found — and closed. See below.

The Proof Full text, current version — three theorems, checked line by line. A Real Vulnerability, Found & Closed Adversarial testing found a real gap between proof and implementation. Fixed, verified. How This Lab Stays Rigorous Eight verification rules, each with a real example of the error it caught. Full Lab Notebook →