def
definition
validAlternativePeriods
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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