eruptionRecurrenceCert
plain-language theorem explainer
The definition assembles an EruptionRecurrenceCert record by wiring the positivity, band, and cumulative identities already established for the VEI step ratio φ². Recognition Science modelers working on Track E6 would cite the resulting certificate when stating that adjacent-VEI recurrence ratios lie in (2.59, 2.63) and that cumulative ratios equal φ^{2k}. The construction is a direct record literal that references five sibling theorems for its fields.
Claim. Let φ denote the golden ratio. The eruption recurrence certificate is the structure whose fields assert 0 < φ², 2.59 < φ² < 2.63, ∀k ∈ ℕ (0 < φ^{2k}), ∀k ∈ ℕ (φ^{2k} = (φ²)^k), and φ² = φ².
background
The module models volcanic eruption recurrence intervals on the recognition lattice. Each VEI step corresponds to one octave on the J-cost spectrum, so the ratio between successive classes is fixed at φ². The cumulative ratio across k steps is therefore defined as φ^{2k}. EruptionRecurrenceCert is the structure that packages the five required properties: positivity of the step ratio, its numerical band, positivity of all cumulative ratios, the factorization into powers of the step ratio, and the one-step base case.
proof idea
The definition is a direct record construction. It populates the five fields of EruptionRecurrenceCert by supplying the theorems vei_step_ratio_pos, vei_step_ratio_band, cumulative_ratio_pos, cumulative_ratio_factors, and cumulative_ratio_one_step.
why it matters
The definition supplies the concrete certificate referenced by the eruption recurrence one-statement comment in the same module. It thereby completes the structural claim for Track E6: the φ² ratio and its cumulative powers satisfy the positivity and factorization conditions required by the eight-tick lattice. The construction rests on the phi-ladder and the gap-45 frustration already derived in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.