atmo_is_proper_subset
plain-language theorem explainer
The cardinality of the full planetary stratification exceeds that of the atmospheric layer alone because the former is the disjoint sum of three five-element strata while the latter is a single five-element set. Researchers modeling cross-domain embeddings in Recognition Science cite this to confirm the proper-subset relations among radial shells. The proof is a one-line wrapper that rewrites the goal with the precomputed cardinality theorems and decides the resulting numerical inequality.
Claim. $|A| > |B|$ where $A$ is the disjoint union of the atmospheric, terrestrial and oceanic layers and $B$ is the atmospheric layer.
background
In the CrossDomain.PlanetStratification module PlanetStratum is the disjoint sum AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer. AtmosphericLayer is the inductive type with five constructors (troposphere through exosphere). The upstream theorem atmoCount states that AtmosphericLayer has cardinality 5 while planetStratumCount states that the full sum has cardinality 15 by adding the three component counts. The module documentation presents this as the structural claim for three nested five-element stratifications covering Earth, distinct from a product because the strata occupy different radial shells.
proof idea
The proof is a one-line wrapper. It rewrites the goal using planetStratumCount and atmoCount to obtain the concrete inequality 15 > 5, then applies the decide tactic.
why it matters
This theorem supplies the atmo_sub field of the planetStratificationCert record that aggregates the three proper-subset statements with the total count. It completes the combinatorial certification for the 5+5+5 structure in the C2 wave of the Recognition Science framework, consistent with the emphasis on D = 3 realized through summed five-element strata. The module documentation notes the implied testable phi-ladder ratios for wave speeds at the tropopause and asthenosphere boundary, although that dynamical content lies outside the present result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.