OctaveFamily
plain-language theorem explainer
OctaveFamily packages a map from integer rungs to octaves for multi-scale recognition models. Researchers assembling consistent state spaces and strain functionals across manifestation levels would reference it when building RRF structures. The definition is a direct structure with one field that assigns an Octave instance to each rung without added constraints or proofs.
Claim. An octave family is a map $f : OctaveRung → Octave$ where $OctaveRung := ℤ$ and each octave consists of a state space $S$, a strain functional $J : S → ℝ$, a channel bundle, and a non-emptiness witness.
background
The RRF.Core.Octave module treats an octave as an abstract scale of manifestation in which the same underlying pattern appears at different levels. OctaveRung is the integer type alias serving as the rung index. Each Octave is a structure containing a state space Type*, the strain functional (J-cost), a ChannelBundle of display channels, and a Nonempty witness. Upstream results define the octave ratio as 2 or the period as 8 ticks, while phi-scaling remains a separate hypothesis layered on top.
proof idea
This is a structure definition whose single field octaveAt directly encodes the map from OctaveRung to Octave. No lemmas or tactics are invoked; the declaration simply packages the family at the type level.
why it matters
The structure supplies the abstract octave scaffolding required by the RRF core, aligning with the eight-tick octave period in the forcing chain. It supports the hypothesis that particles, proteins, and other entities are manifestations of the same pattern at different scales, while keeping physical constants and phi-ladder relations outside this definition. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.