octavePeriod_pos
plain-language theorem explainer
The theorem establishes that the octave period, defined as 2^3 in the volcanic forcing model, is strictly positive. Geologists modeling climate cascades via J-cost impulses cite this to keep per-octave impulse magnitudes well-defined and non-negative. The proof is a one-line term wrapper that rewrites via the equality to eight and discharges the numerical goal with norm_num.
Claim. $0 < 2^{3}$, where $2^{3}$ is the minimal complete-cover period for the three-dimensional climate cascade.
background
In the volcanic forcing module the octave period is the natural number $2^{3}$, the minimal climate-cascade period forced at D=3 by the eight-tick structure. It multiplies the J-cost of the VEI ratio to produce the per-octave impulse on the climate ledger. The module replaces an earlier placeholder exponent with this derivation from Patterns.eight_tick_min and Cost.Jcost.
proof idea
The proof is a one-line term wrapper. It rewrites the goal with the lemma octavePeriod_eq_eight to obtain 0 < 8, then applies norm_num to finish.
why it matters
This result anchors the non-negativity and strict-positivity theorems for impulse_per_octave in the same module. It realizes the T7 step of the unified forcing chain by confirming the eight-tick octave period is positive, enabling the impulse formula impulse_per_octave(VEI) = J(VEI_ratio) · period at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.