plateTypeCount
plain-language theorem explainer
plateTypeCount establishes that the Recognition Science model of plate tectonics admits exactly five canonical types. Earth-dynamics researchers using the phi-ladder for velocity predictions would cite this count to fix the configDim parameter at 5. The proof is a one-line decide tactic that evaluates the Fintype instance derived from the five-constructor inductive enumeration.
Claim. The finite set of plate types has cardinality five: $|PlateType| = 5$, where $PlateType$ enumerates the variants continentalFast, continentalSlow, oceanicFast, oceanicSlow, and collisional.
background
The PlateMotionFromPhiLadder module predicts plate velocities on the phi-ladder, with fastest-to-slowest ratios near phi^5. It introduces five canonical plate types (continental fast, continental slow, oceanic fast, oceanic slow, collisional) that realize configDim D = 5. This rests on the upstream inductive definition of PlateType, which enumerates the five cases and derives DecidableEq, Repr, BEq, and Fintype.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the goal Fintype.card PlateType = 5. The tactic succeeds because the inductive type carries an automatically generated Fintype instance whose cardinality is exactly the number of constructors.
why it matters
This supplies the five_types component of the downstream plateMotionCert definition, which pairs it with plateVelocityRatio to certify the full plate-motion model. It realizes the module's claim that five types arise from the phi-ladder structure in the Recognition framework, consistent with the eight-tick octave and spatial dimension D = 3. No open scaffolding questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.