RecognitionStep
plain-language theorem explainer
RecognitionStep encodes a one-step ledger update in which the tick index advances by one while defect is non-increasing. Researchers formalizing the arrow of time in Recognition Science cite this structure when establishing irreversibility of recognition events. The declaration is introduced directly as a four-field structure whose fields capture the input snapshot, output snapshot, tick increment, and defect monotonicity.
Claim. A recognition step is a pair of ledger snapshots $(s_1, s_2)$ such that the tick index of $s_2$ equals the tick index of $s_1$ plus one and the defect of $s_2$ is at most the defect of $s_1$, where a ledger snapshot consists of a tick together with a nonnegative real defect value.
background
The TimeEmergence module identifies time with the discrete tick counter on the ledger and derives the arrow of time from monotonic decrease of defect. A LedgerSnapshot is a state at a given tick carrying a defect value; the defect functional equals the J-cost from the Law of Existence. The module states the core results for F-004 and F-006: time equals tick count with no background parameter, and recognition is one-way because defect cannot increase along the tick sequence. Upstream, defect x is defined as J x and tick is the fundamental quantum τ₀ = 1; the CellularAutomata.step supplies the local update that produces successor states.
proof idea
The declaration is a structure definition that introduces the four fields directly; no theorem or tactic is involved.
why it matters
RecognitionStep supplies the witness used by recognition_irreversible and time_emergence_certificate to prove that recognition cannot be reversed while advancing the tick. It realizes the module claim that recognition is a one-way operation and supplies the monotonicity needed for the arrow of time. The structure is referenced by TimeAsOrbit theorems that equate the tick orbit to the natural-number object. It connects to the eight-tick epoch (T7) as the minimal complete cycle forced by D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.