timeOK
plain-language theorem explainer
timeOK defines the predicate for temporal admissibility of an integer tick index n under eight-tick gating parameters p. Researchers constructing feasibility conditions in discrete measurement models cite this when intersecting angular and temporal constraints. The definition reduces the check to residue-class membership after mapping n modulo 8 through integer-to-natural conversion.
Claim. The temporal admissibility predicate holds for integer tick index $n$ and eight-tick parameters $p$ precisely when the residue class of $n$ modulo 8, converted to an element of Fin 8, belongs to the admissible window set of $p$.
background
The module abstracts discrete sampling via eight-tick windows and defines a feasibility predicate that combines an angular threshold with temporal admissibility. EightTickParams is the structure carrying a phase in Fin 8 together with a nonempty set of admissible windows in Fin 8. Upstream, toNat supplies the forward map from logical iteration counts to natural numbers that supports the residue computation.
proof idea
The definition is a direct one-line computation. It forms the class cls as (Int.toNat (Int.emod n 8)).toFin and returns the proposition that cls lies in the window field of the EightTickParams structure p.
why it matters
timeOK supplies the temporal half of the feasible predicate. Downstream theorems such as exists_feasible_if_angleOK_and_time_slot invoke it to conclude existence of a feasible event once both angleOK and a permitted time slot are given. It implements the eight-tick octave (T7) of the forcing chain, enabling combined geometric-temporal admissibility checks in the measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.