PlanetStratificationCert
PlanetStratificationCert packages the combinatorial assertion that the planet stratum set has cardinality 15 as the disjoint union of three five-element layer sets. Researchers working on cross-domain wave propagation in Recognition Science cite the structure to fix the 5+5+5 count before invoking phi-ladder ratios on boundary velocities. The definition is a direct record whose five fields are populated by sibling cardinality lemmas.
claimLet $S$ denote the disjoint union of the atmospheric, terrestrial, and oceanic layer sets. Then the cardinality of $S$ equals 15, $15 = 3 times 5$, and the cardinality of $S$ is strictly larger than the cardinality of each of the three component sets.
background
PlanetStratum is the disjoint union AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer. Each component is an inductive type with five constructors (troposphere through exosphere; innerCore through crust; surface through abyssal), so each carries Fintype cardinality 5. The module sets the local theoretical setting for cross-domain stratification C2, where the three strata occupy distinct radial shells and therefore combine by sum rather than product.
proof idea
PlanetStratificationCert is introduced directly as a structure whose fields are the five required cardinality statements. No lemmas are applied and no tactics are used; the structure functions as a typed container that is later instantiated by the sibling definition planetStratificationCert.
why it matters in Recognition Science
The structure supplies the combinatorial backbone for the C2 claim inside the Recognition Science framework. It is instantiated by planetStratificationCert, which anchors downstream arguments that link the 15-element stratification to testable phi-ladder ratios between atmospheric and seismic velocities. The three_D field aligns with the spatial dimension D = 3 from the unified forcing chain while the 5+5+5 sum encodes the nested radial shells.
scope and limits
- Does not derive any wave equations or velocity fields inside the layers.
- Does not establish phi-ladder ratios between layer boundaries.
- Does not address empirical testability of the predicted velocity ratios.
- Does not connect to J-cost, defectDist, or the core forcing chain axioms.
formal statement (Lean)
62structure PlanetStratificationCert where
63 stratum_count : Fintype.card PlanetStratum = 15
64 three_D : 15 = 3 * 5
65 atmo_sub : Fintype.card PlanetStratum > Fintype.card AtmosphericLayer
66 earth_sub : Fintype.card PlanetStratum > Fintype.card EarthLayer
67 ocean_sub : Fintype.card PlanetStratum > Fintype.card OceanLayer
68