trivialParams
plain-language theorem explainer
The baseline eight-tick parameter set is supplied with phase zero and the universal window over the eight ticks. Researchers modeling temporal gating in Recognition Science reference this construction to establish that any angle-admissible configuration is feasible under continuous sampling. The definition is realized by a direct structure literal together with a classical nonemptiness witness for the full set.
Claim. Define the baseline eight-tick gating parameters to have phase index $0$, admissible window equal to the full set of eight ticks, and the canonical witness that the window is nonempty.
background
The TemporalGating module abstracts discrete eight-tick sampling windows and combines them with the angle threshold to form a feasibility predicate. EightTickParams is the structure consisting of a phase in Fin 8, a nonempty subset of admissible ticks, and the nonemptiness proof; its doc-comment states it packages 'a chosen phase and a nonempty set of admissible windows.' This setting rests on the phase definition from the EightTick foundation, which assigns $kπ/4$ to each index $k$, and on the R3 geometry imported from ActionSmallAngle and BlindCone. The angleOK predicate asserts that the angle formed at $x$ by $y$ and $z$ meets or exceeds the budget-dependent threshold thetaMin(Amax).
proof idea
The definition is realized by a direct structure literal that sets phase to 0, window to the universal set, and supplies the nonemptiness witness via classical exact Set.nonempty_univ. No upstream lemmas are applied beyond the built-in properties of the universal set.
why it matters
This supplies the canonical always-on case for the feasibility predicate, enabling the module example to conclude that angleOK configurations admit a feasible tick index. It instantiates the eight-tick structure central to the T7 octave in the forcing chain. No parent theorems appear among the used-by edges, indicating its role as an internal example rather than a lemma feeding further results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.