earth_is_proper_subset
plain-language theorem explainer
The theorem asserts that the full planetary stratification has strictly more elements than the terrestrial layer alone. Cross-domain modelers in Recognition Science cite it when assembling the nested sum structure for Earth. The proof is a one-line wrapper that rewrites the two cardinalities and hands the resulting numerical inequality to the decide tactic.
Claim. Let $P$ be the disjoint union of the atmospheric, terrestrial, and oceanic layers and let $E$ be the terrestrial layer. Then $|P| > |E|$.
background
The Planet Stratification module models Earth as three nested five-element stratifications whose disjoint sum is PlanetStratum := AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer. EarthLayer is the inductive type whose five constructors are innerCore, outerCore, lowerMantle, upperMantle and crust. Upstream theorems planetStratumCount and earthCount fix the respective cardinalities at 15 and 5; the former records that each injection covers only five of the fifteen strata.
proof idea
The proof is a one-line wrapper that rewrites the target inequality by planetStratumCount and earthCount, then applies decide to confirm 15 > 5.
why it matters
The result is one of the three subset facts aggregated inside planetStratificationCert. It therefore supplies the combinatorial half of the module claim that three nested D = 5 stratifications sum to fifteen. In the Recognition framework this supplies a discrete layering model consistent with the eight-tick octave; the module documentation notes that the corresponding phi-ladder wave-speed predictions remain open for empirical test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.