EightTickFalsifier
plain-language theorem explainer
The EightTickFalsifier structure packages an observed event trace with a natural-number period that differs from 8 together with a placeholder assertion of superior performance, supplying a concrete witness against the eight-tick periodicity hypothesis. Researchers testing RRF discretization claims against pulsar timing or LNAL traces would cite it when exhibiting counterexamples. The definition is a plain record type whose sole non-trivial field is the inequality on the period; the performance field remains the trivial True placeholder.
Claim. A falsification witness for the eight-tick hypothesis consists of a finite list of events (the observed trace), a natural number $p$ satisfying $p ≠ 8$, and a proposition asserting that $p$ yields better performance than the eight-tick cycle.
background
The module states the eight-tick hypothesis explicitly: observed folding and recognition traces exhibit eight-phase periodicity, with phases 0-3 forming the LOCK segment (structure formation) and phases 4-7 forming the BALANCE segment (equilibration). This is presented as a testable claim about empirical traces rather than an axiom. The fundamental time quantum is the tick, defined as 1 in RS-native units, with one octave equal to eight ticks. Upstream constants include the period function from pulsar emission regimes, given by $φ^k$ for integer rung $k$.
proof idea
The declaration is a structure definition that directly introduces four fields: the trace list, the optimal period, the inequality proving it differs from 8, and a placeholder True proposition. No lemmas are invoked and no tactics are applied; it is a pure record type with no proof obligations beyond the stated inequality.
why it matters
This definition supplies the falsification interface for the eight-tick hypothesis and is used directly by the strongFalsifier predicate that checks whether the optimal period lies outside valid alternative periods. It operationalizes the module's listed falsification criteria, allowing concrete counterexamples to challenge the T7 eight-tick octave landmark of the forcing chain. The placeholder performance field leaves open the requirement for a concrete metric before the witness can support empirical tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.