def
definition
validAlternativePeriods
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Hypotheses.EightTick on GitHub at line 122.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
119 works_better : True -- Placeholder for a concrete metric
120
121/-- Alternative: 4-tick (half cycle) or 16-tick (double cycle) might also work. -/
122def validAlternativePeriods : List ℕ := [4, 8, 16]
123
124/-- If a falsifier exists with period outside valid alternatives, it's strong evidence. -/
125def strongFalsifier (E : Type*) (f : EightTickFalsifier E) : Prop :=
126 f.optimalPeriod ∉ validAlternativePeriods
127
128end RRF.Hypotheses
129end IndisputableMonolith