atmo_is_proper_subset
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 in Recognition Science
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.
scope and limits
- Does not prove physical nesting or radial ordering of the layers.
- Does not derive phi-ladder ratios for wave speeds.
- Does not generalize to stratifications on other planets.
- Does not supply an explicit injection witnessing the subset relation.
Lean usage
example : Fintype.card PlanetStratum > Fintype.card AtmosphericLayer := atmo_is_proper_subsetformal statement (Lean)
47theorem atmo_is_proper_subset :
48 Fintype.card PlanetStratum > Fintype.card AtmosphericLayer := by
proof body
One-line wrapper that applies rw.
49 rw [planetStratumCount, atmoCount]; decide
50