amocTimescale_pos
plain-language theorem explainer
The theorem proves positivity of the AMOC characteristic timescale defined as phi to the eighth power. Oceanographers and Recognition Science modelers would cite it when confirming that the derived thermohaline timescale remains strictly positive in the J-cost framework. The proof is a one-line wrapper that unfolds the definition and applies the standard positivity of powers lemma to the positive base phi.
Claim. $0 < phi^8$ (in years), where $phi$ is the self-similar fixed point of the Recognition Composition Law.
background
The module derives the Atlantic Meridional Overturning Circulation timescale from the J-cost applied to the buoyancy-force ratio between warm saline inflow and cold freshwater deepening. The definition amocTimescale_yr sets this timescale explicitly to phi raised to the eighth power, yielding the RS prediction of approximately 47 years. This sits inside the first Oceanography module and relies on the phi-ladder and J-uniqueness from the forcing chain T5-T8.
proof idea
This is a one-line wrapper proof. It unfolds amocTimescale_yr to expose phi^(8:ℕ), then applies the lemma pow_pos using the known positivity of phi.
why it matters
The result supplies the amoc_pos field required by the downstream cert definition that assembles ThermohalineCert. It completes the structural theorem block for the Oceanography module by confirming the timescale is positive, directly invoking the eight-tick octave (exponent 8 = 2^3) from the forcing chain. The module falsifier remains an observed variability timescale outside the (20,100)-year band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.