pith. machine review for the scientific record. sign in
def definition def or abbrev high

eruptionRecurrenceCert

show as:
view Lean formalization →

Eruption recurrence ratios between successive VEI classes are certified to equal φ² in the interval (2.59, 2.63). Recognition theorists working on the geology track would cite this certificate when invoking the φ-ladder prediction for volcanic intervals. The definition is a direct record constructor that assembles six sibling lemmas on positivity, band membership, and power factorization.

claimThe certificate asserts that the VEI step ratio $r = φ^2$ satisfies $0 < r$ and $2.59 < r < 2.63$, the cumulative ratio across $k$ steps equals $φ^{2k}$, this equals $r^k$ for all $k$, and the base case $k=1$ recovers $r$.

background

The module models volcanic recurrence on the recognition lattice, with each VEI step as one octave in the J-cost impulse spectrum. It defines cumulative_ratio k := φ^(2k) and the structure EruptionRecurrenceCert with fields for step-ratio positivity, the numerical band (2.59, 2.63), cumulative positivity, factorization into powers of the step ratio, and the one-step equality. Upstream lemmas establish vei_step_ratio = φ² together with its positivity and band membership, plus the power identities for the cumulative function.

proof idea

This is a definition that constructs the certificate by direct field assignment: step_ratio_pos is taken from vei_step_ratio_pos, the band from vei_step_ratio_band, cumulative_pos from cumulative_ratio_pos, factors from cumulative_ratio_factors, and the one-step equality from cumulative_ratio_one_step.

why it matters in Recognition Science

This supplies the master certificate for Track E6, realizing the structural prediction that adjacent-VEI recurrence ratios cluster at φ² and cumulatives at φ^(2k). The module doc ties the ratio to the eight-tick octave plus gap-45 frustration on long-period events, with the explicit falsifier that any median GVP ratio for n ≥ 4 falls outside (2.5, 2.7).

scope and limits

formal statement (Lean)

 103def eruptionRecurrenceCert : EruptionRecurrenceCert where
 104  step_ratio_pos := vei_step_ratio_pos

proof body

Definition body.

 105  step_ratio_band := vei_step_ratio_band
 106  cumulative_pos := cumulative_ratio_pos
 107  cumulative_factors := cumulative_ratio_factors
 108  one_step_eq := cumulative_ratio_one_step
 109
 110/-- **ERUPTION RECURRENCE ONE-STATEMENT.** Adjacent-VEI eruption
 111recurrence ratios cluster at `φ² ∈ (2.59, 2.63)`; cumulative
 112recurrence across `k` VEI steps equals `φ^(2k) = (φ²)^k`. -/

depends on (6)

Lean names referenced from this declaration's body.