recognition_irreversible
plain-language theorem explainer
Recognition steps that strictly reduce defect cannot be undone by any later step restoring the original defect value while advancing the tick. Researchers modeling emergent time from discrete ledger updates cite this to establish the thermodynamic arrow. The proof assumes a candidate reverse step, invokes its built-in defect non-increase property, rewrites via the input equality, and obtains an immediate contradiction with linear arithmetic.
Claim. Let $s$ be a recognition step with defect of output strictly less than defect of input. Then no recognition step $r$ exists such that the input snapshot of $r$ equals the output snapshot of $s$ and the defect of the output of $r$ equals the defect of the input of $s$.
background
A recognition step consists of an input ledger snapshot, an output ledger snapshot, a tick advance of exactly one unit, and the inequality that output defect is at most input defect. The defect functional equals the J-cost on positive reals and is non-increasing along successive ticks. In this module time is defined as the ledger tick counter with no background continuum; the arrow of time is the direction in which defect decreases toward its minimum inside each epoch. Upstream results supply the defect definition from LawOfExistence and the fundamental tick as the RS-native time quantum of one.
proof idea
Proof by contradiction. Assume a reverse recognition step exists with matching input and restored defect. Apply the defect_reduce field of that reverse step to obtain a non-strict inequality. Rewrite the input snapshot using the equality hypothesis. Linear arithmetic then contradicts the given strict decrease.
why it matters
The theorem supplies the irreversibility clause inside time_emergence_certificate, which certifies F-004 and F-006 by combining time-as-tick-count, the eight-tick epoch, and one-way recognition. It grounds the framework claim that the arrow of time coincides with the direction of defect decrease, consistent with the eight-tick octave and dimension forcing. No scaffolding remains; the result closes the irreversibility step in the emergence chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.