eightbeat_holds
plain-language theorem explainer
The lemma asserts existence of a complete cover in three dimensions with exact period 8. Researchers tracing the eight-tick octave in the Recognition Science forcing chain would cite it to confirm T7. The proof is a one-line simplification that invokes the period_exactly_8 result from the Patterns module.
Claim. $There exists a complete cover $w$ of dimension 3 such that the period of $w$ equals 8$.
background
The module URCAdapters.EightBeat isolates the eight-beat existence statement. Its sole definition eightbeat_prop encodes the claim as the existence of a CompleteCover object of dimension 3 whose period field equals 8. CompleteCover is imported from IndisputableMonolith.Patterns and represents a periodic covering structure whose period is a positive integer. The upstream lemma period_exactly_8 in Patterns supplies the concrete existence witness used here.
proof idea
The proof is a one-line wrapper that applies the period_exactly_8 theorem from IndisputableMonolith.Patterns via the simpa tactic.
why it matters
This result verifies the eight-beat existence required by the T7 step of the forcing chain, where the period is fixed at 2^3. It anchors the self-similar octave structure that later steps use to derive D=3 and the phi-ladder mass formula. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.