pith. sign in
theorem

hurricaneCategoryCount_eq

proved
show as:
module
IndisputableMonolith.Meteorology.HurricaneCategoryFromPhiLadder
domain
Meteorology
line
31 · github
papers citing
none yet

plain-language theorem explainer

Recognition Science derives the Saffir-Simpson hurricane scale as having precisely five categories from the five-dimensional configuration space. Framework users in meteorology and RS modelers cite this when validating the category count against observations. The proof is a direct reflexivity on the constant definition of the count.

Claim. The number of Saffir-Simpson hurricane categories equals five: $N = 5$.

background

In the Meteorology.HurricaneCategoryFromPhiLadder module the local setting is a structural theorem with zero axioms or sorrys. The definition sets the category count to the natural number five, matching the observed Saffir-Simpson categories one through five. This count is predicted by the Recognition Science forcing chain at step T8 where the configuration dimension equals five.

proof idea

The proof proceeds by term-mode reflexivity, which immediately equates the definition of the hurricane category count to the numeral five without further computation.

why it matters

This equality is the base fact feeding the positivity theorem categoryCount_pos and the certificate definition cert in the same module. It realizes the module's claim that five categories are forced by configDim D equals five, consistent with the eight-tick octave and phi-ladder structure in the broader framework. The module doc states that adoption of a sixth category would require either dimension four or a non-phi principle.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.