octavePeriod_eq_eight
plain-language theorem explainer
The climate cascade octave period equals 8 ticks at spatial dimension 3. Geologists and climate modelers working with volcanic J-cost impulses cite this result to anchor the per-octave impulse magnitude. The proof is a one-line term that unfolds the definition of octavePeriod and normalizes the numeral.
Claim. The period of one octave in the eight-tick climate cascade equals $8$.
background
The module frames volcanic eruptions as instantaneous J-cost impulses on the climate's eight-tick attractor whose state space is the 3-bit pattern. octavePeriod is the length of the minimal complete cover of that pattern space. MODULE_DOC states that the exponent 8 is forced by T7 at D=3 via Patterns.eight_tick_min rather than asserted. Upstream Constants.RSNativeUnits.octavePeriod supplies the definition being evaluated, while MusicalScale.octave records the base ratio 2.
proof idea
Term-mode proof. It unfolds the definition of octavePeriod then applies norm_num to reduce the resulting expression to the numeral 8.
why it matters
This supplies the concrete value required by octavePeriod_is_minimal_cover (which invokes Patterns.eight_tick_min) and by volcanic_forcing_one_statement (which packages the three structural facts of volcanic forcing). It realizes the T7 eight-tick octave (period 2^3) inside the geology track and closes the placeholder exponent from v4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.