cert
plain-language theorem explainer
The definition assembles a certificate that the hurricane category count equals five with positive value and zero cost at equal nonzero weights. Recognition Science researchers would cite it to link the phi-ladder to the Saffir-Simpson scale via dimensional forcing. It is a direct structure record that supplies the three required fields from sibling results.
Claim. The certificate satisfies category count equals five, the count is positive, and the cost function vanishes for all nonzero equal arguments.
background
The module derives the Saffir-Simpson hurricane scale from the phi-ladder. It states that five categories are forced by configuration dimension five, with adjacent thresholds in ratio approximately the cube root of phi. The local setting treats this as a structural theorem with zero axioms or sorrys, and supplies a falsifier: adoption of a sixth category would require either dimension four or a non-phi principle.
proof idea
The definition is a direct structure constructor that supplies the three fields of the certificate. It assigns the count equality from the reflexivity result on the count, the positivity from the norm-num reduction of that equality, and the cost property from unfolding the cost definition followed by the unit-zero lemma on J-cost.
why it matters
This certificate closes the meteorology application of the phi-ladder by instantiating the required structural properties. It supports the framework claim that five categories follow from the dimensional prediction in the forcing chain. The module doc-comment positions the result as part of the structural theorem and notes the explicit falsifier for a sixth category.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.