stop
plain-language theorem explainer
The stop definition returns the terminal tick of a discrete measurement window by adding its start tick to its length. Researchers modeling RS-native observables or classical fluid bridges would cite it when tracking window endpoints in tick arithmetic. The implementation is a direct one-line field sum with no lemmas or reductions required.
Claim. For a measurement window with start tick $t_0$ and length $l$, the terminal tick is given by $t_0 + l$.
background
The RS-Native Measurement Framework supplies a lightweight scaffold for tick-based observables with $τ_0 = 1$, separating core theory from optional external calibrations. A measurement window is a finite discrete interval specified by its starting tick and length in ticks, with zero length denoting an instantaneous record. This module emphasizes explicit protocols so that windowing choices remain visible rather than hidden in arbitrary coarse-graining.
proof idea
One-line definition that directly sums the start-tick and length fields of the window structure.
why it matters
The definition supplies endpoint arithmetic used by the bridge construction in ClassicalBridge.Fluids.CPM2D, which packages discrete states with defect and energy interpretations. It occupies a basic position in the measurement seam of the Recognition Science framework, supporting T7 tick-octave primitives without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.