EightTickParams
plain-language theorem explainer
EightTickParams packages a phase index in the eight-tick cycle with a nonempty subset of admissible time slots. Measurement modelers cite it when parameterizing temporal admissibility for events that must also satisfy an angular threshold. The declaration is a plain structure definition with three fields and no proof obligations.
Claim. A structure consisting of a phase index $p :$ Fin $8$, a nonempty subset $W$ of admissible slots in the eight-tick cycle, and a proof that $W$ is nonempty.
background
The module defines temporal gating over the eight-tick octave. The upstream tick constant supplies the fundamental time quantum τ₀ = 1, with one octave exactly eight ticks long. The phase field indexes one of the discrete phases kπ/4 for k = 0..7, matching the phase definition in the EightTick module.
proof idea
This is a structure definition. It introduces the type with fields phase : Fin 8, window : Set (Fin 8), and hNonempty : window.Nonempty. No lemmas or tactics are invoked.
why it matters
EightTickParams supplies the temporal parameters required by the feasibility predicate and the theorems exists_feasible_if_angleOK_and_time_slot and no_feasible_if_angle_below_threshold in the same module. It realizes the eight-tick octave (T7) by providing the discrete phase and window structure needed for gating measurements that combine angular and temporal conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.