EarthLayer
plain-language theorem explainer
The inductive type enumerating Earth's five interior layers supports Recognition Science models of planetary stratification under the configDim D equals five constraint. Researchers deriving geophysical observables from nested recognition spheres cite it when establishing layer counts or certifying cross-domain relations. The declaration is a direct inductive enumeration whose decidable equality and finite type instances are generated automatically by the deriving clauses.
Claim. The inductive type of Earth layers is generated by the five constructors corresponding to the inner core, outer core, lower mantle, upper mantle, and crust.
background
In the GeophysicsFromRS module the Earth is modeled as nested recognition spheres whose configuration dimension equals five. This produces the five canonical layers that underlie the five geophysical observables (seismicity, gravimetry, geomagnetism, heat flow, GPS geodesy). The module states that Lean encodes exactly these five layers plus five observables with zero axioms or sorrys.
proof idea
The declaration is a bare inductive definition containing no proof body. The four deriving clauses for decidable equality, representation, boolean equality, and finite type are supplied automatically by Lean from the five-constructor enumeration.
why it matters
This definition supplies the layer type required by the earth layer count theorem and the planet stratification certificate, which records fifteen total strata as three times five. It realizes the module claim that five geophysical observables equal configDim D, consistent with the eight-tick octave and spatial dimension three from the unified forcing chain. The definition closes the local scaffolding for geophysical certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.