EarthLayer
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive layer radii or densities from the phi-ladder.
- Does not connect boundaries to the J-cost or Recognition Composition Law.
- Does not address wave-speed predictions at the tropopause or asthenosphere.
- Does not prove dynamical properties such as seismic phase velocities.
formal statement (Lean)
29inductive EarthLayer where
30 | innerCore | outerCore | lowerMantle | upperMantle | crust
31 deriving DecidableEq, Repr, BEq, Fintype
32