stop
plain-language theorem explainer
The declaration defines stop on a discrete measurement window as the sum of its start tick and length, yielding the terminal tick of the interval. Measurement protocol authors in the RS-native framework cite it when closing observation windows for ledger observables. The implementation is a direct one-line definition with no lemmas or reductions.
Claim. For a measurement window $w$ with start tick $t_0$ and length $l$, define stop$(w) := t_0 + l$.
background
The module supplies a Lean-first measurement scaffold for Recognition Science with core observables built from ticks, voxels, and ledger entries at $τ_0 = 1$. A Window is the structure holding a start tick $t_0$ and length $l$ (both natural numbers) that represents a finite discrete observation interval. The surrounding design requires every measurement to carry an explicit protocol and falsifiers so that windowing choices remain visible rather than hidden.
proof idea
Direct definition that returns the arithmetic sum of the two fields of the Window structure. No upstream lemmas are invoked; the body is the primitive operation itself.
why it matters
The definition supplies the terminal tick needed by downstream bridge constructions such as the CPM2D bridge, which records defectMeaning and energyMeaning for discrete states. It implements the tick-based time coordinate required by the RS-native units and the eight-tick octave structure. It leaves open the integration of these finite windows with continuous calibration outside the core module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.