validAlternativePeriods
plain-language theorem explainer
The definition supplies the fixed list of admissible alternative periods [4, 8, 16] for the eight-tick discretization hypothesis. Researchers testing periodicity in recognition traces or pulsar emission regimes would cite this list when constructing a falsifier predicate. It is realized as a direct constant enumeration to enable membership checks.
Claim. The admissible alternative cycle lengths are the list $[4, 8, 16]$.
background
The module states the eight-tick hypothesis as an explicit claim that observed folding and recognition traces exhibit 8-phase periodicity, with phases 0-3 forming the LOCK stage of structure formation and phases 4-7 forming the BALANCE stage of equilibration. The hypothesis is presented as a testable interface rather than a definitional axiom, and the module supplies falsification criteria based on traces that favor non-8 periodicity. The upstream period definition returns rung-dependent periods via the expression phi^k, while the evidence definition returns the marginal likelihood computed as the sum over prior probabilities times likelihood values.
proof idea
The declaration is a one-line definition that returns the constant list containing the integers 4, 8 and 16.
why it matters
The list is referenced directly by the strongFalsifier predicate to decide whether an observed optimal period lies outside the admissible set and thereby supplies strong evidence against the hypothesis. It operationalizes the first falsification criterion listed in the module documentation. The enumerated values align with the eight-tick octave (period 2^3) identified at step T7 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.