RecognitionStep
plain-language theorem explainer
RecognitionStep records a single ledger update from one snapshot to the next that advances the discrete tick index by exactly one while keeping defect non-increasing. Researchers formalizing emergent time and the arrow of time from recognition processes cite this structure as the atomic transition rule. It is introduced directly as a four-field structure whose fields encode the update constraints without further proof obligations.
Claim. A RecognitionStep is a pair of ledger snapshots $s$ and $s'$ such that the tick index satisfies $s'.tick.index = s.tick.index + 1$ and the defect satisfies $s'.defect ≤ s.defect$, where defect is the recognition cost functional on the snapshot.
background
The TimeEmergence module identifies time with the discrete tick counter on the ledger and derives its direction from monotonic defect decrease. A LedgerSnapshot packages a Tick together with a nonnegative real defect value; the defect functional itself is the J-cost from the Law of Existence, which equals J(x) for positive x and vanishes at unity. The fundamental tick is normalized to 1 in RS-native units, and the cellular-automata step operation supplies the local update rule that produces global ledger transitions.
proof idea
This declaration is a structure definition that directly bundles the input and output snapshots with the two required constraints on tick advancement and defect non-increase. No separate proof body or tactic steps are needed; the four fields constitute the definition.
why it matters
RecognitionStep supplies the atomic object for the arrow-of-time results, feeding directly into recognition_irreversible, time_emergence_certificate, and the TimeAsOrbitCert construction that equates the tick orbit with the natural-number object. It implements the one-way character of recognition stated in the module doc-comment and sits inside the eight-tick epoch (T7) and three-dimensional forcing (T8) by providing the update step within each epoch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.