earthLayerCount
plain-language theorem explainer
The declaration asserts that the finite set of canonical Earth layers has cardinality five, matching the configuration dimension in Recognition Science. Geophysicists and planetary modelers working in the RS framework cite this to fix the layer count for Earth as nested recognition spheres. The proof is a one-line decision procedure that enumerates the five constructors of the EarthLayer inductive type.
Claim. The cardinality of the finite set of Earth layers equals five: $|EarthLayer| = 5$, where EarthLayer enumerates the inner core, outer core, lower mantle, upper mantle, and crust.
background
The Geophysics from RS module models Earth as nested recognition spheres whose five canonical layers realize configDim D = 5. EarthLayer is the inductive type with constructors innerCore, outerCore, lowerMantle, upperMantle, crust, equipped with a derived Fintype instance. This local setting is stated directly in the module documentation and aligns with the five geophysical observables also set to dimension five.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card computation on the EarthLayer inductive type.
why it matters
This supplies the layer count used in geophysicsCert to certify five layers and five observables. It also feeds earthAxis for the coupled axis at dimension five, planetStrataCert, and the total strata count of fifteen. The result realizes the five-layer model required by the Recognition Science framework for Earth, consistent with configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.