106structure RecognitionStep where 107 input : LedgerSnapshot 108 output : LedgerSnapshot 109 tick_advance : output.tick.index = input.tick.index + 1 110 defect_reduce : output.defect ≤ input.defect 111 112/-- **Theorem**: Recognition is irreversible. 113 If a step reduces defect from d₁ to d₂ < d₁, there is no step 114 that goes from d₂ back to d₁ while advancing the tick counter, 115 because defect is non-increasing along ticks. -/
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.