EarthLayer
plain-language theorem explainer
EarthLayer enumerates the five radial shells of Earth's solid interior as an inductive type. Cross-domain modelers cite it when forming the composite PlanetStratum as the disjoint sum of atmospheric, terrestrial, and oceanic strata. The declaration is a direct inductive definition that introduces the five cases and derives decidable equality together with finite-type structure.
Claim. The inductive type of Earth's interior layers consists of five cases: inner core, outer core, lower mantle, upper mantle, and crust.
background
The module treats planetary stratification as a disjoint sum of three five-element types because the strata occupy distinct radial shells and cannot overlap at the same radius. EarthLayer supplies the five solid-interior cases that complete the sum AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer. This yields the fifteen-element PlanetStratum required for the C2 structural claim.
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances in one step.
why it matters
EarthLayer supplies one summand of PlanetStratum and is invoked by earthCount, earth_is_proper_subset, and PlanetStratificationCert to establish the relations 15 = 3 × 5 together with proper-subset inequalities. It thereby fills the combinatorial half of the 5 + 5 + 5 = 15 claim in the cross-domain stratification. The construction follows the Recognition Science pattern of encoding nested physical structure by finite sum types rather than continuous geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.