timeOK
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not fix concrete phase or window contents inside EightTickParams.
- Does not incorporate the geometric angleOK threshold.
- Does not assert existence of any n satisfying the predicate for given p.
- Does not address continuous time or periods other than eight ticks.
formal statement (Lean)
32def timeOK (n : ℤ) (p : EightTickParams) : Prop :=
proof body
Definition body.
33 let cls : Fin 8 := (Int.toNat (Int.emod n 8)).toFin
34 cls ∈ p.window
35
36/-- Geometric admissibility (angle threshold). -/