categoryCount_pos
plain-language theorem explainer
The theorem establishes positivity of the Saffir-Simpson hurricane category count. Researchers constructing RS-derived meteorological certificates cite it to confirm the count exceeds zero before bundling into larger structures. The proof is a one-line wrapper that rewrites via the equality to five and normalizes the resulting numeric inequality.
Claim. $0 < 5$
background
The module models the Saffir-Simpson scale inside Recognition Science by tying category count to configDim D = 5 on the phi-ladder. hurricaneCategoryCount is defined directly as the natural number 5. The upstream equality hurricaneCategoryCount_eq states that this definition holds by reflexivity and supplies the substitution needed for all subsequent checks.
proof idea
The proof is a one-line wrapper. It applies rw on hurricaneCategoryCount_eq to reduce the goal to 0 < 5, then invokes norm_num to discharge the numeric fact.
why it matters
The result supplies the count_pos field inside the HurricaneCategoryCert constructor, which also carries the equality and the cost-at-threshold lemma. It thereby completes the structural claim that D = 5 forces exactly five categories with threshold ratio near phi to the one-third. The module falsifier notes that adoption of a sixth category would require either D = 4 or a non-phi organizational principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.