strongFalsifier
plain-language theorem explainer
The declaration defines a strong falsifier for the eight-tick hypothesis as any EightTickFalsifier whose optimal period falls outside the valid alternatives of 4, 8, or 16 ticks. Researchers testing the RRF discretization would cite this to flag decisive counterexamples to the 8-phase cycle. The definition is a direct membership check against the list of valid periods.
Claim. Let $f$ be a falsification witness for an event type $E$, consisting of a trace, an optimal period $p$ with $p ≠ 8$, and evidence that $p$ works better. Then $f$ is a strong falsifier if $p ∉ {4, 8, 16}.
background
The module states the 8-tick hypothesis as an explicit claim about observed recognition traces in the RRF framework: traces exhibit 8-phase periodicity with phases 0-3 for LOCK (structure formation) and 4-7 for BALANCE (equilibration). An EightTickFalsifier is the structure supplying a trace, an optimalPeriod ≠ 8, and a placeholder works_better metric. validAlternativePeriods returns the list [4, 8, 16] to allow half-cycle or double-cycle alternatives. Upstream, RRF is the local non-sealed recognition field interface (Fin 4 → ℝ) → ℝ, while E counts the edges of the D-cube as D × 2^(D-1).
proof idea
This is a direct definition that checks whether the optimalPeriod field of the input EightTickFalsifier lies outside the list returned by validAlternativePeriods.
why it matters
This definition sharpens the falsification criteria for the eight-tick hypothesis in the RRF module. It distinguishes weak alternatives (4 or 16 ticks) from strong counterexamples that would challenge the T7 eight-tick octave in the forcing chain. It supports empirical testing of the discretization without providing a full theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.