eightbeat_holds
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 in Recognition Science
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.
scope and limits
- Does not construct an explicit cover witness.
- Does not prove uniqueness of the period-8 cover.
- Does not extend the result to dimensions other than 3.
- Does not connect the period to the Recognition Composition Law or the phi fixed point.
formal statement (Lean)
10lemma eightbeat_holds : eightbeat_prop := by
proof body
Term-mode proof.
11 simpa using IndisputableMonolith.Patterns.period_exactly_8
12
13end URCAdapters
14end IndisputableMonolith