Window
plain-language theorem explainer
A discrete measurement window in Recognition Science is a pair of natural numbers giving the starting tick and duration in fundamental time quanta. Measurement and complexity researchers cite it when defining protocols for observables or cellular automata encodings. The definition is a direct record type with decidable equality derived automatically.
Claim. A measurement window is a pair $(t_0, L)$ with $t_0, L$ natural numbers, where $L=0$ denotes an instantaneous observation, equipped with decidable equality.
background
The RS-native measurement module treats time as discrete ticks with fundamental quantum $τ_0=1$ from Constants.tick. It separates core RS concepts (ticks, voxels, ledger observables) from optional SI calibrations. Upstream the CellularAutomata module supplies a distinct Window type as a finite tape segment (Fin n → CellState) used for local update rules.
proof idea
Direct structure definition introducing the two Nat fields with an automatically derived DecidableEq instance. No lemmas or tactics are invoked.
why it matters
The structure supplies the basic unit for windowed measurements that appear in cost-composition cancellation, ledger balance preservation, photobiomodulation device specifications, and SAT-clause encodings. It supports the explicit-protocol requirement of the RS measurement scaffold and aligns with the eight-tick octave by permitting lengths that are multiples of 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.