planetStrataCert
plain-language theorem explainer
The definition planetStrataCert assembles a certificate structure for the planetary 15-stratum model in Recognition Science. It certifies that the atmosphere, solid Earth, and ocean each consist of five layers whose cardinalities sum to fifteen, with the same total recovered via the disjoint sum over the three RS axes. A researcher modeling planetary wave propagation or strata in the RS framework would cite this to invoke the structural claim without rederiving the layer counts. The construction is a direct field assignment from three decide-tl
Claim. Define the certificate structure $C$ by the assignments $|$AtmosphericLayer$| = 5$, $|$EarthLayer$| = 5$, $|$OceanLayer$| = 5$, $|$AtmosphericLayer$| + |$EarthLayer$| + |$OceanLayer$| = 15$, and the sum of the three axis cardinalities of the planet strata sum equals 15.
background
In the Recognition Science framework the planet is modeled as a direct sum of three independent five-layer stacks (atmosphere, solid Earth, ocean) whose cardinalities add to fifteen. Each physical parcel belongs to exactly one stratum in one stack; the construction is therefore a disjoint sum rather than a tensor product. The module proves only this finite structural claim; any wave-speed phi-ratio predictions are left empirical.
proof idea
The definition constructs the PlanetStrataCert instance by direct field assignment: atmosphericLayerCount supplies the atmospheric_count field, earthLayerCount supplies earth_count, oceanLayerCount supplies ocean_count, planet_strata_total_15 supplies total_15, and planet_strata_disjoint_sum_15 supplies rs_sum_15.
why it matters
This definition supplies the concrete certificate for the C2 planetary 15-stratum claim. It closes the structural part of the planetary strata model, which is a prerequisite for any downstream application of the disjoint-sum composition law to planetary physics. The module documentation notes that the wave-speed phi-ratio prediction remains empirical, leaving open the derivation of dynamical predictions from the strata counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.