plateTypeCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute or prove any plate velocity values.
- Does not establish the phi^5 ratio approximation for velocities.
- Does not derive the five types from spatial dimension D = 3.
- Does not prove that these five types are the only possible enumeration.
Lean usage
def exampleCert : PlateMotionCert := { five_types := plateTypeCount, phi_ratio := plateVelocityRatio }formal statement (Lean)
26theorem plateTypeCount : Fintype.card PlateType = 5 := by decide
proof body
27