Window
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not enforce any relation between start tick and length beyond membership in Nat.
- Does not require window length to be a multiple of 8 or 45.
- Does not embed protocol or falsifier data.
- Does not define arithmetic or composition operations on windows.
formal statement (Lean)
70structure Window where
71 /-- Start tick. -/
72 t0 : Nat
73 /-- Window length in ticks (0 = instantaneous). -/
74 len : Nat
75 deriving DecidableEq
76
77namespace Window
78