Window
plain-language theorem explainer
Window is a structure that records a finite observation interval in the RS tick time, with start tick t0 and length len (len=0 for instantaneous). Measurement and algebra modules cite it when parameterizing cost aggregation or device specs. The definition is a direct structure with decidable equality derived from the two Nat fields.
Claim. A measurement window is a pair $(t_0, l)$ with $t_0, l : ℕ$, where $t_0$ marks the initial tick and $l$ the duration in ticks ($l=0$ denotes an instantaneous sample).
background
The RS-Native Measurement Framework supplies a Lean-first scaffold for observables built on ticks, voxels, coherence and ledger quantities with fundamental time quantum τ₀ = 1. Window supplies the basic discrete interval type used to bound measurements inside this setting. Upstream, Constants.tick states that the fundamental RS time quantum satisfies τ₀ = 1 tick, while the CellularAutomata.Window definition supplies the finite-tape analogue Fin n → CellState that this structure adapts to measurement use.
proof idea
This is a structure definition; the body consists only of the two fields t0 and len together with the deriving DecidableEq clause. No lemmas or tactics are applied.
why it matters
Window is referenced by thirteen downstream declarations, including costCompose_right_cancel (CostAlgebra), paired_preserves_balance (LedgerAlgebra), PBMDeviceSpec (Applied), encodeClause (CellularAutomata) and beat_fraction_irreducible (Gap45.RecognitionBarrier). It supplies the concrete interval object required by the eight-tick octave (T7) and by window-based ledger and cost constructions inside the RS-native measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.