earthCount
The theorem asserts that the finite type EarthLayer has cardinality five, matching the five radial shells of the planet. Researchers assembling the Recognition Science planet stratification model cite it when summing the three nested D=5 strata to fifteen. The proof is a direct decision procedure that enumerates the five inductive constructors.
claimThe cardinality of the finite set of Earth layers equals 5, where the layers are the inner core, outer core, lower mantle, upper mantle, and crust.
background
EarthLayer is defined as an inductive type whose five constructors are innerCore, outerCore, lowerMantle, upperMantle, and crust; it derives DecidableEq, Repr, BEq, and Fintype. This supplies the middle term in the module's structural claim that three nested D=5 stratifications cover Earth via the disjoint sum AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer = 15. The same inductive definition appears upstream in GeophysicsFromRS, establishing the combinatorial count before any physical mapping.
proof idea
The proof applies the decide tactic. Because the inductive type derives Fintype, decide computes the cardinality directly from the five constructors without invoking additional lemmas.
why it matters in Recognition Science
This supplies the middle cardinality in planetStratumCount, which establishes the total of 15, and is invoked by earth_is_proper_subset to witness the proper inclusion. It fills the combinatorial slot in the Wave 62 cross-domain claim of the module documentation, consistent with the Recognition Science requirement that each stratum obey the five-element count before phi-ladder ratios are tested at the boundaries.
scope and limits
- Does not derive the layer count from the J-uniqueness or forcing chain.
- Does not map the five shells to observed seismic discontinuities.
- Does not establish phi-ladder ratios for wave speeds at the boundaries.
- Does not extend the count to non-Earth planets or other stratifications.
Lean usage
rw [earthCount]formal statement (Lean)
38theorem earthCount : Fintype.card EarthLayer = 5 := by decide